Step | Hyp | Ref
| Expression |
1 | | amgmlemALT.0 |
. . 3
mulGrpℂfld |
2 | | amgmlemALT.1 |
. . 3
|
3 | | amgmlemALT.2 |
. . 3
|
4 | | amgmlemALT.3 |
. . 3
|
5 | | hashnncl 13157 |
. . . . . . . 8
|
6 | 2, 5 | syl 17 |
. . . . . . 7
|
7 | 3, 6 | mpbird 247 |
. . . . . 6
|
8 | 7 | nnrpd 11870 |
. . . . 5
|
9 | 8 | rpreccld 11882 |
. . . 4
|
10 | | fconst6g 6094 |
. . . 4
|
11 | 9, 10 | syl 17 |
. . 3
|
12 | | fconstmpt 5163 |
. . . . . 6
|
13 | 12 | a1i 11 |
. . . . 5
|
14 | 13 | oveq2d 6666 |
. . . 4
ℂfld g
ℂfld g |
15 | 7 | nnrecred 11066 |
. . . . . 6
|
16 | 15 | recnd 10068 |
. . . . 5
|
17 | | simpl 473 |
. . . . . 6
|
18 | | simplr 792 |
. . . . . 6
|
19 | 17, 18 | gsumfsum 19813 |
. . . . 5
ℂfld g
|
20 | 2, 16, 19 | syl2anc 693 |
. . . 4
ℂfld g
|
21 | | fsumconst 14522 |
. . . . . 6
|
22 | 2, 16, 21 | syl2anc 693 |
. . . . 5
|
23 | 7 | nncnd 11036 |
. . . . . 6
|
24 | 7 | nnne0d 11065 |
. . . . . 6
|
25 | 23, 24 | recidd 10796 |
. . . . 5
|
26 | 22, 25 | eqtrd 2656 |
. . . 4
|
27 | 14, 20, 26 | 3eqtrd 2660 |
. . 3
ℂfld g
|
28 | 1, 2, 3, 4, 11, 27 | amgmwlem 42548 |
. 2
g ℂfld g |
29 | | rpssre 11843 |
. . . . . 6
|
30 | | ax-resscn 9993 |
. . . . . 6
|
31 | 29, 30 | sstri 3612 |
. . . . 5
|
32 | | eqid 2622 |
. . . . . 6
↾s
↾s |
33 | | cnfldbas 19750 |
. . . . . . 7
ℂfld |
34 | 1, 33 | mgpbas 18495 |
. . . . . 6
|
35 | 32, 34 | ressbas2 15931 |
. . . . 5
↾s |
36 | 31, 35 | ax-mp 5 |
. . . 4
↾s |
37 | | cnfld1 19771 |
. . . . . 6
ℂfld |
38 | 1, 37 | ringidval 18503 |
. . . . 5
|
39 | 1 | oveq1i 6660 |
. . . . . . . . . 10
↾s mulGrpℂfld
↾s |
40 | 39 | rpmsubg 19810 |
. . . . . . . . 9
SubGrp ↾s |
41 | | subgsubm 17616 |
. . . . . . . . 9
SubGrp ↾s SubMnd ↾s |
42 | 40, 41 | ax-mp 5 |
. . . . . . . 8
SubMnd ↾s |
43 | | cnring 19768 |
. . . . . . . . . 10
ℂfld |
44 | | cnfld0 19770 |
. . . . . . . . . . . 12
ℂfld |
45 | | cndrng 19775 |
. . . . . . . . . . . 12
ℂfld |
46 | 33, 44, 45 | drngui 18753 |
. . . . . . . . . . 11
Unitℂfld |
47 | 46, 1 | unitsubm 18670 |
. . . . . . . . . 10
ℂfld SubMnd |
48 | 43, 47 | ax-mp 5 |
. . . . . . . . 9
SubMnd |
49 | | eqid 2622 |
. . . . . . . . . 10
↾s
↾s |
50 | 49 | subsubm 17357 |
. . . . . . . . 9
SubMnd SubMnd ↾s
SubMnd |
51 | 48, 50 | ax-mp 5 |
. . . . . . . 8
SubMnd ↾s
SubMnd
|
52 | 42, 51 | mpbi 220 |
. . . . . . 7
SubMnd
|
53 | 52 | simpli 474 |
. . . . . 6
SubMnd |
54 | | eqid 2622 |
. . . . . . 7
|
55 | 32, 54 | subm0 17356 |
. . . . . 6
SubMnd ↾s |
56 | 53, 55 | ax-mp 5 |
. . . . 5
↾s |
57 | 38, 56 | eqtri 2644 |
. . . 4
↾s |
58 | | cncrng 19767 |
. . . . . 6
ℂfld |
59 | 1 | crngmgp 18555 |
. . . . . 6
ℂfld
CMnd |
60 | 58, 59 | ax-mp 5 |
. . . . 5
CMnd |
61 | 32 | submmnd 17354 |
. . . . . 6
SubMnd
↾s |
62 | 53, 61 | mp1i 13 |
. . . . 5
↾s |
63 | 32 | subcmn 18242 |
. . . . 5
CMnd ↾s
↾s CMnd |
64 | 60, 62, 63 | sylancr 695 |
. . . 4
↾s CMnd |
65 | | reex 10027 |
. . . . . . . 8
|
66 | 65, 29 | ssexi 4803 |
. . . . . . 7
|
67 | | cnfldmul 19752 |
. . . . . . . . 9
ℂfld |
68 | 1, 67 | mgpplusg 18493 |
. . . . . . . 8
|
69 | 32, 68 | ressplusg 15993 |
. . . . . . 7
↾s |
70 | 66, 69 | ax-mp 5 |
. . . . . 6
↾s |
71 | | eqid 2622 |
. . . . . . . 8
mulGrpℂfld ↾s
mulGrpℂfld
↾s |
72 | 71 | rpmsubg 19810 |
. . . . . . 7
SubGrpmulGrpℂfld ↾s |
73 | 1 | oveq1i 6660 |
. . . . . . . . 9
↾s
mulGrpℂfld ↾s |
74 | | cnex 10017 |
. . . . . . . . . . 11
|
75 | | difss 3737 |
. . . . . . . . . . 11
|
76 | 74, 75 | ssexi 4803 |
. . . . . . . . . 10
|
77 | | rpcndif0 11851 |
. . . . . . . . . . 11
|
78 | 77 | ssriv 3607 |
. . . . . . . . . 10
|
79 | | ressabs 15939 |
. . . . . . . . . 10
mulGrpℂfld
↾s ↾s mulGrpℂfld
↾s |
80 | 76, 78, 79 | mp2an 708 |
. . . . . . . . 9
mulGrpℂfld
↾s ↾s mulGrpℂfld
↾s |
81 | 73, 80 | eqtr4i 2647 |
. . . . . . . 8
↾s
mulGrpℂfld
↾s ↾s |
82 | 81 | subggrp 17597 |
. . . . . . 7
SubGrpmulGrpℂfld ↾s ↾s |
83 | 72, 82 | mp1i 13 |
. . . . . 6
↾s |
84 | | simpr 477 |
. . . . . . . 8
|
85 | 15 | adantr 481 |
. . . . . . . 8
|
86 | 84, 85 | rpcxpcld 24476 |
. . . . . . 7
|
87 | | eqid 2622 |
. . . . . . 7
|
88 | 86, 87 | fmptd 6385 |
. . . . . 6
|
89 | | simprl 794 |
. . . . . . . . 9
|
90 | 89 | rprege0d 11879 |
. . . . . . . 8
|
91 | | simprr 796 |
. . . . . . . . 9
|
92 | 91 | rprege0d 11879 |
. . . . . . . 8
|
93 | 16 | adantr 481 |
. . . . . . . 8
|
94 | | mulcxp 24431 |
. . . . . . . 8
|
95 | 90, 92, 93, 94 | syl3anc 1326 |
. . . . . . 7
|
96 | | rpmulcl 11855 |
. . . . . . . . 9
|
97 | 96 | adantl 482 |
. . . . . . . 8
|
98 | | oveq1 6657 |
. . . . . . . . 9
|
99 | | ovex 6678 |
. . . . . . . . 9
|
100 | 98, 87, 99 | fvmpt3i 6287 |
. . . . . . . 8
|
101 | 97, 100 | syl 17 |
. . . . . . 7
|
102 | | oveq1 6657 |
. . . . . . . . . 10
|
103 | 102, 87, 99 | fvmpt3i 6287 |
. . . . . . . . 9
|
104 | 89, 103 | syl 17 |
. . . . . . . 8
|
105 | | oveq1 6657 |
. . . . . . . . . 10
|
106 | 105, 87, 99 | fvmpt3i 6287 |
. . . . . . . . 9
|
107 | 91, 106 | syl 17 |
. . . . . . . 8
|
108 | 104, 107 | oveq12d 6668 |
. . . . . . 7
|
109 | 95, 101, 108 | 3eqtr4d 2666 |
. . . . . 6
|
110 | 36, 36, 70, 70, 83, 83, 88, 109 | isghmd 17669 |
. . . . 5
↾s ↾s |
111 | | ghmmhm 17670 |
. . . . 5
↾s ↾s
↾s MndHom ↾s |
112 | 110, 111 | syl 17 |
. . . 4
↾s MndHom ↾s |
113 | | 1red 10055 |
. . . . 5
|
114 | 4, 2, 113 | fdmfifsupp 8285 |
. . . 4
finSupp |
115 | 36, 57, 64, 62, 2, 112, 4, 114 | gsummhm 18338 |
. . 3
↾s g
↾s g |
116 | 53 | a1i 11 |
. . . . 5
SubMnd |
117 | 4 | ffvelrnda 6359 |
. . . . . . 7
|
118 | 15 | adantr 481 |
. . . . . . 7
|
119 | 117, 118 | rpcxpcld 24476 |
. . . . . 6
|
120 | | eqid 2622 |
. . . . . 6
|
121 | 119, 120 | fmptd 6385 |
. . . . 5
|
122 | 2, 116, 121, 32 | gsumsubm 17373 |
. . . 4
g ↾s g |
123 | 9 | adantr 481 |
. . . . . 6
|
124 | 4 | feqmptd 6249 |
. . . . . 6
|
125 | 2, 117, 123, 124, 13 | offval2 6914 |
. . . . 5
|
126 | 125 | oveq2d 6666 |
. . . 4
g g |
127 | 102 | cbvmptv 4750 |
. . . . . . 7
|
128 | 127 | a1i 11 |
. . . . . 6
|
129 | | oveq1 6657 |
. . . . . 6
|
130 | 117, 124,
128, 129 | fmptco 6396 |
. . . . 5
|
131 | 130 | oveq2d 6666 |
. . . 4
↾s g
↾s g |
132 | 122, 126,
131 | 3eqtr4rd 2667 |
. . 3
↾s g g |
133 | 36, 57, 64, 2, 4, 114 | gsumcl 18316 |
. . . . 5
↾s g |
134 | | oveq1 6657 |
. . . . . 6
↾s g ↾s g |
135 | 134, 87, 99 | fvmpt3i 6287 |
. . . . 5
↾s g ↾s g ↾s g |
136 | 133, 135 | syl 17 |
. . . 4
↾s g ↾s g |
137 | 2, 116, 4, 32 | gsumsubm 17373 |
. . . . 5
g
↾s g |
138 | 137 | oveq1d 6665 |
. . . 4
g ↾s g |
139 | 136, 138 | eqtr4d 2659 |
. . 3
↾s g g |
140 | 115, 132,
139 | 3eqtr3d 2664 |
. 2
g g |
141 | 117 | rpcnd 11874 |
. . . . . . 7
|
142 | 2, 141 | fsumcl 14464 |
. . . . . 6
|
143 | 142, 23, 24 | divrecd 10804 |
. . . . 5
|
144 | 2, 16, 141 | fsummulc1 14517 |
. . . . 5
|
145 | 143, 144 | eqtr2d 2657 |
. . . 4
|
146 | 16 | adantr 481 |
. . . . . 6
|
147 | 141, 146 | mulcld 10060 |
. . . . 5
|
148 | 2, 147 | gsumfsum 19813 |
. . . 4
ℂfld g
|
149 | 2, 141 | gsumfsum 19813 |
. . . . 5
ℂfld g |
150 | 149 | oveq1d 6665 |
. . . 4
ℂfld g
|
151 | 145, 148,
150 | 3eqtr4d 2666 |
. . 3
ℂfld g ℂfld g |
152 | 2, 117, 146, 124, 13 | offval2 6914 |
. . . 4
|
153 | 152 | oveq2d 6666 |
. . 3
ℂfld g
ℂfld g |
154 | 124 | oveq2d 6666 |
. . . 4
ℂfld g ℂfld g |
155 | 154 | oveq1d 6665 |
. . 3
ℂfld g ℂfld g |
156 | 151, 153,
155 | 3eqtr4d 2666 |
. 2
ℂfld g
ℂfld g |
157 | 28, 140, 156 | 3brtr3d 4684 |
1
g ℂfld g |