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

Theorem mpfind 19481
 Description: Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 19-Mar-2015.)
Hypotheses
Ref Expression
mpfind.cb
mpfind.cp
mpfind.ct
mpfind.cq evalSub
mpfind.mu
mpfind.wa
mpfind.wb
mpfind.wc
mpfind.wd
mpfind.we
mpfind.wf
mpfind.wg
mpfind.co
mpfind.pr
mpfind.a
Assertion
Ref Expression
mpfind
Distinct variable groups:   ,   ,   ,,   ,,   ,   ,   ,   ,   ,   ,   ,,,   ,,,   ,,,   ,,   ,,   ,,   ,,,
Allowed substitution hints:   ()   ()   (,)   (,)   (,)   (,)   (,)   (,)   (,)   (,)   ()   ()   ()

Proof of Theorem mpfind
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mpfind.a . . . . 5
2 mpfind.cq . . . . 5 evalSub
31, 2syl6eleq 2406 . . . 4 evalSub
42mpfrcl 19455 . . . . . . . . 9 SubRing
51, 4syl 15 . . . . . . . 8 SubRing
6 eqid 2316 . . . . . . . . 9 evalSub evalSub
7 eqid 2316 . . . . . . . . 9 mPoly s mPoly s
8 eqid 2316 . . . . . . . . 9 s s
9 eqid 2316 . . . . . . . . 9 s s
10 mpfind.cb . . . . . . . . 9
116, 7, 8, 9, 10evlsrhm 19458 . . . . . . . 8 SubRing evalSub mPoly s RingHom s
125, 11syl 15 . . . . . . 7 evalSub mPoly s RingHom s
13 eqid 2316 . . . . . . . 8 mPoly s mPoly s
14 eqid 2316 . . . . . . . 8 s s
1513, 14rhmf 15553 . . . . . . 7 evalSub mPoly s RingHom s evalSub mPoly s s
1612, 15syl 15 . . . . . 6 evalSub mPoly s s
17 ffn 5427 . . . . . 6 evalSub mPoly s s evalSub mPoly s
1816, 17syl 15 . . . . 5 evalSub mPoly s
19 fvelrnb 5608 . . . . 5 evalSub mPoly s evalSub mPoly s evalSub
2018, 19syl 15 . . . 4 evalSub mPoly s evalSub
213, 20mpbid 201 . . 3 mPoly s evalSub
22 ffun 5429 . . . . . . . 8 evalSub mPoly s s evalSub
2316, 22syl 15 . . . . . . 7 evalSub
2423adantr 451 . . . . . 6 mPoly s evalSub
25 eqid 2316 . . . . . . 7 s s
26 eqid 2316 . . . . . . 7 mVar s mVar s
27 eqid 2316 . . . . . . 7 mPoly s mPoly s
28 eqid 2316 . . . . . . 7 mPoly s mPoly s
29 eqid 2316 . . . . . . 7 algSc mPoly s algSc mPoly s
305simp1d 967 . . . . . . . . . . . 12
315simp2d 968 . . . . . . . . . . . . . 14
325simp3d 969 . . . . . . . . . . . . . 14 SubRing
338subrgcrng 15598 . . . . . . . . . . . . . 14 SubRing s
3431, 32, 33syl2anc 642 . . . . . . . . . . . . 13 s
35 crngrng 15400 . . . . . . . . . . . . 13 s s
3634, 35syl 15 . . . . . . . . . . . 12 s
377mplrng 16245 . . . . . . . . . . . 12 s mPoly s
3830, 36, 37syl2anc 642 . . . . . . . . . . 11 mPoly s
3938adantr 451 . . . . . . . . . 10 evalSub evalSub mPoly s
40 simprl 732 . . . . . . . . . . . 12 evalSub evalSub evalSub
41 elpreima 5683 . . . . . . . . . . . . . 14 evalSub mPoly s evalSub mPoly s evalSub
4218, 41syl 15 . . . . . . . . . . . . 13 evalSub mPoly s evalSub
4342adantr 451 . . . . . . . . . . . 12 evalSub evalSub evalSub mPoly s evalSub
4440, 43mpbid 201 . . . . . . . . . . 11 evalSub evalSub mPoly s evalSub
4544simpld 445 . . . . . . . . . 10 evalSub evalSub mPoly s
46 simprr 733 . . . . . . . . . . . 12 evalSub evalSub evalSub
47 elpreima 5683 . . . . . . . . . . . . . 14 evalSub mPoly s evalSub mPoly s evalSub
4818, 47syl 15 . . . . . . . . . . . . 13 evalSub mPoly s evalSub
4948adantr 451 . . . . . . . . . . . 12 evalSub evalSub evalSub mPoly s evalSub
5046, 49mpbid 201 . . . . . . . . . . 11 evalSub evalSub mPoly s evalSub
5150simpld 445 . . . . . . . . . 10 evalSub evalSub mPoly s
5213, 27rngacl 15417 . . . . . . . . . 10 mPoly s mPoly s mPoly s mPoly s mPoly s
5339, 45, 51, 52syl3anc 1182 . . . . . . . . 9 evalSub evalSub mPoly s mPoly s
54 rhmghm 15552 . . . . . . . . . . . . . 14 evalSub mPoly s RingHom s evalSub mPoly s s
5512, 54syl 15 . . . . . . . . . . . . 13 evalSub mPoly s s
5655adantr 451 . . . . . . . . . . . 12 evalSub evalSub evalSub mPoly s s
57 eqid 2316 . . . . . . . . . . . . 13 s s
5813, 27, 57ghmlin 14737 . . . . . . . . . . . 12 evalSub mPoly s s mPoly s mPoly s evalSub mPoly s evalSub s evalSub
5956, 45, 51, 58syl3anc 1182 . . . . . . . . . . 11 evalSub evalSub evalSub mPoly s evalSub s evalSub
6031adantr 451 . . . . . . . . . . . 12 evalSub evalSub
61 ovex 5925 . . . . . . . . . . . . 13
6261a1i 10 . . . . . . . . . . . 12 evalSub evalSub
6316adantr 451 . . . . . . . . . . . . 13 evalSub evalSub evalSub mPoly s s
64 ffvelrn 5701 . . . . . . . . . . . . 13 evalSub mPoly s s mPoly s evalSub s
6563, 45, 64syl2anc 642 . . . . . . . . . . . 12 evalSub evalSub evalSub s
66 ffvelrn 5701 . . . . . . . . . . . . 13 evalSub mPoly s s mPoly s evalSub s
6763, 51, 66syl2anc 642 . . . . . . . . . . . 12 evalSub evalSub evalSub s
68 mpfind.cp . . . . . . . . . . . 12
699, 14, 60, 62, 65, 67, 68, 57pwsplusgval 13438 . . . . . . . . . . 11 evalSub evalSub evalSub s evalSub evalSub evalSub
7059, 69eqtrd 2348 . . . . . . . . . 10 evalSub evalSub evalSub mPoly s evalSub evalSub
71 simpl 443 . . . . . . . . . . 11 evalSub evalSub
7218adantr 451 . . . . . . . . . . . . . 14 evalSub evalSub evalSub mPoly s
73 fnfvelrn 5700 . . . . . . . . . . . . . 14 evalSub mPoly s mPoly s evalSub evalSub
7472, 45, 73syl2anc 642 . . . . . . . . . . . . 13 evalSub evalSub evalSub evalSub
7574, 2syl6eleqr 2407 . . . . . . . . . . . 12 evalSub evalSub evalSub
7623adantr 451 . . . . . . . . . . . . 13 evalSub evalSub evalSub
77 fvimacnvi 5677 . . . . . . . . . . . . 13 evalSub evalSub evalSub
7876, 40, 77syl2anc 642 . . . . . . . . . . . 12 evalSub evalSub evalSub
7975, 78jca 518 . . . . . . . . . . 11 evalSub evalSub evalSub evalSub
80 fnfvelrn 5700 . . . . . . . . . . . . . 14 evalSub mPoly s mPoly s evalSub evalSub
8172, 51, 80syl2anc 642 . . . . . . . . . . . . 13 evalSub evalSub evalSub evalSub
8281, 2syl6eleqr 2407 . . . . . . . . . . . 12 evalSub evalSub evalSub
83 fvimacnvi 5677 . . . . . . . . . . . . 13 evalSub evalSub evalSub
8476, 46, 83syl2anc 642 . . . . . . . . . . . 12 evalSub evalSub evalSub
8582, 84jca 518 . . . . . . . . . . 11 evalSub evalSub evalSub evalSub
86 fvex 5577 . . . . . . . . . . . 12 evalSub
87 fvex 5577 . . . . . . . . . . . 12 evalSub
88 eleq1 2376 . . . . . . . . . . . . . . . 16 evalSub evalSub
89 vex 2825 . . . . . . . . . . . . . . . . . 18
90 mpfind.wc . . . . . . . . . . . . . . . . . 18
9189, 90elab 2948 . . . . . . . . . . . . . . . . 17
92 eleq1 2376 . . . . . . . . . . . . . . . . 17 evalSub evalSub
9391, 92syl5bbr 250 . . . . . . . . . . . . . . . 16 evalSub evalSub
9488, 93anbi12d 691 . . . . . . . . . . . . . . 15 evalSub evalSub evalSub
95 eleq1 2376 . . . . . . . . . . . . . . . 16 evalSub evalSub
96 vex 2825 . . . . . . . . . . . . . . . . . 18
97 mpfind.wd . . . . . . . . . . . . . . . . . 18
9896, 97elab 2948 . . . . . . . . . . . . . . . . 17
99 eleq1 2376 . . . . . . . . . . . . . . . . 17 evalSub evalSub
10098, 99syl5bbr 250 . . . . . . . . . . . . . . . 16 evalSub evalSub
10195, 100anbi12d 691 . . . . . . . . . . . . . . 15 evalSub evalSub evalSub
10294, 101bi2anan9 843 . . . . . . . . . . . . . 14 evalSub evalSub evalSub evalSub evalSub evalSub
103102anbi2d 684 . . . . . . . . . . . . 13 evalSub evalSub evalSub evalSub evalSub evalSub
104 ovex 5925 . . . . . . . . . . . . . . 15
105 mpfind.we . . . . . . . . . . . . . . 15
106104, 105elab 2948 . . . . . . . . . . . . . 14
107 oveq12 5909 . . . . . . . . . . . . . . 15 evalSub evalSub evalSub evalSub
108107eleq1d 2382 . . . . . . . . . . . . . 14 evalSub evalSub evalSub evalSub
109106, 108syl5bbr 250 . . . . . . . . . . . . 13 evalSub evalSub evalSub evalSub
110103, 109imbi12d 311 . . . . . . . . . . . 12 evalSub evalSub evalSub evalSub evalSub evalSub evalSub evalSub
111 mpfind.ad . . . . . . . . . . . 12
11286, 87, 110, 111vtocl2 2873 . . . . . . . . . . 11 evalSub evalSub evalSub evalSub evalSub evalSub
11371, 79, 85, 112syl12anc 1180 . . . . . . . . . 10 evalSub evalSub evalSub evalSub
11470, 113eqeltrd 2390 . . . . . . . . 9 evalSub evalSub evalSub mPoly s
115 elpreima 5683 . . . . . . . . . . 11 evalSub mPoly s mPoly s evalSub mPoly s mPoly s evalSub mPoly s
11618, 115syl 15 . . . . . . . . . 10 mPoly s evalSub mPoly s mPoly s evalSub mPoly s
117116adantr 451 . . . . . . . . 9 evalSub evalSub mPoly s evalSub mPoly s mPoly s evalSub mPoly s
11853, 114, 117mpbir2and 888 . . . . . . . 8 evalSub evalSub mPoly s evalSub
119118adantlr 695 . . . . . . 7 mPoly s evalSub evalSub mPoly s evalSub
12013, 28rngcl 15403 . . . . . . . . . 10 mPoly s mPoly s mPoly s mPoly s mPoly s
12139, 45, 51, 120syl3anc 1182 . . . . . . . . 9 evalSub evalSub mPoly s mPoly s
122 eqid 2316 . . . . . . . . . . . . . . 15 mulGrp mPoly s mulGrp mPoly s
123 eqid 2316 . . . . . . . . . . . . . . 15 mulGrp s mulGrp s
124122, 123rhmmhm 15551 . . . . . . . . . . . . . 14 evalSub mPoly s RingHom s evalSub mulGrp mPoly s MndHom mulGrp s
12512, 124syl 15 . . . . . . . . . . . . 13 evalSub mulGrp mPoly s MndHom mulGrp s
126125adantr 451 . . . . . . . . . . . 12 evalSub evalSub evalSub mulGrp mPoly s MndHom mulGrp s
127122, 13mgpbas 15380 . . . . . . . . . . . . 13 mPoly s mulGrp mPoly s
128122, 28mgpplusg 15378 . . . . . . . . . . . . 13 mPoly s mulGrp mPoly s
129 eqid 2316 . . . . . . . . . . . . . 14 s s
130123, 129mgpplusg 15378 . . . . . . . . . . . . 13 s mulGrp s
131127, 128, 130mhmlin 14471 . . . . . . . . . . . 12 evalSub mulGrp mPoly s MndHom mulGrp s mPoly s mPoly s evalSub mPoly s evalSub s evalSub
132126, 45, 51, 131syl3anc 1182 . . . . . . . . . . 11 evalSub evalSub evalSub mPoly s evalSub s evalSub
133 mpfind.ct . . . . . . . . . . . 12
1349, 14, 60, 62, 65, 67, 133, 129pwsmulrval 13439 . . . . . . . . . . 11 evalSub evalSub evalSub s evalSub evalSub evalSub
135132, 134eqtrd 2348 . . . . . . . . . 10 evalSub evalSub evalSub mPoly s evalSub evalSub
136 ovex 5925 . . . . . . . . . . . . . . 15
137 mpfind.wf . . . . . . . . . . . . . . 15
138136, 137elab 2948 . . . . . . . . . . . . . 14
139 oveq12 5909 . . . . . . . . . . . . . . 15 evalSub evalSub evalSub evalSub
140139eleq1d 2382 . . . . . . . . . . . . . 14 evalSub evalSub evalSub evalSub
141138, 140syl5bbr 250 . . . . . . . . . . . . 13 evalSub evalSub evalSub evalSub
142103, 141imbi12d 311 . . . . . . . . . . . 12 evalSub evalSub evalSub evalSub evalSub evalSub evalSub evalSub
143 mpfind.mu . . . . . . . . . . . 12
14486, 87, 142, 143vtocl2 2873 . . . . . . . . . . 11 evalSub evalSub evalSub evalSub evalSub evalSub
14571, 79, 85, 144syl12anc 1180 . . . . . . . . . 10 evalSub evalSub evalSub evalSub
146135, 145eqeltrd 2390 . . . . . . . . 9 evalSub evalSub evalSub mPoly s
147 elpreima 5683 . . . . . . . . . . 11 evalSub mPoly s mPoly s evalSub mPoly s mPoly s evalSub mPoly s
14818, 147syl 15 . . . . . . . . . 10 mPoly s evalSub mPoly s mPoly s evalSub mPoly s
149148adantr 451 . . . . . . . . 9 evalSub evalSub mPoly s evalSub mPoly s mPoly s evalSub mPoly s
150121, 146, 149mpbir2and 888 . . . . . . . 8 evalSub evalSub mPoly s evalSub
151150adantlr 695 . . . . . . 7 mPoly s evalSub evalSub mPoly s evalSub
1527mplassa 16247 . . . . . . . . . . . . . 14 s mPoly s AssAlg
15330, 34, 152syl2anc 642 . . . . . . . . . . . . 13 mPoly s AssAlg
154 eqid 2316 . . . . . . . . . . . . . 14 Scalar mPoly s Scalar mPoly s
15529, 154asclrhm 16130 . . . . . . . . . . . . 13 mPoly s AssAlg algSc mPoly s Scalar mPoly s RingHom mPoly s
156153, 155syl 15 . . . . . . . . . . . 12 algSc mPoly s Scalar mPoly s RingHom mPoly s
157 eqid 2316 . . . . . . . . . . . . 13 Scalar mPoly s Scalar mPoly s
158157, 13rhmf 15553 . . . . . . . . . . . 12 algSc mPoly s Scalar mPoly s RingHom mPoly s algSc mPoly s Scalar mPoly s mPoly s
159156, 158syl 15 . . . . . . . . . . 11 algSc mPoly s Scalar mPoly s mPoly s
160159adantr 451 . . . . . . . . . 10 s algSc mPoly s Scalar mPoly s mPoly s
1617, 30, 34mplsca 16238 . . . . . . . . . . . . 13 s Scalar mPoly s
162161fveq2d 5567 . . . . . . . . . . . 12 s Scalar mPoly s
163162eleq2d 2383 . . . . . . . . . . 11 s Scalar mPoly s
164163biimpa 470 . . . . . . . . . 10 s Scalar mPoly s
165 ffvelrn 5701 . . . . . . . . . 10 algSc mPoly s Scalar mPoly s mPoly s Scalar mPoly s algSc mPoly s mPoly s
166160, 164, 165syl2anc 642 . . . . . . . . 9 s algSc mPoly s mPoly s
16730adantr 451 . . . . . . . . . . 11 s
16831adantr 451 . . . . . . . . . . 11 s
16932adantr 451 . . . . . . . . . . 11 s SubRing
17010subrgss 15595 . . . . . . . . . . . . . . 15 SubRing
17132, 170syl 15 . . . . . . . . . . . . . 14
1728, 10ressbas2 13246 . . . . . . . . . . . . . 14 s
173171, 172syl 15 . . . . . . . . . . . . 13 s
174173eleq2d 2383 . . . . . . . . . . . 12 s
175174biimpar 471 . . . . . . . . . . 11 s
1766, 7, 8, 10, 29, 167, 168, 169, 175evlssca 19459 . . . . . . . . . 10 s evalSub algSc mPoly s
177 mpfind.co . . . . . . . . . . . . . 14
178177ralrimiva 2660 . . . . . . . . . . . . 13
179 snex 4253 . . . . . . . . . . . . . . . . 17
18061, 179xpex 4838 . . . . . . . . . . . . . . . 16
181 mpfind.wa . . . . . . . . . . . . . . . 16
182180, 181elab 2948 . . . . . . . . . . . . . . 15
183 sneq 3685 . . . . . . . . . . . . . . . . 17
184183xpeq2d 4750 . . . . . . . . . . . . . . . 16
185184eleq1d 2382 . . . . . . . . . . . . . . 15
186182, 185syl5bbr 250 . . . . . . . . . . . . . 14
187186cbvralv 2798 . . . . . . . . . . . . 13
188178, 187sylib 188 . . . . . . . . . . . 12
189188r19.21bi 2675 . . . . . . . . . . 11
190175, 189syldan 456 . . . . . . . . . 10 s
191176, 190eqeltrd 2390 . . . . . . . . 9 s evalSub algSc mPoly s
192 elpreima 5683 . . . . . . . . . . 11 evalSub mPoly s algSc mPoly s evalSub algSc mPoly s mPoly s evalSub algSc mPoly s
19318, 192syl 15 . . . . . . . . . 10 algSc mPoly s evalSub algSc mPoly s mPoly s evalSub algSc mPoly s
194193adantr 451 . . . . . . . . 9 s algSc mPoly s evalSub algSc mPoly s mPoly s evalSub algSc mPoly s
195166, 191, 194mpbir2and 888 . . . . . . . 8 s algSc mPoly s evalSub
196195adantlr 695 . . . . . . 7 mPoly s s algSc mPoly s evalSub
19730adantr 451 . . . . . . . . . 10
19836adantr 451 . . . . . . . . . 10 s
199 simpr 447 . . . . . . . . . 10
2007, 26, 13, 197, 198, 199mvrcl 16242 . . . . . . . . 9 mVar s mPoly s
20131adantr 451 . . . . . . . . . . 11
20232adantr 451 . . . . . . . . . . 11 SubRing
2036, 26, 8, 10, 197, 201, 202, 199evlsvar 19460 . . . . . . . . . 10 evalSub mVar s
204 mpfind.pr . . . . . . . . . . . . . 14
20561mptex 5787 . . . . . . . . . . . . . . 15
206 mpfind.wb . . . . . . . . . . . . . . 15
207205, 206elab 2948 . . . . . . . . . . . . . 14
208204, 207sylibr 203 . . . . . . . . . . . . 13
209208ralrimiva 2660 . . . . . . . . . . . 12
210 fveq2 5563 . . . . . . . . . . . . . . 15
211210mpteq2dv 4144 . . . . . . . . . . . . . 14
212211eleq1d 2382 . . . . . . . . . . . . 13
213212cbvralv 2798 . . . . . . . . . . . 12
214209, 213sylib 188 . . . . . . . . . . 11
215214r19.21bi 2675 . . . . . . . . . 10
216203, 215eqeltrd 2390 . . . . . . . . 9 evalSub mVar s
217 elpreima 5683 . . . . . . . . . . 11 evalSub mPoly s mVar s evalSub mVar s mPoly s evalSub mVar s
21818, 217syl 15 . . . . . . . . . 10 mVar s evalSub mVar s mPoly s evalSub mVar s
219218adantr 451 . . . . . . . . 9 mVar s evalSub mVar s mPoly s evalSub mVar s
220200, 216, 219mpbir2and 888 . . . . . . . 8 mVar s evalSub
221220adantlr 695 . . . . . . 7 mPoly s mVar s evalSub
222 simpr 447 . . . . . . 7 mPoly s mPoly s
22330adantr 451 . . . . . . 7 mPoly s
22434adantr 451 . . . . . . 7 mPoly s s
22525, 26, 7, 27, 28, 29, 13, 119, 151, 196, 221, 222, 223, 224mplind 16292 . . . . . 6 mPoly s evalSub
226 fvimacnvi 5677 . . . . . 6 evalSub evalSub evalSub
22724, 225, 226syl2anc 642 . . . . 5 mPoly s evalSub
228 eleq1 2376 . . . . 5 evalSub evalSub
229227, 228syl5ibcom 211 . . . 4 mPoly s evalSub
230229rexlimdva 2701 . . 3 mPoly s evalSub
23121, 230mpd 14 . 2
232 mpfind.wg . . . 4
233232elabg 2949 . . 3
2341, 233syl 15 . 2
235231, 234mpbid 201 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wceq 1633   wcel 1701  cab 2302  wral 2577  wrex 2578  cvv 2822   wss 3186  csn 3674   cmpt 4114   cxp 4724  ccnv 4725   crn 4727  cima 4729   wfun 5286   wfn 5287  wf 5288  cfv 5292  (class class class)co 5900   cof 6118   cmap 6815  cbs 13195   ↾s cress 13196   cplusg 13255  cmulr 13256  Scalarcsca 13258   s cpws 13396   MndHom cmhm 14462   cghm 14729  mulGrpcmgp 15374  crg 15386  ccrg 15387   RingHom crh 15543  SubRingcsubrg 15590  AssAlgcasa 16099  algSccascl 16101   mVar cmvr 16137   mPoly cmpl 16138   evalSub ces 16139 This theorem is referenced by:  pf1ind  19491  mzpmfp  25973 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-rep 4168  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-inf2 7387  ax-cnex 8838  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-mulcom 8846  ax-addass 8847  ax-mulass 8848  ax-distr 8849  ax-i2m1 8850  ax-1ne0 8851  ax-1rid 8852  ax-rnegex 8853  ax-rrecex 8854  ax-cnre 8855  ax-pre-lttri 8856  ax-pre-lttrn 8857  ax-pre-ltadd 8858  ax-pre-mulgt0 8859 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-reu 2584  df-rmo 2585  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-int 3900  df-iun 3944  df-iin 3945  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-se 4390  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-isom 5301  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-of 6120  df-ofr 6121  df-1st 6164  df-2nd 6165  df-riota 6346  df-recs 6430  df-rdg 6465  df-1o 6521  df-2o 6522  df-oadd 6525  df-er 6702  df-map 6817  df-pm 6818  df-ixp 6861  df-en 6907  df-dom 6908  df-sdom 6909  df-fin 6910  df-sup 7239  df-oi 7270  df-card 7617  df-pnf 8914  df-mnf 8915  df-xr 8916  df-ltxr 8917  df-le 8918  df-sub 9084  df-neg 9085  df-nn 9792  df-2 9849  df-3 9850  df-4 9851  df-5 9852  df-6 9853  df-7 9854  df-8 9855  df-9 9856  df-10 9857  df-n0 10013  df-z 10072  df-dec 10172  df-uz 10278  df-fz 10830  df-fzo 10918  df-seq 11094  df-hash 11385  df-struct 13197  df-ndx 13198  df-slot 13199  df-base 13200  df-sets 13201  df-ress 13202  df-plusg 13268  df-mulr 13269  df-sca 13271  df-vsca 13272  df-tset 13274  df-ple 13275  df-ds 13277  df-hom 13279  df-cco 13280  df-prds 13397  df-pws 13399  df-0g 13453  df-gsum 13454  df-mre 13537  df-mrc 13538  df-acs 13540  df-mnd 14416  df-mhm 14464  df-submnd 14465  df-grp 14538  df-minusg 14539  df-sbg 14540  df-mulg 14541  df-subg 14667  df-ghm 14730  df-cntz 14842  df-cmn 15140  df-abl 15141  df-mgp 15375  df-rng 15389  df-cring 15390  df-ur 15391  df-rnghom 15545  df-subrg 15592  df-lmod 15678  df-lss 15739  df-lsp 15778  df-assa 16102  df-asp 16103  df-ascl 16104  df-psr 16147  df-mvr 16148  df-mpl 16149  df-evls 16150
 Copyright terms: Public domain W3C validator