Step | Hyp | Ref
| Expression |
1 | | mdetrsca.eq |
. . . . . . . . . . . . . 14
|
2 | 1 | oveqd 6667 |
. . . . . . . . . . . . 13
|
3 | 2 | adantr 481 |
. . . . . . . . . . . 12
|
4 | | mdetrsca.i |
. . . . . . . . . . . . . . 15
|
5 | 4 | adantr 481 |
. . . . . . . . . . . . . 14
|
6 | | snidg 4206 |
. . . . . . . . . . . . . 14
|
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . 13
|
8 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
9 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
10 | 8, 9 | symgbasf1o 17803 |
. . . . . . . . . . . . . . . 16
|
11 | 10 | adantl 482 |
. . . . . . . . . . . . . . 15
|
12 | | f1of 6137 |
. . . . . . . . . . . . . . 15
|
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . 14
|
14 | 13, 5 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
|
15 | | ovres 6800 |
. . . . . . . . . . . . 13
|
16 | 7, 14, 15 | syl2anc 693 |
. . . . . . . . . . . 12
|
17 | | opelxpi 5148 |
. . . . . . . . . . . . . . 15
|
18 | 7, 14, 17 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
19 | | snfi 8038 |
. . . . . . . . . . . . . . . 16
|
20 | | mdetrsca.x |
. . . . . . . . . . . . . . . . . . 19
|
21 | | mdetrsca.a |
. . . . . . . . . . . . . . . . . . . 20
Mat |
22 | | mdetrsca.b |
. . . . . . . . . . . . . . . . . . . 20
|
23 | 21, 22 | matrcl 20218 |
. . . . . . . . . . . . . . . . . . 19
|
24 | 20, 23 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
25 | 24 | simpld 475 |
. . . . . . . . . . . . . . . . 17
|
26 | 25 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
27 | | xpfi 8231 |
. . . . . . . . . . . . . . . 16
|
28 | 19, 26, 27 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
29 | | mdetrsca.y |
. . . . . . . . . . . . . . . 16
|
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . 15
|
31 | | mdetrsca.z |
. . . . . . . . . . . . . . . . . . 19
|
32 | | mdetrsca.k |
. . . . . . . . . . . . . . . . . . . 20
|
33 | 21, 32, 22 | matbas2i 20228 |
. . . . . . . . . . . . . . . . . . 19
|
34 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . 19
|
35 | 31, 33, 34 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
|
36 | 35 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
37 | | ffn 6045 |
. . . . . . . . . . . . . . . . 17
|
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
|
39 | 5 | snssd 4340 |
. . . . . . . . . . . . . . . . 17
|
40 | | xpss1 5228 |
. . . . . . . . . . . . . . . . 17
|
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
|
42 | | fnssres 6004 |
. . . . . . . . . . . . . . . 16
|
43 | 38, 41, 42 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
44 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
|
45 | 28, 30, 43, 44 | ofc1 6920 |
. . . . . . . . . . . . . 14
|
46 | 18, 45 | mpdan 702 |
. . . . . . . . . . . . 13
|
47 | | df-ov 6653 |
. . . . . . . . . . . . 13
|
48 | | df-ov 6653 |
. . . . . . . . . . . . . 14
|
49 | 48 | oveq2i 6661 |
. . . . . . . . . . . . 13
|
50 | 46, 47, 49 | 3eqtr4g 2681 |
. . . . . . . . . . . 12
|
51 | 3, 16, 50 | 3eqtr3d 2664 |
. . . . . . . . . . 11
|
52 | | ovres 6800 |
. . . . . . . . . . . . 13
|
53 | 7, 14, 52 | syl2anc 693 |
. . . . . . . . . . . 12
|
54 | 53 | oveq2d 6666 |
. . . . . . . . . . 11
|
55 | 51, 54 | eqtrd 2656 |
. . . . . . . . . 10
|
56 | 55 | oveq1d 6665 |
. . . . . . . . 9
mulGrp g mulGrp g |
57 | | mdetrsca.r |
. . . . . . . . . . . 12
|
58 | | crngring 18558 |
. . . . . . . . . . . 12
|
59 | 57, 58 | syl 17 |
. . . . . . . . . . 11
|
60 | 59 | adantr 481 |
. . . . . . . . . 10
|
61 | 36, 5, 14 | fovrnd 6806 |
. . . . . . . . . 10
|
62 | | eqid 2622 |
. . . . . . . . . . . 12
mulGrp mulGrp |
63 | 62, 32 | mgpbas 18495 |
. . . . . . . . . . 11
mulGrp |
64 | 62 | crngmgp 18555 |
. . . . . . . . . . . . 13
mulGrp
CMnd |
65 | 57, 64 | syl 17 |
. . . . . . . . . . . 12
mulGrp CMnd |
66 | 65 | adantr 481 |
. . . . . . . . . . 11
mulGrp CMnd |
67 | | difssd 3738 |
. . . . . . . . . . . 12
|
68 | | ssfi 8180 |
. . . . . . . . . . . 12
|
69 | 26, 67, 68 | syl2anc 693 |
. . . . . . . . . . 11
|
70 | | eldifi 3732 |
. . . . . . . . . . . . 13
|
71 | 35 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
72 | | simpr 477 |
. . . . . . . . . . . . . 14
|
73 | 13 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
|
74 | 71, 72, 73 | fovrnd 6806 |
. . . . . . . . . . . . 13
|
75 | 70, 74 | sylan2 491 |
. . . . . . . . . . . 12
|
76 | 75 | ralrimiva 2966 |
. . . . . . . . . . 11
|
77 | 63, 66, 69, 76 | gsummptcl 18366 |
. . . . . . . . . 10
mulGrp g |
78 | | mdetrsca.t |
. . . . . . . . . . 11
|
79 | 32, 78 | ringass 18564 |
. . . . . . . . . 10
mulGrp g mulGrp g mulGrp g |
80 | 60, 30, 61, 77, 79 | syl13anc 1328 |
. . . . . . . . 9
mulGrp g mulGrp g |
81 | 56, 80 | eqtrd 2656 |
. . . . . . . 8
mulGrp g mulGrp g |
82 | 62, 78 | mgpplusg 18493 |
. . . . . . . . . 10
mulGrp |
83 | 21, 32, 22 | matbas2i 20228 |
. . . . . . . . . . . . 13
|
84 | | elmapi 7879 |
. . . . . . . . . . . . 13
|
85 | 20, 83, 84 | 3syl 18 |
. . . . . . . . . . . 12
|
86 | 85 | ad2antrr 762 |
. . . . . . . . . . 11
|
87 | 86, 72, 73 | fovrnd 6806 |
. . . . . . . . . 10
|
88 | | disjdif 4040 |
. . . . . . . . . . 11
|
89 | 88 | a1i 11 |
. . . . . . . . . 10
|
90 | | undif 4049 |
. . . . . . . . . . . 12
|
91 | 39, 90 | sylib 208 |
. . . . . . . . . . 11
|
92 | 91 | eqcomd 2628 |
. . . . . . . . . 10
|
93 | 63, 82, 66, 26, 87, 89, 92 | gsummptfidmsplit 18330 |
. . . . . . . . 9
mulGrp g mulGrp g mulGrp g |
94 | | cmnmnd 18208 |
. . . . . . . . . . . 12
mulGrp CMnd mulGrp |
95 | 66, 94 | syl 17 |
. . . . . . . . . . 11
mulGrp |
96 | 85 | adantr 481 |
. . . . . . . . . . . 12
|
97 | 96, 5, 14 | fovrnd 6806 |
. . . . . . . . . . 11
|
98 | | id 22 |
. . . . . . . . . . . . 13
|
99 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
100 | 98, 99 | oveq12d 6668 |
. . . . . . . . . . . 12
|
101 | 63, 100 | gsumsn 18354 |
. . . . . . . . . . 11
mulGrp mulGrp g |
102 | 95, 5, 97, 101 | syl3anc 1326 |
. . . . . . . . . 10
mulGrp g |
103 | | mdetrsca.ne |
. . . . . . . . . . . . . . 15
|
104 | 103 | oveqd 6667 |
. . . . . . . . . . . . . 14
|
105 | 104 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
106 | | simpr 477 |
. . . . . . . . . . . . . 14
|
107 | 70, 73 | sylan2 491 |
. . . . . . . . . . . . . 14
|
108 | | ovres 6800 |
. . . . . . . . . . . . . 14
|
109 | 106, 107,
108 | syl2anc 693 |
. . . . . . . . . . . . 13
|
110 | | ovres 6800 |
. . . . . . . . . . . . . 14
|
111 | 106, 107,
110 | syl2anc 693 |
. . . . . . . . . . . . 13
|
112 | 105, 109,
111 | 3eqtr3d 2664 |
. . . . . . . . . . . 12
|
113 | 112 | mpteq2dva 4744 |
. . . . . . . . . . 11
|
114 | 113 | oveq2d 6666 |
. . . . . . . . . 10
mulGrp g mulGrp g |
115 | 102, 114 | oveq12d 6668 |
. . . . . . . . 9
mulGrp g mulGrp g mulGrp g |
116 | 93, 115 | eqtrd 2656 |
. . . . . . . 8
mulGrp g mulGrp g |
117 | 63, 82, 66, 26, 74, 89, 92 | gsummptfidmsplit 18330 |
. . . . . . . . . 10
mulGrp g mulGrp g mulGrp g |
118 | 98, 99 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
119 | 63, 118 | gsumsn 18354 |
. . . . . . . . . . . 12
mulGrp mulGrp g |
120 | 95, 5, 61, 119 | syl3anc 1326 |
. . . . . . . . . . 11
mulGrp g |
121 | 120 | oveq1d 6665 |
. . . . . . . . . 10
mulGrp g mulGrp g mulGrp g |
122 | 117, 121 | eqtrd 2656 |
. . . . . . . . 9
mulGrp g mulGrp g |
123 | 122 | oveq2d 6666 |
. . . . . . . 8
mulGrp g mulGrp g |
124 | 81, 116, 123 | 3eqtr4d 2666 |
. . . . . . 7
mulGrp g mulGrp g |
125 | 124 | oveq2d 6666 |
. . . . . 6
RHom pmSgn mulGrp g RHom pmSgn mulGrp g |
126 | 57 | adantr 481 |
. . . . . . . . 9
|
127 | | zrhpsgnmhm 19930 |
. . . . . . . . . . . 12
RHom pmSgn MndHom mulGrp |
128 | 59, 25, 127 | syl2anc 693 |
. . . . . . . . . . 11
RHom pmSgn MndHom mulGrp |
129 | 9, 63 | mhmf 17340 |
. . . . . . . . . . 11
RHom pmSgn MndHom mulGrp
RHom pmSgn |
130 | 128, 129 | syl 17 |
. . . . . . . . . 10
RHom pmSgn |
131 | 130 | ffvelrnda 6359 |
. . . . . . . . 9
RHom pmSgn |
132 | 32, 78 | crngcom 18562 |
. . . . . . . . 9
RHom pmSgn
RHom pmSgn RHom pmSgn |
133 | 126, 131,
30, 132 | syl3anc 1326 |
. . . . . . . 8
RHom pmSgn RHom pmSgn |
134 | 133 | oveq1d 6665 |
. . . . . . 7
RHom pmSgn
mulGrp g RHom pmSgn
mulGrp g |
135 | 74 | ralrimiva 2966 |
. . . . . . . . 9
|
136 | 63, 66, 26, 135 | gsummptcl 18366 |
. . . . . . . 8
mulGrp g |
137 | 32, 78 | ringass 18564 |
. . . . . . . 8
RHom pmSgn
mulGrp g RHom pmSgn
mulGrp g RHom pmSgn mulGrp g |
138 | 60, 131, 30, 136, 137 | syl13anc 1328 |
. . . . . . 7
RHom pmSgn
mulGrp g RHom pmSgn mulGrp g |
139 | 32, 78 | ringass 18564 |
. . . . . . . 8
RHom pmSgn mulGrp g RHom pmSgn mulGrp g RHom pmSgn mulGrp g |
140 | 60, 30, 131, 136, 139 | syl13anc 1328 |
. . . . . . 7
RHom pmSgn
mulGrp g RHom pmSgn mulGrp g |
141 | 134, 138,
140 | 3eqtr3d 2664 |
. . . . . 6
RHom pmSgn mulGrp g RHom pmSgn mulGrp g |
142 | 125, 141 | eqtrd 2656 |
. . . . 5
RHom pmSgn mulGrp g RHom pmSgn mulGrp g |
143 | 142 | mpteq2dva 4744 |
. . . 4
RHom pmSgn mulGrp g RHom pmSgn mulGrp g |
144 | 143 | oveq2d 6666 |
. . 3
g RHom pmSgn mulGrp g g
RHom pmSgn mulGrp g |
145 | | eqid 2622 |
. . . 4
|
146 | | eqid 2622 |
. . . 4
|
147 | 8, 9 | symgbasfi 17806 |
. . . . 5
|
148 | 25, 147 | syl 17 |
. . . 4
|
149 | 32, 78 | ringcl 18561 |
. . . . 5
RHom pmSgn mulGrp g RHom pmSgn mulGrp g |
150 | 60, 131, 136, 149 | syl3anc 1326 |
. . . 4
RHom pmSgn mulGrp g |
151 | | eqid 2622 |
. . . . 5
RHom pmSgn mulGrp g RHom pmSgn mulGrp g |
152 | | ovexd 6680 |
. . . . 5
RHom pmSgn mulGrp g |
153 | | fvexd 6203 |
. . . . 5
|
154 | 151, 148,
152, 153 | fsuppmptdm 8286 |
. . . 4
RHom pmSgn mulGrp g finSupp |
155 | 32, 145, 146, 78, 59, 148, 29, 150, 154 | gsummulc2 18607 |
. . 3
g RHom pmSgn mulGrp g g
RHom pmSgn mulGrp g |
156 | 144, 155 | eqtrd 2656 |
. 2
g RHom pmSgn mulGrp g g RHom pmSgn mulGrp g |
157 | | mdetrsca.d |
. . . 4
maDet |
158 | | eqid 2622 |
. . . 4
RHom RHom |
159 | | eqid 2622 |
. . . 4
pmSgn pmSgn |
160 | 157, 21, 22, 9, 158, 159, 78, 62 | mdetleib2 20394 |
. . 3
g RHom pmSgn mulGrp g |
161 | 57, 20, 160 | syl2anc 693 |
. 2
g
RHom pmSgn mulGrp g |
162 | 157, 21, 22, 9, 158, 159, 78, 62 | mdetleib2 20394 |
. . . 4
g RHom pmSgn mulGrp g |
163 | 57, 31, 162 | syl2anc 693 |
. . 3
g
RHom pmSgn mulGrp g |
164 | 163 | oveq2d 6666 |
. 2
g RHom pmSgn mulGrp g |
165 | 156, 161,
164 | 3eqtr4d 2666 |
1
|