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

Theorem mp2pm2mplem4 19910
 Description: Lemma 4 for mp2pm2mp 19912. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 5-Dec-2019.)
Hypotheses
Ref Expression
mp2pm2mp.a Mat
mp2pm2mp.q Poly1
mp2pm2mp.l
mp2pm2mp.m
mp2pm2mp.e .gmulGrp
mp2pm2mp.y var1
mp2pm2mp.i g coe1
mp2pm2mplem2.p Poly1
Assertion
Ref Expression
mp2pm2mplem4 decompPMat coe1
Distinct variable groups:   ,   ,   ,,,   ,,,,   ,   ,   ,   ,   ,   ,,,   ,   ,   ,,   ,,   ,,   ,   ,,   ,,   ,,   ,,,   ,   ,   ,
Allowed substitution hints:   ()   (,,,)   (,,,)   ()

Proof of Theorem mp2pm2mplem4
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mp2pm2mp.a . . 3 Mat
2 mp2pm2mp.q . . 3 Poly1
3 mp2pm2mp.l . . 3
4 mp2pm2mp.m . . 3
5 mp2pm2mp.e . . 3 .gmulGrp
6 mp2pm2mp.y . . 3 var1
7 mp2pm2mp.i . . 3 g coe1
8 mp2pm2mplem2.p . . 3 Poly1
91, 2, 3, 4, 5, 6, 7, 8mp2pm2mplem3 19909 . 2 decompPMat coe1 g coe1
10 eqid 2471 . . . . . . . . 9
11 eqid 2471 . . . . . . . . 9
128ply1ring 18918 . . . . . . . . . . . . 13
13123ad2ant2 1052 . . . . . . . . . . . 12
14 ringcmn 17889 . . . . . . . . . . . 12 CMnd
1513, 14syl 17 . . . . . . . . . . 11 CMnd
1615ad3antrrr 744 . . . . . . . . . 10 coe1 CMnd
17163ad2ant1 1051 . . . . . . . . 9 coe1 CMnd
18 simpl2 1034 . . . . . . . . . . . . . 14
1918ad2antrr 740 . . . . . . . . . . . . 13 coe1
20193ad2ant1 1051 . . . . . . . . . . . 12 coe1
2120adantr 472 . . . . . . . . . . 11 coe1
22 eqid 2471 . . . . . . . . . . . 12
23 eqid 2471 . . . . . . . . . . . 12
24 simpl2 1034 . . . . . . . . . . . 12 coe1
25 simpl3 1035 . . . . . . . . . . . 12 coe1
26 simpl3 1035 . . . . . . . . . . . . . . 15
2726ad2antrr 740 . . . . . . . . . . . . . 14 coe1
28273ad2ant1 1051 . . . . . . . . . . . . 13 coe1
29 eqid 2471 . . . . . . . . . . . . . 14 coe1 coe1
3029, 3, 2, 23coe1fvalcl 18882 . . . . . . . . . . . . 13 coe1
3128, 30sylan 479 . . . . . . . . . . . 12 coe1 coe1
321, 22, 23, 24, 25, 31matecld 19528 . . . . . . . . . . 11 coe1 coe1
33 simpr 468 . . . . . . . . . . 11 coe1
34 eqid 2471 . . . . . . . . . . . 12 mulGrp mulGrp
3522, 8, 6, 4, 34, 5, 10ply1tmcl 18942 . . . . . . . . . . 11 coe1 coe1
3621, 32, 33, 35syl3anc 1292 . . . . . . . . . 10 coe1 coe1
3736ralrimiva 2809 . . . . . . . . 9 coe1 coe1
38 simp1lr 1094 . . . . . . . . 9 coe1
39 oveq 6314 . . . . . . . . . . . . . . . . 17 coe1 coe1
4039oveq1d 6323 . . . . . . . . . . . . . . . 16 coe1 coe1
41 3simpa 1027 . . . . . . . . . . . . . . . . . . . . . . 23
4241ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . . 22
43 eqid 2471 . . . . . . . . . . . . . . . . . . . . . . 23
441, 43mat0op 19521 . . . . . . . . . . . . . . . . . . . . . 22
4542, 44syl 17 . . . . . . . . . . . . . . . . . . . . 21
46 eqidd 2472 . . . . . . . . . . . . . . . . . . . . 21
47 simprl 772 . . . . . . . . . . . . . . . . . . . . 21
48 simprr 774 . . . . . . . . . . . . . . . . . . . . 21
49 fvex 5889 . . . . . . . . . . . . . . . . . . . . . 22
5049a1i 11 . . . . . . . . . . . . . . . . . . . . 21
5145, 46, 47, 48, 50ovmpt2d 6443 . . . . . . . . . . . . . . . . . . . 20
5251adantr 472 . . . . . . . . . . . . . . . . . . 19
5352oveq1d 6323 . . . . . . . . . . . . . . . . . 18
5418ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . 21
558ply1sca 18923 . . . . . . . . . . . . . . . . . . . . 21 Scalar
5654, 55syl 17 . . . . . . . . . . . . . . . . . . . 20 Scalar
5756fveq2d 5883 . . . . . . . . . . . . . . . . . . 19 Scalar
5857oveq1d 6323 . . . . . . . . . . . . . . . . . 18 Scalar
598ply1lmod 18922 . . . . . . . . . . . . . . . . . . . . 21
60593ad2ant2 1052 . . . . . . . . . . . . . . . . . . . 20
6160ad4antr 746 . . . . . . . . . . . . . . . . . . 19
62 simpr 468 . . . . . . . . . . . . . . . . . . . 20
638, 6, 34, 5, 10ply1moncl 18941 . . . . . . . . . . . . . . . . . . . 20
6454, 62, 63syl2anc 673 . . . . . . . . . . . . . . . . . . 19
65 eqid 2471 . . . . . . . . . . . . . . . . . . . 20 Scalar Scalar
66 eqid 2471 . . . . . . . . . . . . . . . . . . . 20 Scalar Scalar
6710, 65, 4, 66, 11lmod0vs 18202 . . . . . . . . . . . . . . . . . . 19 Scalar
6861, 64, 67syl2anc 673 . . . . . . . . . . . . . . . . . 18 Scalar
6953, 58, 683eqtrd 2509 . . . . . . . . . . . . . . . . 17
7069adantr 472 . . . . . . . . . . . . . . . 16
7140, 70sylan9eqr 2527 . . . . . . . . . . . . . . 15 coe1 coe1
7271exp31 615 . . . . . . . . . . . . . 14 coe1 coe1
7372a2d 28 . . . . . . . . . . . . 13 coe1 coe1
7473ralimdva 2805 . . . . . . . . . . . 12 coe1 coe1
7574impancom 447 . . . . . . . . . . 11 coe1 coe1
76753impib 1229 . . . . . . . . . 10 coe1 coe1
77 breq2 4399 . . . . . . . . . . . 12
78 fveq2 5879 . . . . . . . . . . . . . . 15 coe1 coe1
7978oveqd 6325 . . . . . . . . . . . . . 14 coe1 coe1
80 oveq1 6315 . . . . . . . . . . . . . 14
8179, 80oveq12d 6326 . . . . . . . . . . . . 13 coe1 coe1
8281eqeq1d 2473 . . . . . . . . . . . 12 coe1 coe1
8377, 82imbi12d 327 . . . . . . . . . . 11 coe1 coe1
8483cbvralv 3005 . . . . . . . . . 10 coe1 coe1
8576, 84sylibr 217 . . . . . . . . 9 coe1 coe1
8610, 11, 17, 37, 38, 85gsummptnn0fzv 17694 . . . . . . . 8 coe1 g coe1 g coe1
8786fveq2d 5883 . . . . . . 7 coe1 coe1 g coe1 coe1 g coe1
8887fveq1d 5881 . . . . . 6 coe1 coe1 g coe1 coe1 g coe1
89 simpllr 777 . . . . . . . 8 coe1
90893ad2ant1 1051 . . . . . . 7 coe1
91 elfznn0 11913 . . . . . . . . . 10
9236expcom 442 . . . . . . . . . 10 coe1 coe1
9391, 92syl 17 . . . . . . . . 9 coe1 coe1
9493com12 31 . . . . . . . 8 coe1 coe1
9594ralrimiv 2808 . . . . . . 7 coe1 coe1
96 fzfid 12224 . . . . . . 7 coe1
978, 10, 20, 90, 95, 96coe1fzgsumd 18973 . . . . . 6 coe1 coe1 g coe1 g coe1coe1
9888, 97eqtrd 2505 . . . . 5 coe1 coe1 g coe1 g coe1coe1
9998mpt2eq3dva 6374 . . . 4 coe1 coe1 g coe1 g coe1coe1
100183ad2ant1 1051 . . . . . . . . . . 11
101100adantr 472 . . . . . . . . . 10
102 simpl2 1034 . . . . . . . . . . 11
103 simpl3 1035 . . . . . . . . . . 11
104263ad2ant1 1051 . . . . . . . . . . . 12
105104, 91, 30syl2an 485 . . . . . . . . . . 11 coe1
1061, 22, 23, 102, 103, 105matecld 19528 . . . . . . . . . 10 coe1
10791adantl 473 . . . . . . . . . 10
10843, 22, 8, 6, 4, 34, 5coe1tm 18943 . . . . . . . . . 10 coe1 coe1coe1 coe1
109101, 106, 107, 108syl3anc 1292 . . . . . . . . 9 coe1coe1 coe1
110 eqeq1 2475 . . . . . . . . . . 11
111110ifbid 3894 . . . . . . . . . 10 coe1 coe1
112111adantl 473 . . . . . . . . 9 coe1 coe1
113 simpl1r 1082 . . . . . . . . 9
114 ovex 6336 . . . . . . . . . . 11 coe1
115114, 49ifex 3940 . . . . . . . . . 10 coe1
116115a1i 11 . . . . . . . . 9 coe1
117109, 112, 113, 116fvmptd 5969 . . . . . . . 8 coe1coe1 coe1
118117mpteq2dva 4482 . . . . . . 7 coe1coe1 coe1
119118oveq2d 6324 . . . . . 6 g coe1coe1 g coe1
120119mpt2eq3dva 6374 . . . . 5 g coe1coe1 g coe1
121120ad2antrr 740 . . . 4 coe1 g coe1coe1 g coe1
122 breq2 4399 . . . . . . . . . . . . . 14
123 fveq2 5879 . . . . . . . . . . . . . . 15 coe1 coe1
124123eqeq1d 2473 . . . . . . . . . . . . . 14 coe1 coe1
125122, 124imbi12d 327 . . . . . . . . . . . . 13 coe1 coe1
126125rspcva 3134 . . . . . . . . . . . 12 coe1 coe1
1271, 43mat0op 19521 . . . . . . . . . . . . . . . . . . . . 21
128127eqcomd 2477 . . . . . . . . . . . . . . . . . . . 20
1291283adant3 1050 . . . . . . . . . . . . . . . . . . 19
130129ad3antlr 745 . . . . . . . . . . . . . . . . . 18 coe1
131 elfz2nn0 11911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
132 nn0re 10902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
133132ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
134 nn0re 10902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
135134ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
136 nn0re 10902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
137136adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
138 lelttr 9742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
139133, 135, 137, 138syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
140 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
141140olcd 400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
142 df-ne 2643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
143132adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
144 lttri2 9734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
145136, 143, 144syl2anr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
146145adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
147142, 146syl5bbr 267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
148141, 147mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
149148ex 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
150139, 149syld 44 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
151150exp4b 618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
152151com24 89 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
153152expimpd 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
154153com23 80 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
155154imp 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1561553adant2 1049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
157131, 156sylbi 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
158157com13 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
159158adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
160159imp 436 . . . . . . . . . . . . . . . . . . . . . . . . . 26
161160adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 coe1
1621613ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . 24 coe1
163162imp 436 . . . . . . . . . . . . . . . . . . . . . . 23 coe1
164163iffalsed 3883 . . . . . . . . . . . . . . . . . . . . . 22 coe1 coe1
165164mpteq2dva 4482 . . . . . . . . . . . . . . . . . . . . 21 coe1 coe1
166165oveq2d 6324 . . . . . . . . . . . . . . . . . . . 20 coe1 g coe1 g
167 ringmnd 17867 . . . . . . . . . . . . . . . . . . . . . . . 24
1681673ad2ant2 1052 . . . . . . . . . . . . . . . . . . . . . . 23
169 ovex 6336 . . . . . . . . . . . . . . . . . . . . . . 23
17043gsumz 16699 . . . . . . . . . . . . . . . . . . . . . . 23 g
171168, 169, 170sylancl 675 . . . . . . . . . . . . . . . . . . . . . 22 g
172171ad3antlr 745 . . . . . . . . . . . . . . . . . . . . 21 coe1 g
1731723ad2ant1 1051 . . . . . . . . . . . . . . . . . . . 20 coe1 g
174166, 173eqtrd 2505 . . . . . . . . . . . . . . . . . . 19 coe1 g coe1
175174mpt2eq3dva 6374 . . . . . . . . . . . . . . . . . 18 coe1 g coe1
176 simpr 468 . . . . . . . . . . . . . . . . . 18 coe1 coe1
177130, 175, 1763eqtr4d 2515 . . . . . . . . . . . . . . . . 17 coe1 g coe1 coe1
178177ex 441 . . . . . . . . . . . . . . . 16 coe1 g coe1 coe1
179178expr 626 . . . . . . . . . . . . . . 15 coe1 g coe1 coe1
180179a2d 28 . . . . . . . . . . . . . 14 coe1 g coe1 coe1
181180exp31 615 . . . . . . . . . . . . 13 coe1 g coe1 coe1
182181com14 90 . . . . . . . . . . . 12 coe1 g coe1 coe1
183126, 182syl 17 . . . . . . . . . . 11 coe1 g coe1 coe1
184183ex 441 . . . . . . . . . 10 coe1 g coe1 coe1
185184com25 93 . . . . . . . . 9 coe1 g coe1 coe1
186185pm2.43i 48 . . . . . . . 8 coe1 g coe1 coe1
187186impcom 437 . . . . . . 7 coe1 g coe1 coe1
188187imp31 439 . . . . . 6 coe1 g coe1 coe1
189188com12 31 . . . . 5 coe1 g coe1 coe1
190168ad3antrrr 744 . . . . . . . . . . 11 coe1
191190adantl 473 . . . . . . . . . 10 coe1
1921913ad2ant1 1051 . . . . . . . . 9 coe1
193169a1i 11 . . . . . . . . 9 coe1
194 lenlt 9730 . . . . . . . . . . . . . . 15
195136, 134, 194syl2an 485 . . . . . . . . . . . . . 14
196 simpll 768 . . . . . . . . . . . . . . . 16
197 simplr 770 . . . . . . . . . . . . . . . 16
198 simpr 468 . . . . . . . . . . . . . . . 16
199 elfz2nn0 11911 . . . . . . . . . . . . . . . 16
200196, 197, 198, 199syl3anbrc 1214 . . . . . . . . . . . . . . 15
201200ex 441 . . . . . . . . . . . . . 14
202195, 201sylbird 243 . . . . . . . . . . . . 13
203202adantll 728 . . . . . . . . . . . 12
204203adantr 472 . . . . . . . . . . 11 coe1
205204impcom 437 . . . . . . . . . 10 coe1
2062053ad2ant1 1051 . . . . . . . . 9 coe1
207 eqcom 2478 . . . . . . . . . . 11
208 ifbi 3893 . . . . . . . . . . 11 coe1 coe1
209207, 208ax-mp 5 . . . . . . . . . 10 coe1 coe1
210209mpteq2i 4479 . . . . . . . . 9 coe1 coe1
211 simpl2 1034 . . . . . . . . . . . 12 coe1
212 simpl3 1035 . . . . . . . . . . . 12 coe1
21327adantl 473 . . . . . . . . . . . . . 14 coe1
2142133ad2ant1 1051 . . . . . . . . . . . . 13 coe1
215214, 30sylan 479 . . . . . . . . . . . 12 coe1 coe1
2161, 22, 23, 211, 212, 215matecld 19528 . . . . . . . . . . 11 coe1 coe1
21791, 216sylan2 482 . . . . . . . . . 10 coe1 coe1
218217ralrimiva 2809 . . . . . . . . 9 coe1 coe1
21943, 192, 193, 206, 210, 218gsummpt1n0 17675 . . . . . . . 8 coe1 g coe1 coe1
220219mpt2eq3dva 6374 . . . . . . 7 coe1 g coe1 coe1
221 csbov 6343 . . . . . . . . . . . . . . 15 coe1 coe1
222 csbfv 5916 . . . . . . . . . . . . . . . . 17 coe1 coe1
223222a1i 11 . . . . . . . . . . . . . . . 16 coe1 coe1
224223oveqd 6325 . . . . . . . . . . . . . . 15 coe1 coe1
225221, 224syl5eq 2517 . . . . . . . . . . . . . 14 coe1 coe1
226225ad2antlr 741 . . . . . . . . . . . . 13 coe1 coe1
227226mpt2eq3dv 6376 . . . . . . . . . . . 12 coe1 coe1
228 oveq12 6317 . . . . . . . . . . . . 13 coe1 coe1
229228adantl 473 . . . . . . . . . . . 12 coe1 coe1
230 simprl 772 . . . . . . . . . . . 12
231 simprr 774 . . . . . . . . . . . 12
232 ovex 6336 . . . . . . . . . . . . 13 coe1
233232a1i 11 . . . . . . . . . . . 12 coe1
234227, 229, 230, 231, 233ovmpt2d 6443 . . . . . . . . . . 11 coe1 coe1
235234ralrimivva 2814 . . . . . . . . . 10 coe1 coe1
236 simpl1 1033 . . . . . . . . . . . 12
237222oveqi 6321 . . . . . . . . . . . . . 14 coe1 coe1
238221, 237eqtri 2493 . . . . . . . . . . . . 13 coe1 coe1
239 simp2 1031 . . . . . . . . . . . . . 14
240 simp3 1032 . . . . . . . . . . . . . 14
24129, 3, 2, 23coe1fvalcl 18882 . . . . . . . . . . . . . . . 16 coe1
2422413ad2antl3 1194 . . . . . . . . . . . . . . 15 coe1
2432423ad2ant1 1051 . . . . . . . . . . . . . 14 coe1
2441, 22, 23, 239, 240, 243matecld 19528 . . . . . . . . . . . . 13 coe1
245238, 244syl5eqel 2553 . . . . . . . . . . . 12 coe1
2461, 22, 23, 236, 18, 245matbas2d 19525 . . . . . . . . . . 11 coe1
2471, 23eqmat 19526 . . . . . . . . . . 11 coe1 coe1 coe1 coe1 coe1 coe1
248246, 242, 247syl2anc 673 . . . . . . . . . 10 coe1 coe1 coe1 coe1
249235, 248mpbird 240 . . . . . . . . 9 coe1 coe1
250249ad2antrr 740 . . . . . . . 8 coe1 coe1 coe1
251250adantl 473 . . . . . . 7 coe1 coe1 coe1
252220, 251eqtrd 2505 . . . . . 6 coe1 g coe1 coe1
253252ex 441 . . . . 5 coe1 g coe1 coe1
254189, 253pm2.61i 169 . . . 4 coe1 g coe1 coe1
25599, 121, 2543eqtrd 2509 . . 3 coe1 coe1 g coe1 coe1
256 eqid 2471 . . . . . 6
25729, 3, 2, 256coe1sfi 18883 . . . . 5 coe1 finSupp
25826, 257syl 17 . . . 4 coe1 finSupp
25929, 3, 2, 256, 23coe1fsupp 18884 . . . . . 6 coe1 finSupp
260 elrabi 3181 . . . . . 6 coe1 finSupp coe1
26126, 259, 2603syl 18 . . . . 5 coe1
262 fvex 5889 . . . . 5
263 fsuppmapnn0ub 12245 . . . . 5 coe1 coe1 finSupp coe1
264261, 262, 263sylancl 675 . . . 4 coe1 finSupp coe1
265258, 264mpd 15 . . 3 coe1
266255, 265r19.29a 2918 . 2 coe1 g coe1 coe1
2679, 266eqtrd 2505 1 decompPMat coe1
 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  crab 2760  cvv 3031  csb 3349  cif 3872   class class class wbr 4395   cmpt 4454  cfv 5589  (class class class)co 6308   cmpt2 6310   cmap 7490  cfn 7587   finSupp cfsupp 7901  cr 9556  cc0 9557   clt 9693   cle 9694  cn0 10893  cfz 11810  cbs 15199  Scalarcsca 15271  cvsca 15272  c0g 15416   g cgsu 15417  cmnd 16613  .gcmg 16750  CMndccmn 17508  mulGrpcmgp 17801  crg 17858  clmod 18169  var1cv1 18846  Poly1cpl1 18847  coe1cco1 18848   Mat cmat 19509   decompPMat cdecpmat 19863 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 9634 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-ot 3968  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-ofr 6551  df-om 6712  df-1st 6812  df-2nd 6813  df-supp 6934  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-ixp 7541  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fsupp 7902  df-sup 7974  df-oi 8043  df-card 8391  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-nn 10632  df-2 10690  df-3 10691  df-4 10692  df-5 10693  df-6 10694  df-7 10695  df-8 10696  df-9 10697  df-10 10698  df-n0 10894  df-z 10962  df-dec 11075  df-uz 11183  df-fz 11811  df-fzo 11943  df-seq 12252  df-hash 12554  df-struct 15201  df-ndx 15202  df-slot 15203  df-base 15204  df-sets 15205  df-ress 15206  df-plusg 15281  df-mulr 15282  df-sca 15284  df-vsca 15285  df-ip 15286  df-tset 15287  df-ple 15288  df-ds 15290  df-hom 15292  df-cco 15293  df-0g 15418  df-gsum 15419  df-prds 15424  df-pws 15426  df-mre 15570  df-mrc 15571  df-acs 15573  df-mgm 16566  df-sgrp 16605  df-mnd 16615  df-mhm 16660  df-submnd 16661  df-grp 16751  df-minusg 16752  df-sbg 16753  df-mulg 16754  df-subg 16892  df-ghm 16959  df-cntz 17049  df-cmn 17510  df-abl 17511  df-mgp 17802  df-ur 17814  df-ring 17860  df-subrg 18084  df-lmod 18171  df-lss 18234  df-sra 18473  df-rgmod 18474  df-psr 18657  df-mvr 18658  df-mpl 18659  df-opsr 18661  df-psr1 18850  df-vr1 18851  df-ply1 18852  df-coe1 18853  df-dsmm 19372  df-frlm 19387  df-mat 19510  df-decpmat 19864 This theorem is referenced by:  mp2pm2mplem5  19911  mp2pm2mp  19912
 Copyright terms: Public domain W3C validator