Metamath Proof Explorer


Theorem mzpcompact2lem

Description: Lemma for mzpcompact2 . (Contributed by Stefan O'Rear, 9-Oct-2014)

Ref Expression
Hypothesis mzpcompact2lem.i B V
Assertion mzpcompact2lem A mzPoly B a Fin b mzPoly a a B A = c B b c a

Proof

Step Hyp Ref Expression
1 mzpcompact2lem.i B V
2 tru
3 0fin Fin
4 0ex V
5 mzpconst V f × f mzPoly
6 4 5 mpan f × f mzPoly
7 0ss B
8 7 a1i f B
9 fconstmpt B × f = d B f
10 simpr f d B d B
11 elmapssres d B B d
12 10 7 11 sylancl f d B d
13 vex f V
14 13 fvconst2 d × f d = f
15 12 14 syl f d B × f d = f
16 15 mpteq2dva f d B × f d = d B f
17 9 16 eqtr4id f B × f = d B × f d
18 fveq1 b = × f b d = × f d
19 18 mpteq2dv b = × f d B b d = d B × f d
20 19 eqeq2d b = × f B × f = d B b d B × f = d B × f d
21 20 anbi2d b = × f B B × f = d B b d B B × f = d B × f d
22 21 rspcev × f mzPoly B B × f = d B × f d b mzPoly B B × f = d B b d
23 6 8 17 22 syl12anc f b mzPoly B B × f = d B b d
24 fveq2 a = mzPoly a = mzPoly
25 sseq1 a = a B B
26 reseq2 a = d a = d
27 26 fveq2d a = b d a = b d
28 27 mpteq2dv a = d B b d a = d B b d
29 28 eqeq2d a = B × f = d B b d a B × f = d B b d
30 25 29 anbi12d a = a B B × f = d B b d a B B × f = d B b d
31 24 30 rexeqbidv a = b mzPoly a a B B × f = d B b d a b mzPoly B B × f = d B b d
32 31 rspcev Fin b mzPoly B B × f = d B b d a Fin b mzPoly a a B B × f = d B b d a
33 3 23 32 sylancr f a Fin b mzPoly a a B B × f = d B b d a
34 33 adantl f a Fin b mzPoly a a B B × f = d B b d a
35 snfi f Fin
36 snex f V
37 vsnid f f
38 mzpproj f V f f g f g f mzPoly f
39 36 37 38 mp2an g f g f mzPoly f
40 39 a1i f B g f g f mzPoly f
41 snssi f B f B
42 fveq1 g = d g f = d f
43 42 cbvmptv g B g f = d B d f
44 simpr f B d B d B
45 simpl f B d B f B
46 45 snssd f B d B f B
47 elmapssres d B f B d f f
48 44 46 47 syl2anc f B d B d f f
49 fveq1 g = d f g f = d f f
50 eqid g f g f = g f g f
51 fvex d f f V
52 49 50 51 fvmpt d f f g f g f d f = d f f
53 48 52 syl f B d B g f g f d f = d f f
54 fvres f f d f f = d f
55 37 54 ax-mp d f f = d f
56 53 55 eqtr2di f B d B d f = g f g f d f
57 56 mpteq2dva f B d B d f = d B g f g f d f
58 43 57 syl5eq f B g B g f = d B g f g f d f
59 fveq1 b = g f g f b d f = g f g f d f
60 59 mpteq2dv b = g f g f d B b d f = d B g f g f d f
61 60 eqeq2d b = g f g f g B g f = d B b d f g B g f = d B g f g f d f
62 61 anbi2d b = g f g f f B g B g f = d B b d f f B g B g f = d B g f g f d f
63 62 rspcev g f g f mzPoly f f B g B g f = d B g f g f d f b mzPoly f f B g B g f = d B b d f
64 40 41 58 63 syl12anc f B b mzPoly f f B g B g f = d B b d f
65 fveq2 a = f mzPoly a = mzPoly f
66 sseq1 a = f a B f B
67 reseq2 a = f d a = d f
68 67 fveq2d a = f b d a = b d f
69 68 mpteq2dv a = f d B b d a = d B b d f
70 69 eqeq2d a = f g B g f = d B b d a g B g f = d B b d f
71 66 70 anbi12d a = f a B g B g f = d B b d a f B g B g f = d B b d f
72 65 71 rexeqbidv a = f b mzPoly a a B g B g f = d B b d a b mzPoly f f B g B g f = d B b d f
73 72 rspcev f Fin b mzPoly f f B g B g f = d B b d f a Fin b mzPoly a a B g B g f = d B b d a
74 35 64 73 sylancr f B a Fin b mzPoly a a B g B g f = d B b d a
75 74 adantl f B a Fin b mzPoly a a B g B g f = d B b d a
76 simplll h Fin i mzPoly h h B j Fin k mzPoly j j B h Fin
77 simprll h Fin i mzPoly h h B j Fin k mzPoly j j B j Fin
78 unfi h Fin j Fin h j Fin
79 76 77 78 syl2anc h Fin i mzPoly h h B j Fin k mzPoly j j B h j Fin
80 vex h V
81 vex j V
82 80 81 unex h j V
83 82 a1i h Fin i mzPoly h h B j Fin k mzPoly j j B h j V
84 ssun1 h h j
85 84 a1i h Fin i mzPoly h h B j Fin k mzPoly j j B h h j
86 simpllr h Fin i mzPoly h h B j Fin k mzPoly j j B i mzPoly h
87 mzpresrename h j V h h j i mzPoly h l h j i l h mzPoly h j
88 83 85 86 87 syl3anc h Fin i mzPoly h h B j Fin k mzPoly j j B l h j i l h mzPoly h j
89 ssun2 j h j
90 89 a1i h Fin i mzPoly h h B j Fin k mzPoly j j B j h j
91 simprlr h Fin i mzPoly h h B j Fin k mzPoly j j B k mzPoly j
92 mzpresrename h j V j h j k mzPoly j l h j k l j mzPoly h j
93 83 90 91 92 syl3anc h Fin i mzPoly h h B j Fin k mzPoly j j B l h j k l j mzPoly h j
94 mzpaddmpt l h j i l h mzPoly h j l h j k l j mzPoly h j l h j i l h + k l j mzPoly h j
95 88 93 94 syl2anc h Fin i mzPoly h h B j Fin k mzPoly j j B l h j i l h + k l j mzPoly h j
96 simplr h Fin i mzPoly h h B j Fin k mzPoly j j B h B
97 simprr h Fin i mzPoly h h B j Fin k mzPoly j j B j B
98 96 97 unssd h Fin i mzPoly h h B j Fin k mzPoly j j B h j B
99 ovex B V
100 99 a1i h Fin i mzPoly h h B j Fin k mzPoly j j B B V
101 1 a1i h Fin i mzPoly h h B j Fin k mzPoly j j B B V
102 mzpresrename B V h B i mzPoly h d B i d h mzPoly B
103 101 96 86 102 syl3anc h Fin i mzPoly h h B j Fin k mzPoly j j B d B i d h mzPoly B
104 mzpf d B i d h mzPoly B d B i d h : B
105 ffn d B i d h : B d B i d h Fn B
106 103 104 105 3syl h Fin i mzPoly h h B j Fin k mzPoly j j B d B i d h Fn B
107 mzpresrename B V j B k mzPoly j d B k d j mzPoly B
108 101 97 91 107 syl3anc h Fin i mzPoly h h B j Fin k mzPoly j j B d B k d j mzPoly B
109 mzpf d B k d j mzPoly B d B k d j : B
110 ffn d B k d j : B d B k d j Fn B
111 108 109 110 3syl h Fin i mzPoly h h B j Fin k mzPoly j j B d B k d j Fn B
112 ofmpteq B V d B i d h Fn B d B k d j Fn B d B i d h + f d B k d j = d B i d h + k d j
113 100 106 111 112 syl3anc h Fin i mzPoly h h B j Fin k mzPoly j j B d B i d h + f d B k d j = d B i d h + k d j
114 elmapi d B d : B
115 fssres d : B h j B d h j : h j
116 114 98 115 syl2anr h Fin i mzPoly h h B j Fin k mzPoly j j B d B d h j : h j
117 zex V
118 117 82 elmap d h j h j d h j : h j
119 116 118 sylibr h Fin i mzPoly h h B j Fin k mzPoly j j B d B d h j h j
120 reseq1 l = d h j l h = d h j h
121 120 fveq2d l = d h j i l h = i d h j h
122 reseq1 l = d h j l j = d h j j
123 122 fveq2d l = d h j k l j = k d h j j
124 121 123 oveq12d l = d h j i l h + k l j = i d h j h + k d h j j
125 eqid l h j i l h + k l j = l h j i l h + k l j
126 ovex i d h j h + k d h j j V
127 124 125 126 fvmpt d h j h j l h j i l h + k l j d h j = i d h j h + k d h j j
128 119 127 syl h Fin i mzPoly h h B j Fin k mzPoly j j B d B l h j i l h + k l j d h j = i d h j h + k d h j j
129 resabs1 h h j d h j h = d h
130 84 129 ax-mp d h j h = d h
131 130 fveq2i i d h j h = i d h
132 resabs1 j h j d h j j = d j
133 89 132 ax-mp d h j j = d j
134 133 fveq2i k d h j j = k d j
135 131 134 oveq12i i d h j h + k d h j j = i d h + k d j
136 128 135 eqtr2di h Fin i mzPoly h h B j Fin k mzPoly j j B d B i d h + k d j = l h j i l h + k l j d h j
137 136 mpteq2dva h Fin i mzPoly h h B j Fin k mzPoly j j B d B i d h + k d j = d B l h j i l h + k l j d h j
138 113 137 eqtrd h Fin i mzPoly h h B j Fin k mzPoly j j B d B i d h + f d B k d j = d B l h j i l h + k l j d h j
139 fveq1 b = l h j i l h + k l j b d h j = l h j i l h + k l j d h j
140 139 mpteq2dv b = l h j i l h + k l j d B b d h j = d B l h j i l h + k l j d h j
141 140 eqeq2d b = l h j i l h + k l j d B i d h + f d B k d j = d B b d h j d B i d h + f d B k d j = d B l h j i l h + k l j d h j
142 141 anbi2d b = l h j i l h + k l j h j B d B i d h + f d B k d j = d B b d h j h j B d B i d h + f d B k d j = d B l h j i l h + k l j d h j
143 142 rspcev l h j i l h + k l j mzPoly h j h j B d B i d h + f d B k d j = d B l h j i l h + k l j d h j b mzPoly h j h j B d B i d h + f d B k d j = d B b d h j
144 95 98 138 143 syl12anc h Fin i mzPoly h h B j Fin k mzPoly j j B b mzPoly h j h j B d B i d h + f d B k d j = d B b d h j
145 mzpmulmpt l h j i l h mzPoly h j l h j k l j mzPoly h j l h j i l h k l j mzPoly h j
146 88 93 145 syl2anc h Fin i mzPoly h h B j Fin k mzPoly j j B l h j i l h k l j mzPoly h j
147 ofmpteq B V d B i d h Fn B d B k d j Fn B d B i d h × f d B k d j = d B i d h k d j
148 100 106 111 147 syl3anc h Fin i mzPoly h h B j Fin k mzPoly j j B d B i d h × f d B k d j = d B i d h k d j
149 121 123 oveq12d l = d h j i l h k l j = i d h j h k d h j j
150 eqid l h j i l h k l j = l h j i l h k l j
151 ovex i d h j h k d h j j V
152 149 150 151 fvmpt d h j h j l h j i l h k l j d h j = i d h j h k d h j j
153 119 152 syl h Fin i mzPoly h h B j Fin k mzPoly j j B d B l h j i l h k l j d h j = i d h j h k d h j j
154 131 134 oveq12i i d h j h k d h j j = i d h k d j
155 153 154 eqtr2di h Fin i mzPoly h h B j Fin k mzPoly j j B d B i d h k d j = l h j i l h k l j d h j
156 155 mpteq2dva h Fin i mzPoly h h B j Fin k mzPoly j j B d B i d h k d j = d B l h j i l h k l j d h j
157 148 156 eqtrd h Fin i mzPoly h h B j Fin k mzPoly j j B d B i d h × f d B k d j = d B l h j i l h k l j d h j
158 fveq1 b = l h j i l h k l j b d h j = l h j i l h k l j d h j
159 158 mpteq2dv b = l h j i l h k l j d B b d h j = d B l h j i l h k l j d h j
160 159 eqeq2d b = l h j i l h k l j d B i d h × f d B k d j = d B b d h j d B i d h × f d B k d j = d B l h j i l h k l j d h j
161 160 anbi2d b = l h j i l h k l j h j B d B i d h × f d B k d j = d B b d h j h j B d B i d h × f d B k d j = d B l h j i l h k l j d h j
162 161 rspcev l h j i l h k l j mzPoly h j h j B d B i d h × f d B k d j = d B l h j i l h k l j d h j b mzPoly h j h j B d B i d h × f d B k d j = d B b d h j
163 146 98 157 162 syl12anc h Fin i mzPoly h h B j Fin k mzPoly j j B b mzPoly h j h j B d B i d h × f d B k d j = d B b d h j
164 fveq2 a = h j mzPoly a = mzPoly h j
165 sseq1 a = h j a B h j B
166 reseq2 a = h j d a = d h j
167 166 fveq2d a = h j b d a = b d h j
168 167 mpteq2dv a = h j d B b d a = d B b d h j
169 168 eqeq2d a = h j d B i d h + f d B k d j = d B b d a d B i d h + f d B k d j = d B b d h j
170 165 169 anbi12d a = h j a B d B i d h + f d B k d j = d B b d a h j B d B i d h + f d B k d j = d B b d h j
171 164 170 rexeqbidv a = h j b mzPoly a a B d B i d h + f d B k d j = d B b d a b mzPoly h j h j B d B i d h + f d B k d j = d B b d h j
172 168 eqeq2d a = h j d B i d h × f d B k d j = d B b d a d B i d h × f d B k d j = d B b d h j
173 165 172 anbi12d a = h j a B d B i d h × f d B k d j = d B b d a h j B d B i d h × f d B k d j = d B b d h j
174 164 173 rexeqbidv a = h j b mzPoly a a B d B i d h × f d B k d j = d B b d a b mzPoly h j h j B d B i d h × f d B k d j = d B b d h j
175 171 174 anbi12d a = h j b mzPoly a a B d B i d h + f d B k d j = d B b d a b mzPoly a a B d B i d h × f d B k d j = d B b d a b mzPoly h j h j B d B i d h + f d B k d j = d B b d h j b mzPoly h j h j B d B i d h × f d B k d j = d B b d h j
176 175 rspcev h j Fin b mzPoly h j h j B d B i d h + f d B k d j = d B b d h j b mzPoly h j h j B d B i d h × f d B k d j = d B b d h j a Fin b mzPoly a a B d B i d h + f d B k d j = d B b d a b mzPoly a a B d B i d h × f d B k d j = d B b d a
177 79 144 163 176 syl12anc h Fin i mzPoly h h B j Fin k mzPoly j j B a Fin b mzPoly a a B d B i d h + f d B k d j = d B b d a b mzPoly a a B d B i d h × f d B k d j = d B b d a
178 177 adantlrr h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B a Fin b mzPoly a a B d B i d h + f d B k d j = d B b d a b mzPoly a a B d B i d h × f d B k d j = d B b d a
179 178 adantrrr h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j a Fin b mzPoly a a B d B i d h + f d B k d j = d B b d a b mzPoly a a B d B i d h × f d B k d j = d B b d a
180 simplrr h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j f = d B i d h
181 simprrr h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j g = d B k d j
182 180 181 oveq12d h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j f + f g = d B i d h + f d B k d j
183 182 eqeq1d h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j f + f g = d B b d a d B i d h + f d B k d j = d B b d a
184 183 anbi2d h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j a B f + f g = d B b d a a B d B i d h + f d B k d j = d B b d a
185 184 rexbidv h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j b mzPoly a a B f + f g = d B b d a b mzPoly a a B d B i d h + f d B k d j = d B b d a
186 180 181 oveq12d h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j f × f g = d B i d h × f d B k d j
187 186 eqeq1d h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j f × f g = d B b d a d B i d h × f d B k d j = d B b d a
188 187 anbi2d h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j a B f × f g = d B b d a a B d B i d h × f d B k d j = d B b d a
189 188 rexbidv h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j b mzPoly a a B f × f g = d B b d a b mzPoly a a B d B i d h × f d B k d j = d B b d a
190 185 189 anbi12d h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j b mzPoly a a B f + f g = d B b d a b mzPoly a a B f × f g = d B b d a b mzPoly a a B d B i d h + f d B k d j = d B b d a b mzPoly a a B d B i d h × f d B k d j = d B b d a
191 190 rexbidv h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j a Fin b mzPoly a a B f + f g = d B b d a b mzPoly a a B f × f g = d B b d a a Fin b mzPoly a a B d B i d h + f d B k d j = d B b d a b mzPoly a a B d B i d h × f d B k d j = d B b d a
192 179 191 mpbird h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j a Fin b mzPoly a a B f + f g = d B b d a b mzPoly a a B f × f g = d B b d a
193 r19.40 a Fin b mzPoly a a B f + f g = d B b d a b mzPoly a a B f × f g = d B b d a a Fin b mzPoly a a B f + f g = d B b d a a Fin b mzPoly a a B f × f g = d B b d a
194 192 193 syl h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j a Fin b mzPoly a a B f + f g = d B b d a a Fin b mzPoly a a B f × f g = d B b d a
195 194 exp32 h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j a Fin b mzPoly a a B f + f g = d B b d a a Fin b mzPoly a a B f × f g = d B b d a
196 195 rexlimdvv h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j a Fin b mzPoly a a B f + f g = d B b d a a Fin b mzPoly a a B f × f g = d B b d a
197 196 ex h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j a Fin b mzPoly a a B f + f g = d B b d a a Fin b mzPoly a a B f × f g = d B b d a
198 197 rexlimivv h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j a Fin b mzPoly a a B f + f g = d B b d a a Fin b mzPoly a a B f × f g = d B b d a
199 198 imp h Fin i mzPoly h h B f = d B i d h j Fin k mzPoly j j B g = d B k d j a Fin b mzPoly a a B f + f g = d B b d a a Fin b mzPoly a a B f × f g = d B b d a
200 199 ad2ant2l f : B h Fin i mzPoly h h B f = d B i d h g : B j Fin k mzPoly j j B g = d B k d j a Fin b mzPoly a a B f + f g = d B b d a a Fin b mzPoly a a B f × f g = d B b d a
201 200 3adant1 f : B h Fin i mzPoly h h B f = d B i d h g : B j Fin k mzPoly j j B g = d B k d j a Fin b mzPoly a a B f + f g = d B b d a a Fin b mzPoly a a B f × f g = d B b d a
202 201 simpld f : B h Fin i mzPoly h h B f = d B i d h g : B j Fin k mzPoly j j B g = d B k d j a Fin b mzPoly a a B f + f g = d B b d a
203 201 simprd f : B h Fin i mzPoly h h B f = d B i d h g : B j Fin k mzPoly j j B g = d B k d j a Fin b mzPoly a a B f × f g = d B b d a
204 eqeq1 e = B × f e = d B b d a B × f = d B b d a
205 204 anbi2d e = B × f a B e = d B b d a a B B × f = d B b d a
206 205 2rexbidv e = B × f a Fin b mzPoly a a B e = d B b d a a Fin b mzPoly a a B B × f = d B b d a
207 eqeq1 e = g B g f e = d B b d a g B g f = d B b d a
208 207 anbi2d e = g B g f a B e = d B b d a a B g B g f = d B b d a
209 208 2rexbidv e = g B g f a Fin b mzPoly a a B e = d B b d a a Fin b mzPoly a a B g B g f = d B b d a
210 eqeq1 e = f e = d B b d a f = d B b d a
211 210 anbi2d e = f a B e = d B b d a a B f = d B b d a
212 211 2rexbidv e = f a Fin b mzPoly a a B e = d B b d a a Fin b mzPoly a a B f = d B b d a
213 fveq2 a = h mzPoly a = mzPoly h
214 sseq1 a = h a B h B
215 reseq2 a = h d a = d h
216 215 fveq2d a = h b d a = b d h
217 216 mpteq2dv a = h d B b d a = d B b d h
218 217 eqeq2d a = h f = d B b d a f = d B b d h
219 214 218 anbi12d a = h a B f = d B b d a h B f = d B b d h
220 213 219 rexeqbidv a = h b mzPoly a a B f = d B b d a b mzPoly h h B f = d B b d h
221 fveq1 b = i b d h = i d h
222 221 mpteq2dv b = i d B b d h = d B i d h
223 222 eqeq2d b = i f = d B b d h f = d B i d h
224 223 anbi2d b = i h B f = d B b d h h B f = d B i d h
225 224 cbvrexvw b mzPoly h h B f = d B b d h i mzPoly h h B f = d B i d h
226 220 225 bitrdi a = h b mzPoly a a B f = d B b d a i mzPoly h h B f = d B i d h
227 226 cbvrexvw a Fin b mzPoly a a B f = d B b d a h Fin i mzPoly h h B f = d B i d h
228 212 227 bitrdi e = f a Fin b mzPoly a a B e = d B b d a h Fin i mzPoly h h B f = d B i d h
229 eqeq1 e = g e = d B b d a g = d B b d a
230 229 anbi2d e = g a B e = d B b d a a B g = d B b d a
231 230 2rexbidv e = g a Fin b mzPoly a a B e = d B b d a a Fin b mzPoly a a B g = d B b d a
232 fveq2 a = j mzPoly a = mzPoly j
233 sseq1 a = j a B j B
234 reseq2 a = j d a = d j
235 234 fveq2d a = j b d a = b d j
236 235 mpteq2dv a = j d B b d a = d B b d j
237 236 eqeq2d a = j g = d B b d a g = d B b d j
238 233 237 anbi12d a = j a B g = d B b d a j B g = d B b d j
239 232 238 rexeqbidv a = j b mzPoly a a B g = d B b d a b mzPoly j j B g = d B b d j
240 fveq1 b = k b d j = k d j
241 240 mpteq2dv b = k d B b d j = d B k d j
242 241 eqeq2d b = k g = d B b d j g = d B k d j
243 242 anbi2d b = k j B g = d B b d j j B g = d B k d j
244 243 cbvrexvw b mzPoly j j B g = d B b d j k mzPoly j j B g = d B k d j
245 239 244 bitrdi a = j b mzPoly a a B g = d B b d a k mzPoly j j B g = d B k d j
246 245 cbvrexvw a Fin b mzPoly a a B g = d B b d a j Fin k mzPoly j j B g = d B k d j
247 231 246 bitrdi e = g a Fin b mzPoly a a B e = d B b d a j Fin k mzPoly j j B g = d B k d j
248 eqeq1 e = f + f g e = d B b d a f + f g = d B b d a
249 248 anbi2d e = f + f g a B e = d B b d a a B f + f g = d B b d a
250 249 2rexbidv e = f + f g a Fin b mzPoly a a B e = d B b d a a Fin b mzPoly a a B f + f g = d B b d a
251 eqeq1 e = f × f g e = d B b d a f × f g = d B b d a
252 251 anbi2d e = f × f g a B e = d B b d a a B f × f g = d B b d a
253 252 2rexbidv e = f × f g a Fin b mzPoly a a B e = d B b d a a Fin b mzPoly a a B f × f g = d B b d a
254 eqeq1 e = A e = d B b d a A = d B b d a
255 254 anbi2d e = A a B e = d B b d a a B A = d B b d a
256 255 2rexbidv e = A a Fin b mzPoly a a B e = d B b d a a Fin b mzPoly a a B A = d B b d a
257 34 75 202 203 206 209 228 247 250 253 256 mzpindd A mzPoly B a Fin b mzPoly a a B A = d B b d a
258 2 257 mpan A mzPoly B a Fin b mzPoly a a B A = d B b d a
259 reseq1 d = c d a = c a
260 259 fveq2d d = c b d a = b c a
261 260 cbvmptv d B b d a = c B b c a
262 261 eqeq2i A = d B b d a A = c B b c a
263 262 anbi2i a B A = d B b d a a B A = c B b c a
264 263 2rexbii a Fin b mzPoly a a B A = d B b d a a Fin b mzPoly a a B A = c B b c a
265 258 264 sylib A mzPoly B a Fin b mzPoly a a B A = c B b c a