Step | Hyp | Ref
| Expression |
1 | | tru 1487 |
. . 3
|
2 | | 0fin 8188 |
. . . . . 6
|
3 | | 0ex 4790 |
. . . . . . . 8
|
4 | | mzpconst 37298 |
. . . . . . . 8
mzPoly |
5 | 3, 4 | mpan 706 |
. . . . . . 7
mzPoly |
6 | | 0ss 3972 |
. . . . . . . 8
|
7 | 6 | a1i 11 |
. . . . . . 7
|
8 | | simpr 477 |
. . . . . . . . . . 11
|
9 | | elmapssres 7882 |
. . . . . . . . . . 11
|
10 | 8, 6, 9 | sylancl 694 |
. . . . . . . . . 10
|
11 | | vex 3203 |
. . . . . . . . . . 11
|
12 | 11 | fvconst2 6469 |
. . . . . . . . . 10
|
13 | 10, 12 | syl 17 |
. . . . . . . . 9
|
14 | 13 | mpteq2dva 4744 |
. . . . . . . 8
|
15 | | fconstmpt 5163 |
. . . . . . . 8
|
16 | 14, 15 | syl6reqr 2675 |
. . . . . . 7
|
17 | | fveq1 6190 |
. . . . . . . . . . 11
|
18 | 17 | mpteq2dv 4745 |
. . . . . . . . . 10
|
19 | 18 | eqeq2d 2632 |
. . . . . . . . 9
|
20 | 19 | anbi2d 740 |
. . . . . . . 8
|
21 | 20 | rspcev 3309 |
. . . . . . 7
mzPoly
mzPoly |
22 | 5, 7, 16, 21 | syl12anc 1324 |
. . . . . 6
mzPoly |
23 | | fveq2 6191 |
. . . . . . . 8
mzPoly mzPoly |
24 | | sseq1 3626 |
. . . . . . . . 9
|
25 | | reseq2 5391 |
. . . . . . . . . . . 12
|
26 | 25 | fveq2d 6195 |
. . . . . . . . . . 11
|
27 | 26 | mpteq2dv 4745 |
. . . . . . . . . 10
|
28 | 27 | eqeq2d 2632 |
. . . . . . . . 9
|
29 | 24, 28 | anbi12d 747 |
. . . . . . . 8
|
30 | 23, 29 | rexeqbidv 3153 |
. . . . . . 7
mzPoly mzPoly |
31 | 30 | rspcev 3309 |
. . . . . 6
mzPoly mzPoly |
32 | 2, 22, 31 | sylancr 695 |
. . . . 5
mzPoly |
33 | 32 | adantl 482 |
. . . 4
mzPoly |
34 | | snfi 8038 |
. . . . . 6
|
35 | | snex 4908 |
. . . . . . . . 9
|
36 | | vsnid 4209 |
. . . . . . . . 9
|
37 | | mzpproj 37300 |
. . . . . . . . 9
mzPoly |
38 | 35, 36, 37 | mp2an 708 |
. . . . . . . 8
mzPoly |
39 | 38 | a1i 11 |
. . . . . . 7
mzPoly |
40 | | snssi 4339 |
. . . . . . 7
|
41 | | fveq1 6190 |
. . . . . . . . 9
|
42 | 41 | cbvmptv 4750 |
. . . . . . . 8
|
43 | | simpr 477 |
. . . . . . . . . . . 12
|
44 | | simpl 473 |
. . . . . . . . . . . . 13
|
45 | 44 | snssd 4340 |
. . . . . . . . . . . 12
|
46 | | elmapssres 7882 |
. . . . . . . . . . . 12
|
47 | 43, 45, 46 | syl2anc 693 |
. . . . . . . . . . 11
|
48 | | fveq1 6190 |
. . . . . . . . . . . 12
|
49 | | eqid 2622 |
. . . . . . . . . . . 12
|
50 | | fvex 6201 |
. . . . . . . . . . . 12
|
51 | 48, 49, 50 | fvmpt 6282 |
. . . . . . . . . . 11
|
52 | 47, 51 | syl 17 |
. . . . . . . . . 10
|
53 | | fvres 6207 |
. . . . . . . . . . 11
|
54 | 36, 53 | ax-mp 5 |
. . . . . . . . . 10
|
55 | 52, 54 | syl6req 2673 |
. . . . . . . . 9
|
56 | 55 | mpteq2dva 4744 |
. . . . . . . 8
|
57 | 42, 56 | syl5eq 2668 |
. . . . . . 7
|
58 | | fveq1 6190 |
. . . . . . . . . . 11
|
59 | 58 | mpteq2dv 4745 |
. . . . . . . . . 10
|
60 | 59 | eqeq2d 2632 |
. . . . . . . . 9
|
61 | 60 | anbi2d 740 |
. . . . . . . 8
|
62 | 61 | rspcev 3309 |
. . . . . . 7
mzPoly mzPoly |
63 | 39, 40, 57, 62 | syl12anc 1324 |
. . . . . 6
mzPoly |
64 | | fveq2 6191 |
. . . . . . . 8
mzPoly mzPoly |
65 | | sseq1 3626 |
. . . . . . . . 9
|
66 | | reseq2 5391 |
. . . . . . . . . . . 12
|
67 | 66 | fveq2d 6195 |
. . . . . . . . . . 11
|
68 | 67 | mpteq2dv 4745 |
. . . . . . . . . 10
|
69 | 68 | eqeq2d 2632 |
. . . . . . . . 9
|
70 | 65, 69 | anbi12d 747 |
. . . . . . . 8
|
71 | 64, 70 | rexeqbidv 3153 |
. . . . . . 7
mzPoly mzPoly |
72 | 71 | rspcev 3309 |
. . . . . 6
mzPoly mzPoly |
73 | 34, 63, 72 | sylancr 695 |
. . . . 5
mzPoly |
74 | 73 | adantl 482 |
. . . 4
mzPoly |
75 | | simplll 798 |
. . . . . . . . . . . . . . . . . 18
mzPoly
mzPoly
|
76 | | simprll 802 |
. . . . . . . . . . . . . . . . . 18
mzPoly
mzPoly |
77 | | unfi 8227 |
. . . . . . . . . . . . . . . . . 18
|
78 | 75, 76, 77 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
mzPoly
mzPoly |
79 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . 22
|
80 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . 22
|
81 | 79, 80 | unex 6956 |
. . . . . . . . . . . . . . . . . . . . 21
|
82 | 81 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly
mzPoly |
83 | | ssun1 3776 |
. . . . . . . . . . . . . . . . . . . . 21
|
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly
mzPoly |
85 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly
mzPoly mzPoly |
86 | | mzpresrename 37313 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly
mzPoly |
87 | 82, 84, 85, 86 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
mzPoly
mzPoly mzPoly
|
88 | | ssun2 3777 |
. . . . . . . . . . . . . . . . . . . . 21
|
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly
mzPoly
|
90 | | simprlr 803 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly
mzPoly mzPoly |
91 | | mzpresrename 37313 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly
mzPoly |
92 | 82, 89, 90, 91 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
mzPoly
mzPoly mzPoly
|
93 | | mzpaddmpt 37304 |
. . . . . . . . . . . . . . . . . . 19
mzPoly
mzPoly mzPoly |
94 | 87, 92, 93 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
mzPoly
mzPoly mzPoly
|
95 | | simplr 792 |
. . . . . . . . . . . . . . . . . . 19
mzPoly
mzPoly |
96 | | simprr 796 |
. . . . . . . . . . . . . . . . . . 19
mzPoly
mzPoly
|
97 | 95, 96 | unssd 3789 |
. . . . . . . . . . . . . . . . . 18
mzPoly
mzPoly
|
98 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . 21
|
99 | 98 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly
mzPoly |
100 | | mzpcompact2lem.i |
. . . . . . . . . . . . . . . . . . . . . . 23
|
101 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
mzPoly
mzPoly
|
102 | | mzpresrename 37313 |
. . . . . . . . . . . . . . . . . . . . . 22
mzPoly
mzPoly |
103 | 101, 95, 85, 102 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
mzPoly
mzPoly mzPoly |
104 | | mzpf 37299 |
. . . . . . . . . . . . . . . . . . . . 21
mzPoly
|
105 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . 21
|
106 | 103, 104,
105 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly
mzPoly |
107 | | mzpresrename 37313 |
. . . . . . . . . . . . . . . . . . . . . 22
mzPoly
mzPoly |
108 | 101, 96, 90, 107 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
mzPoly
mzPoly mzPoly |
109 | | mzpf 37299 |
. . . . . . . . . . . . . . . . . . . . 21
mzPoly
|
110 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . 21
|
111 | 108, 109,
110 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly
mzPoly |
112 | | ofmpteq 6916 |
. . . . . . . . . . . . . . . . . . . 20
|
113 | 99, 106, 111, 112 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
mzPoly
mzPoly |
114 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
115 | | fssres 6070 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
116 | 114, 97, 115 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . . . 23
mzPoly
mzPoly
|
117 | | zex 11386 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
118 | 117, 81 | elmap 7886 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
119 | 116, 118 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . 22
mzPoly
mzPoly
|
120 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
121 | 120 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
122 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
123 | 122 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
124 | 121, 123 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
125 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
126 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
127 | 124, 125,
126 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . 22
|
128 | 119, 127 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
mzPoly
mzPoly
|
129 | | resabs1 5427 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
130 | 83, 129 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
131 | 130 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . . . . . 22
|
132 | | resabs1 5427 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
133 | 88, 132 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
134 | 133 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . . . . . 22
|
135 | 131, 134 | oveq12i 6662 |
. . . . . . . . . . . . . . . . . . . . 21
|
136 | 128, 135 | syl6req 2673 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly
mzPoly
|
137 | 136 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . . . 19
mzPoly
mzPoly
|
138 | 113, 137 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
mzPoly
mzPoly
|
139 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . 22
|
140 | 139 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . 21
|
141 | 140 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . 20
|
142 | 141 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . 19
|
143 | 142 | rspcev 3309 |
. . . . . . . . . . . . . . . . . 18
mzPoly
mzPoly
|
144 | 94, 97, 138, 143 | syl12anc 1324 |
. . . . . . . . . . . . . . . . 17
mzPoly
mzPoly
mzPoly |
145 | | mzpmulmpt 37305 |
. . . . . . . . . . . . . . . . . . 19
mzPoly
mzPoly mzPoly |
146 | 87, 92, 145 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
mzPoly
mzPoly mzPoly
|
147 | | ofmpteq 6916 |
. . . . . . . . . . . . . . . . . . . 20
|
148 | 99, 106, 111, 147 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
mzPoly
mzPoly |
149 | 121, 123 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
150 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
151 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
152 | 149, 150,
151 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . 22
|
153 | 119, 152 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
mzPoly
mzPoly
|
154 | 131, 134 | oveq12i 6662 |
. . . . . . . . . . . . . . . . . . . . 21
|
155 | 153, 154 | syl6req 2673 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly
mzPoly
|
156 | 155 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . . . 19
mzPoly
mzPoly
|
157 | 148, 156 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
mzPoly
mzPoly
|
158 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . 22
|
159 | 158 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . 21
|
160 | 159 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . 20
|
161 | 160 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . 19
|
162 | 161 | rspcev 3309 |
. . . . . . . . . . . . . . . . . 18
mzPoly
mzPoly
|
163 | 146, 97, 157, 162 | syl12anc 1324 |
. . . . . . . . . . . . . . . . 17
mzPoly
mzPoly
mzPoly |
164 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly mzPoly |
165 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . . . . 21
|
166 | | reseq2 5391 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
167 | 166 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
168 | 167 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . 22
|
169 | 168 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . 21
|
170 | 165, 169 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . 20
|
171 | 164, 170 | rexeqbidv 3153 |
. . . . . . . . . . . . . . . . . . 19
mzPoly mzPoly |
172 | 168 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . 21
|
173 | 165, 172 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . 20
|
174 | 164, 173 | rexeqbidv 3153 |
. . . . . . . . . . . . . . . . . . 19
mzPoly mzPoly |
175 | 171, 174 | anbi12d 747 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly
mzPoly
mzPoly
|
176 | 175 | rspcev 3309 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly
mzPoly mzPoly |
177 | 78, 144, 163, 176 | syl12anc 1324 |
. . . . . . . . . . . . . . . 16
mzPoly
mzPoly
mzPoly mzPoly |
178 | 177 | adantlrr 757 |
. . . . . . . . . . . . . . 15
mzPoly mzPoly mzPoly mzPoly |
179 | 178 | adantrrr 761 |
. . . . . . . . . . . . . 14
mzPoly mzPoly
mzPoly mzPoly |
180 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly mzPoly
|
181 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly mzPoly
|
182 | 180, 181 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . 19
mzPoly mzPoly
|
183 | 182 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly
|
184 | 183 | anbi2d 740 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly
|
185 | 184 | rexbidv 3052 |
. . . . . . . . . . . . . . . 16
mzPoly mzPoly
mzPoly
mzPoly |
186 | 180, 181 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . 19
mzPoly mzPoly
|
187 | 186 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly
|
188 | 187 | anbi2d 740 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly
|
189 | 188 | rexbidv 3052 |
. . . . . . . . . . . . . . . 16
mzPoly mzPoly
mzPoly
mzPoly |
190 | 185, 189 | anbi12d 747 |
. . . . . . . . . . . . . . 15
mzPoly mzPoly
mzPoly
mzPoly mzPoly mzPoly |
191 | 190 | rexbidv 3052 |
. . . . . . . . . . . . . 14
mzPoly mzPoly
mzPoly
mzPoly mzPoly mzPoly |
192 | 179, 191 | mpbird 247 |
. . . . . . . . . . . . 13
mzPoly mzPoly
mzPoly mzPoly |
193 | | r19.40 3088 |
. . . . . . . . . . . . 13
mzPoly mzPoly mzPoly mzPoly |
194 | 192, 193 | syl 17 |
. . . . . . . . . . . 12
mzPoly mzPoly
mzPoly mzPoly |
195 | 194 | exp32 631 |
. . . . . . . . . . 11
mzPoly
mzPoly
mzPoly
mzPoly |
196 | 195 | rexlimdvv 3037 |
. . . . . . . . . 10
mzPoly
mzPoly
mzPoly
mzPoly |
197 | 196 | ex 450 |
. . . . . . . . 9
mzPoly
mzPoly
mzPoly
mzPoly |
198 | 197 | rexlimivv 3036 |
. . . . . . . 8
mzPoly
mzPoly
mzPoly
mzPoly |
199 | 198 | imp 445 |
. . . . . . 7
mzPoly mzPoly
mzPoly
mzPoly |
200 | 199 | ad2ant2l 782 |
. . . . . 6
mzPoly
mzPoly
mzPoly mzPoly |
201 | 200 | 3adant1 1079 |
. . . . 5
mzPoly mzPoly
mzPoly mzPoly |
202 | 201 | simpld 475 |
. . . 4
mzPoly mzPoly mzPoly |
203 | 201 | simprd 479 |
. . . 4
mzPoly mzPoly mzPoly |
204 | | eqeq1 2626 |
. . . . . 6
|
205 | 204 | anbi2d 740 |
. . . . 5
|
206 | 205 | 2rexbidv 3057 |
. . . 4
mzPoly
mzPoly |
207 | | eqeq1 2626 |
. . . . . 6
|
208 | 207 | anbi2d 740 |
. . . . 5
|
209 | 208 | 2rexbidv 3057 |
. . . 4
mzPoly
mzPoly |
210 | | eqeq1 2626 |
. . . . . . 7
|
211 | 210 | anbi2d 740 |
. . . . . 6
|
212 | 211 | 2rexbidv 3057 |
. . . . 5
mzPoly
mzPoly |
213 | | fveq2 6191 |
. . . . . . . 8
mzPoly mzPoly |
214 | | sseq1 3626 |
. . . . . . . . 9
|
215 | | reseq2 5391 |
. . . . . . . . . . . 12
|
216 | 215 | fveq2d 6195 |
. . . . . . . . . . 11
|
217 | 216 | mpteq2dv 4745 |
. . . . . . . . . 10
|
218 | 217 | eqeq2d 2632 |
. . . . . . . . 9
|
219 | 214, 218 | anbi12d 747 |
. . . . . . . 8
|
220 | 213, 219 | rexeqbidv 3153 |
. . . . . . 7
mzPoly
mzPoly |
221 | | fveq1 6190 |
. . . . . . . . . . 11
|
222 | 221 | mpteq2dv 4745 |
. . . . . . . . . 10
|
223 | 222 | eqeq2d 2632 |
. . . . . . . . 9
|
224 | 223 | anbi2d 740 |
. . . . . . . 8
|
225 | 224 | cbvrexv 3172 |
. . . . . . 7
mzPoly
mzPoly |
226 | 220, 225 | syl6bb 276 |
. . . . . 6
mzPoly
mzPoly |
227 | 226 | cbvrexv 3172 |
. . . . 5
mzPoly mzPoly |
228 | 212, 227 | syl6bb 276 |
. . . 4
mzPoly
mzPoly |
229 | | eqeq1 2626 |
. . . . . . 7
|
230 | 229 | anbi2d 740 |
. . . . . 6
|
231 | 230 | 2rexbidv 3057 |
. . . . 5
mzPoly
mzPoly |
232 | | fveq2 6191 |
. . . . . . . 8
mzPoly mzPoly |
233 | | sseq1 3626 |
. . . . . . . . 9
|
234 | | reseq2 5391 |
. . . . . . . . . . . 12
|
235 | 234 | fveq2d 6195 |
. . . . . . . . . . 11
|
236 | 235 | mpteq2dv 4745 |
. . . . . . . . . 10
|
237 | 236 | eqeq2d 2632 |
. . . . . . . . 9
|
238 | 233, 237 | anbi12d 747 |
. . . . . . . 8
|
239 | 232, 238 | rexeqbidv 3153 |
. . . . . . 7
mzPoly
mzPoly |
240 | | fveq1 6190 |
. . . . . . . . . . 11
|
241 | 240 | mpteq2dv 4745 |
. . . . . . . . . 10
|
242 | 241 | eqeq2d 2632 |
. . . . . . . . 9
|
243 | 242 | anbi2d 740 |
. . . . . . . 8
|
244 | 243 | cbvrexv 3172 |
. . . . . . 7
mzPoly
mzPoly |
245 | 239, 244 | syl6bb 276 |
. . . . . 6
mzPoly
mzPoly |
246 | 245 | cbvrexv 3172 |
. . . . 5
mzPoly mzPoly |
247 | 231, 246 | syl6bb 276 |
. . . 4
mzPoly
mzPoly |
248 | | eqeq1 2626 |
. . . . . 6
|
249 | 248 | anbi2d 740 |
. . . . 5
|
250 | 249 | 2rexbidv 3057 |
. . . 4
mzPoly
mzPoly |
251 | | eqeq1 2626 |
. . . . . 6
|
252 | 251 | anbi2d 740 |
. . . . 5
|
253 | 252 | 2rexbidv 3057 |
. . . 4
mzPoly
mzPoly |
254 | | eqeq1 2626 |
. . . . . 6
|
255 | 254 | anbi2d 740 |
. . . . 5
|
256 | 255 | 2rexbidv 3057 |
. . . 4
mzPoly
mzPoly |
257 | 33, 74, 202, 203, 206, 209, 228, 247, 250, 253, 256 | mzpindd 37309 |
. . 3
mzPoly
mzPoly
|
258 | 1, 257 | mpan 706 |
. 2
mzPoly
mzPoly
|
259 | | reseq1 5390 |
. . . . . . 7
|
260 | 259 | fveq2d 6195 |
. . . . . 6
|
261 | 260 | cbvmptv 4750 |
. . . . 5
|
262 | 261 | eqeq2i 2634 |
. . . 4
|
263 | 262 | anbi2i 730 |
. . 3
|
264 | 263 | 2rexbii 3042 |
. 2
mzPoly mzPoly |
265 | 258, 264 | sylib 208 |
1
mzPoly
mzPoly
|