Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mdetunilem7 Structured version   Visualization version   Unicode version

Theorem mdetunilem7 19720
 Description: Lemma for mdetuni 19724. (Contributed by SO, 15-Jul-2018.)
Hypotheses
Ref Expression
mdetuni.a Mat
mdetuni.b
mdetuni.k
mdetuni.0g
mdetuni.1r
mdetuni.pg
mdetuni.tg
mdetuni.n
mdetuni.r
mdetuni.ff
mdetuni.al
mdetuni.li
mdetuni.sc
Assertion
Ref Expression
mdetunilem7 RHom pmSgn
Distinct variable groups:   ,,,,,,   ,,,,,,   ,,,,,,   ,,,,,,   ,,,,,,   , ,,,   ,,,,,,   ,,,,,,   ,,,,,,   ,,,,   ,,,,,,   ,,,,   ,,,,   ,,   ,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem mdetunilem7
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq1 5878 . . . . . 6
21oveq1d 6323 . . . . 5
32mpt2eq3dv 6376 . . . 4
43fveq2d 5883 . . 3
5 fveq2 5879 . . . 4 RHom pmSgn RHom pmSgn
65oveq1d 6323 . . 3 RHom pmSgn RHom pmSgn
74, 6eqeq12d 2486 . 2 RHom pmSgn RHom pmSgn
8 fveq1 5878 . . . . . 6
98oveq1d 6323 . . . . 5
109mpt2eq3dv 6376 . . . 4
1110fveq2d 5883 . . 3
12 fveq2 5879 . . . 4 RHom pmSgn RHom pmSgn
1312oveq1d 6323 . . 3 RHom pmSgn RHom pmSgn
1411, 13eqeq12d 2486 . 2 RHom pmSgn RHom pmSgn
15 fveq1 5878 . . . . . 6
1615oveq1d 6323 . . . . 5
1716mpt2eq3dv 6376 . . . 4
1817fveq2d 5883 . . 3
19 fveq2 5879 . . . 4 RHom pmSgn RHom pmSgn
2019oveq1d 6323 . . 3 RHom pmSgn RHom pmSgn
2118, 20eqeq12d 2486 . 2 RHom pmSgn RHom pmSgn
22 fveq1 5878 . . . . . 6
2322oveq1d 6323 . . . . 5
2423mpt2eq3dv 6376 . . . 4
2524fveq2d 5883 . . 3
26 fveq2 5879 . . . 4 RHom pmSgn RHom pmSgn
2726oveq1d 6323 . . 3 RHom pmSgn RHom pmSgn
2825, 27eqeq12d 2486 . 2 RHom pmSgn RHom pmSgn
29 eqid 2471 . 2
30 eqid 2471 . 2
31 eqid 2471 . 2
32 mdetuni.n . . . 4
34 eqid 2471 . . . 4
3534symggrp 17119 . . 3
36 grpmnd 16756 . . 3
3733, 35, 363syl 18 . 2
38 eqid 2471 . . . 4 pmTrsp pmTrsp
3938, 34, 31symgtrf 17188 . . 3 pmTrsp
4039a1i 11 . 2 pmTrsp
41 eqid 2471 . . . . . 6 mrClsSubMnd mrClsSubMnd
4238, 34, 31, 41symggen2 17190 . . . . 5 mrClsSubMnd pmTrsp
4332, 42syl 17 . . . 4 mrClsSubMnd pmTrsp
4443eqcomd 2477 . . 3 mrClsSubMnd pmTrsp
45443ad2ant1 1051 . 2 mrClsSubMnd pmTrsp
46 mdetuni.r . . . . 5
47463ad2ant1 1051 . . . 4
48 mdetuni.ff . . . . . 6
49483ad2ant1 1051 . . . . 5
50 simp3 1032 . . . . 5
5149, 50ffvelrnd 6038 . . . 4
52 mdetuni.k . . . . 5
53 mdetuni.tg . . . . 5
54 mdetuni.1r . . . . 5
5552, 53, 54ringlidm 17882 . . . 4
5647, 51, 55syl2anc 673 . . 3
57 zrhpsgnmhm 19229 . . . . . . 7 RHom pmSgn MndHom mulGrp
5846, 32, 57syl2anc 673 . . . . . 6 RHom pmSgn MndHom mulGrp
59 eqid 2471 . . . . . . . 8 mulGrp mulGrp
6059, 54ringidval 17815 . . . . . . 7 mulGrp
6129, 60mhm0 16668 . . . . . 6 RHom pmSgn MndHom mulGrp RHom pmSgn
6258, 61syl 17 . . . . 5 RHom pmSgn
63623ad2ant1 1051 . . . 4 RHom pmSgn
6463oveq1d 6323 . . 3 RHom pmSgn
6534symgid 17120 . . . . . . . . . . . 12
6632, 65syl 17 . . . . . . . . . . 11
67663ad2ant1 1051 . . . . . . . . . 10
68673ad2ant1 1051 . . . . . . . . 9
6968fveq1d 5881 . . . . . . . 8
70 simp2 1031 . . . . . . . . 9
71 fvresi 6106 . . . . . . . . 9
7270, 71syl 17 . . . . . . . 8
7369, 72eqtr3d 2507 . . . . . . 7
7473oveq1d 6323 . . . . . 6
7574mpt2eq3dva 6374 . . . . 5
76 mdetuni.a . . . . . . . . 9 Mat
77 mdetuni.b . . . . . . . . 9
7876, 52, 77matbas2i 19524 . . . . . . . 8
79783ad2ant3 1053 . . . . . . 7
80 elmapi 7511 . . . . . . 7
81 ffn 5739 . . . . . . 7
8279, 80, 813syl 18 . . . . . 6
83 fnov 6423 . . . . . 6
8482, 83sylib 201 . . . . 5
8575, 84eqtr4d 2508 . . . 4
8685fveq2d 5883 . . 3
8756, 64, 863eqtr4rd 2516 . 2 RHom pmSgn
88 simp2 1031 . . . . . . . . . . . 12 pmTrsp
8939sseli 3414 . . . . . . . . . . . . 13 pmTrsp
90893ad2ant3 1053 . . . . . . . . . . . 12 pmTrsp
9134, 31, 30symgov 17109 . . . . . . . . . . . 12
9288, 90, 91syl2anc 673 . . . . . . . . . . 11 pmTrsp
9392fveq1d 5881 . . . . . . . . . 10 pmTrsp
94933ad2ant1 1051 . . . . . . . . 9 pmTrsp
9534, 31symgbasf1o 17102 . . . . . . . . . . . 12
96 f1of 5828 . . . . . . . . . . . 12
9790, 95, 963syl 18 . . . . . . . . . . 11 pmTrsp
98973ad2ant1 1051 . . . . . . . . . 10 pmTrsp
99 simp2 1031 . . . . . . . . . 10 pmTrsp
100 fvco3 5957 . . . . . . . . . 10
10198, 99, 100syl2anc 673 . . . . . . . . 9 pmTrsp
10294, 101eqtrd 2505 . . . . . . . 8 pmTrsp
103102oveq1d 6323 . . . . . . 7 pmTrsp
104103mpt2eq3dva 6374 . . . . . 6 pmTrsp
105104fveq2d 5883 . . . . 5 pmTrsp
10634, 31symgbasf 17103 . . . . . 6
107 eqid 2471 . . . . . . . . 9 pmTrsp pmTrsp
108107, 38pmtrrn2 17179 . . . . . . . 8 pmTrsp pmTrsp
109 mdetuni.0g . . . . . . . . . . . . . 14
110 mdetuni.pg . . . . . . . . . . . . . 14
111 mdetuni.al . . . . . . . . . . . . . 14
112 mdetuni.li . . . . . . . . . . . . . 14
113 mdetuni.sc . . . . . . . . . . . . . 14
114 simpll1 1069 . . . . . . . . . . . . . 14
115 df-3an 1009 . . . . . . . . . . . . . . . 16
116115biimpri 211 . . . . . . . . . . . . . . 15
117116adantl 473 . . . . . . . . . . . . . 14
11879, 80syl 17 . . . . . . . . . . . . . . . . . 18
119118adantr 472 . . . . . . . . . . . . . . . . 17
120119ad2antrr 740 . . . . . . . . . . . . . . . 16
121 simpllr 777 . . . . . . . . . . . . . . . . 17
122 simprlr 781 . . . . . . . . . . . . . . . . . 18
123122adantr 472 . . . . . . . . . . . . . . . . 17
124121, 123ffvelrnd 6038 . . . . . . . . . . . . . . . 16
125 simpr 468 . . . . . . . . . . . . . . . 16
126120, 124, 125fovrnd 6460 . . . . . . . . . . . . . . 15
127 simprll 780 . . . . . . . . . . . . . . . . . 18
128127adantr 472 . . . . . . . . . . . . . . . . 17
129121, 128ffvelrnd 6038 . . . . . . . . . . . . . . . 16
130120, 129, 125fovrnd 6460 . . . . . . . . . . . . . . 15
131126, 130jca 541 . . . . . . . . . . . . . 14
132118ad2antrr 740 . . . . . . . . . . . . . . . 16
1331323ad2ant1 1051 . . . . . . . . . . . . . . 15
134 simp1lr 1094 . . . . . . . . . . . . . . . 16
135 simp2 1031 . . . . . . . . . . . . . . . 16
136134, 135ffvelrnd 6038 . . . . . . . . . . . . . . 15
137 simp3 1032 . . . . . . . . . . . . . . 15
138133, 136, 137fovrnd 6460 . . . . . . . . . . . . . 14
13976, 77, 52, 109, 54, 110, 53, 32, 46, 48, 111, 112, 113, 114, 117, 131, 138mdetunilem6 19719 . . . . . . . . . . . . 13
140 simpl1 1033 . . . . . . . . . . . . . . 15
141 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . 22 pmTrsp pmTrsp
14232adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24
143 simprll 780 . . . . . . . . . . . . . . . . . . . . . . . 24
144 simprlr 781 . . . . . . . . . . . . . . . . . . . . . . . 24
145 simprr 774 . . . . . . . . . . . . . . . . . . . . . . . 24
146107pmtrprfv 17172 . . . . . . . . . . . . . . . . . . . . . . . 24 pmTrsp
147142, 143, 144, 145, 146syl13anc 1294 . . . . . . . . . . . . . . . . . . . . . . 23 pmTrsp
148147adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 pmTrsp
149141, 148sylan9eqr 2527 . . . . . . . . . . . . . . . . . . . . 21 pmTrsp
150149fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20 pmTrsp
151150oveq1d 6323 . . . . . . . . . . . . . . . . . . 19 pmTrsp
152 iftrue 3878 . . . . . . . . . . . . . . . . . . . 20
153152adantl 473 . . . . . . . . . . . . . . . . . . 19
154151, 153eqtr4d 2508 . . . . . . . . . . . . . . . . . 18 pmTrsp
155 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . 25 pmTrsp pmTrsp
156 prcom 4041 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
157156fveq2i 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 pmTrsp pmTrsp
158157fveq1i 5880 . . . . . . . . . . . . . . . . . . . . . . . . . 26 pmTrsp pmTrsp
15932ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
160 simplrl 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
161160simprd 470 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
162160simpld 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
163 simplrr 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
164163necomd 2698 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
165107pmtrprfv 17172 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 pmTrsp
166159, 161, 162, 164, 165syl13anc 1294 . . . . . . . . . . . . . . . . . . . . . . . . . 26 pmTrsp
167158, 166syl5eq 2517 . . . . . . . . . . . . . . . . . . . . . . . . 25 pmTrsp
168155, 167sylan9eqr 2527 . . . . . . . . . . . . . . . . . . . . . . . 24 pmTrsp
169168fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . 23 pmTrsp
170169oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . 22 pmTrsp
171 iftrue 3878 . . . . . . . . . . . . . . . . . . . . . . 23
172171adantl 473 . . . . . . . . . . . . . . . . . . . . . 22
173170, 172eqtr4d 2508 . . . . . . . . . . . . . . . . . . . . 21 pmTrsp
174173adantlr 729 . . . . . . . . . . . . . . . . . . . 20 pmTrsp
175 vex 3034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
176175elpr 3977 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
177176notbii 303 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
178 ioran 498 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
179177, 178sylbbr 219 . . . . . . . . . . . . . . . . . . . . . . . . . 26
180179adantll 728 . . . . . . . . . . . . . . . . . . . . . . . . 25
181 prssi 4119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
182160, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
183 pr2ne 8454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
184160, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
185163, 184mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
186107pmtrmvd 17175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 pmTrsp
187159, 182, 185, 186syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 pmTrsp
188187eleq2d 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 pmTrsp
189188notbid 301 . . . . . . . . . . . . . . . . . . . . . . . . . 26 pmTrsp
190189ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . 25 pmTrsp
191180, 190mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . 24 pmTrsp
192107pmtrf 17174 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 pmTrsp
193159, 182, 185, 192syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 pmTrsp
194 ffn 5739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 pmTrsp pmTrsp
195193, 194syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 pmTrsp
196 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26
197 fnelnfp 6110 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 pmTrsp pmTrsp pmTrsp
198197necon2bbid 2686 . . . . . . . . . . . . . . . . . . . . . . . . . 26 pmTrsp pmTrsp pmTrsp
199195, 196, 198syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . 25 pmTrsp pmTrsp
200199ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . 24 pmTrsp pmTrsp
201191, 200mpbird 240 . . . . . . . . . . . . . . . . . . . . . . 23 pmTrsp
202201fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . 22 pmTrsp
203202oveq1d 6323 . . . . . . . . . . . . . . . . . . . . 21 pmTrsp
204 iffalse 3881 . . . . . . . . . . . . . . . . . . . . . 22
205204adantl 473 . . . . . . . . . . . . . . . . . . . . 21
206203, 205eqtr4d 2508 . . . . . . . . . . . . . . . . . . . 20 pmTrsp
207174, 206pm2.61dan 808 . . . . . . . . . . . . . . . . . . 19 pmTrsp
208 iffalse 3881 . . . . . . . . . . . . . . . . . . . 20
209208adantl 473 . . . . . . . . . . . . . . . . . . 19
210207, 209eqtr4d 2508 . . . . . . . . . . . . . . . . . 18 pmTrsp
211154, 210pm2.61dan 808 . . . . . . . . . . . . . . . . 17 pmTrsp
2122113adant3 1050 . . . . . . . . . . . . . . . 16 pmTrsp
213212mpt2eq3dva 6374 . . . . . . . . . . . . . . 15 pmTrsp
214140, 213sylan 479 . . . . . . . . . . . . . 14 pmTrsp
215214fveq2d 5883 . . . . . . . . . . . . 13 pmTrsp
216 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21
217216oveq1d 6323 . . . . . . . . . . . . . . . . . . . 20
218 iftrue 3878 . . . . . . . . . . . . . . . . . . . 20
219217, 218eqtr4d 2508 . . . . . . . . . . . . . . . . . . 19
220 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24
221220oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . 23
222 iftrue 3878 . . . . . . . . . . . . . . . . . . . . . . 23
223221, 222eqtr4d 2508 . . . . . . . . . . . . . . . . . . . . . 22
224223adantl 473 . . . . . . . . . . . . . . . . . . . . 21
225 iffalse 3881 . . . . . . . . . . . . . . . . . . . . . . 23
226225eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . 22
227226adantl 473 . . . . . . . . . . . . . . . . . . . . 21
228224, 227pm2.61dan 808 . . . . . . . . . . . . . . . . . . . 20
229 iffalse 3881 . . . . . . . . . . . . . . . . . . . 20
230228, 229eqtr4d 2508 . . . . . . . . . . . . . . . . . . 19
231219, 230pm2.61i 169 . . . . . . . . . . . . . . . . . 18
232231a1i 11 . . . . . . . . . . . . . . . . 17
233232mpt2eq3ia 6375 . . . . . . . . . . . . . . . 16
234233fveq2i 5882 . . . . . . . . . . . . . . 15
235234fveq2i 5882 . . . . . . . . . . . . . 14
236235a1i 11 . . . . . . . . . . . . 13
237139, 215, 2363eqtr4d 2515 . . . . . . . . . . . 12 pmTrsp
238 fveq1 5878 . . . . . . . . . . . . . . . . 17 pmTrsp pmTrsp
239238fveq2d 5883 . . . . . . . . . . . . . . . 16 pmTrsp pmTrsp
240239oveq1d 6323 . . . . . . . . . . . . . . 15 pmTrsp pmTrsp
241240mpt2eq3dv 6376 . . . . . . . . . . . . . 14 pmTrsp pmTrsp
242241fveq2d 5883 . . . . . . . . . . . . 13 pmTrsp pmTrsp
243242eqeq1d 2473 . . . . . . . . . . . 12 pmTrsp pmTrsp
244237, 243syl5ibrcom 230 . . . . . . . . . . 11 pmTrsp
245244expr 626 . . . . . . . . . 10 pmTrsp
246245impd 438 . . . . . . . . 9 pmTrsp
247246rexlimdvva 2878 . . . . . . . 8 pmTrsp
248108, 247syl5 32 . . . . . . 7 pmTrsp
2492483impia 1228 . . . . . 6 pmTrsp
250106, 249syl3an2 1326 . . . . 5 pmTrsp
251105, 250eqtrd 2505 . . . 4 pmTrsp
252251adantr 472 . . 3 pmTrsp RHom pmSgn
253 fveq2 5879 . . . 4 RHom pmSgn RHom pmSgn
254253adantl 473 . . 3 pmTrsp RHom pmSgn RHom pmSgn
255 eqid 2471 . . . . . 6
256473ad2ant1 1051 . . . . . 6 pmTrsp
257583ad2ant1 1051 . . . . . . . . 9 RHom pmSgn MndHom mulGrp
2582573ad2ant1 1051 . . . . . . . 8 pmTrsp RHom pmSgn MndHom mulGrp
25959, 52mgpbas 17807 . . . . . . . . 9 mulGrp
26031, 259mhmf 16665 . . . . . . . 8 RHom pmSgn MndHom mulGrp RHom pmSgn
261258, 260syl 17 . . . . . . 7 pmTrsp RHom pmSgn
262261, 88ffvelrnd 6038 . . . . . 6 pmTrsp RHom pmSgn
263493ad2ant1 1051 . . . . . . 7 pmTrsp
264 simp13 1062 . . . . . . 7 pmTrsp
265263, 264ffvelrnd 6038 . . . . . 6 pmTrsp
26652, 53, 255, 256, 262, 265ringmneg1 17902 . . . . 5 pmTrsp RHom pmSgn RHom pmSgn
26759, 53mgpplusg 17805 . . . . . . . . 9 mulGrp
26831, 30, 267mhmlin 16667 . . . . . . . 8 RHom pmSgn MndHom mulGrp RHom pmSgn RHom pmSgn RHom pmSgn
269258, 88, 90, 268syl3anc 1292 . . . . . . 7 pmTrsp RHom pmSgn RHom pmSgn RHom pmSgn
270333ad2ant1 1051 . . . . . . . . 9 pmTrsp
271 simp3 1032 . . . . . . . . . 10 pmTrsp pmTrsp
27234, 31, 38pmtrodpm 19242 . . . . . . . . . 10 pmTrsp pmEven
273270, 271, 272syl2anc 673 . . . . . . . . 9 pmTrsp pmEven
274 eqid 2471 . . . . . . . . . 10 RHom RHom
275 eqid 2471 . . . . . . . . . 10 pmSgn pmSgn
276274, 275, 54, 31, 255zrhpsgnodpm 19237 . . . . . . . . 9 pmEven RHom pmSgn
277256, 270, 273, 276syl3anc 1292 . . . . . . . 8 pmTrsp RHom pmSgn
278277oveq2d 6324 . . . . . . 7 pmTrsp RHom pmSgn RHom pmSgn RHom pmSgn
27952, 53, 54, 255, 256, 262rngnegr 17901 . . . . . . 7 pmTrsp RHom pmSgn RHom pmSgn
280269, 278, 2793eqtrrd 2510 . . . . . 6 pmTrsp RHom pmSgn RHom pmSgn
281280oveq1d 6323 . . . . 5 pmTrsp RHom pmSgn RHom pmSgn
282266, 281eqtr3d 2507 . . . 4 pmTrsp RHom pmSgn RHom pmSgn
283282adantr 472 . . 3 pmTrsp RHom pmSgn RHom pmSgn RHom pmSgn
284252, 254, 2833eqtrd 2509 . 2 pmTrsp RHom pmSgn RHom pmSgn
285 simp2 1031 . . 3
28634, 31elsymgbas 17101 . . . 4
28733, 286syl 17 . . 3
288285, 287mpbird 240 . 2
2897, 14, 21, 28, 29, 30, 31, 37, 40, 45, 87, 284, 288mrcmndind 16691 1 RHom pmSgn
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wo 375   wa 376   w3a 1007   wceq 1452   wcel 1904   wne 2641  wral 2756  wrex 2757   cdif 3387   wss 3390  cif 3872  csn 3959  cpr 3961   class class class wbr 4395   cid 4749   cxp 4837   cdm 4839   crn 4840   cres 4841   ccom 4843   wfn 5584  wf 5585  wf1o 5588  cfv 5589  (class class class)co 6308   cmpt2 6310   cof 6548  c2o 7194   cmap 7490   cen 7584  cfn 7587  cbs 15199   cplusg 15268  cmulr 15269  c0g 15416  mrClscmrc 15567  cmnd 16613   MndHom cmhm 16658  SubMndcsubmnd 16659  cgrp 16747  cminusg 16748  csymg 17096  pmTrspcpmtr 17160  pmSgncpsgn 17208  pmEvencevpm 17209  mulGrpcmgp 17801  cur 17813  crg 17858  RHomczrh 19148   Mat cmat 19509 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0