Metamath Proof Explorer


Theorem evlslem1

Description: Lemma for evlseu , give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015) (Proof shortened by AV, 26-Jul-2019) (Revised by AV, 11-Apr-2024)

Ref Expression
Hypotheses evlslem1.p P = I mPoly R
evlslem1.b B = Base P
evlslem1.c C = Base S
evlslem1.d D = h 0 I | h -1 Fin
evlslem1.t T = mulGrp S
evlslem1.x × ˙ = T
evlslem1.m · ˙ = S
evlslem1.v V = I mVar R
evlslem1.e E = p B S b D F p b · ˙ T b × ˙ f G
evlslem1.i φ I W
evlslem1.r φ R CRing
evlslem1.s φ S CRing
evlslem1.f φ F R RingHom S
evlslem1.g φ G : I C
evlslem1.a A = algSc P
Assertion evlslem1 φ E P RingHom S E A = F E V = G

Proof

Step Hyp Ref Expression
1 evlslem1.p P = I mPoly R
2 evlslem1.b B = Base P
3 evlslem1.c C = Base S
4 evlslem1.d D = h 0 I | h -1 Fin
5 evlslem1.t T = mulGrp S
6 evlslem1.x × ˙ = T
7 evlslem1.m · ˙ = S
8 evlslem1.v V = I mVar R
9 evlslem1.e E = p B S b D F p b · ˙ T b × ˙ f G
10 evlslem1.i φ I W
11 evlslem1.r φ R CRing
12 evlslem1.s φ S CRing
13 evlslem1.f φ F R RingHom S
14 evlslem1.g φ G : I C
15 evlslem1.a A = algSc P
16 eqid 1 P = 1 P
17 eqid 1 S = 1 S
18 eqid P = P
19 11 crngringd φ R Ring
20 1 10 19 mplringd φ P Ring
21 12 crngringd φ S Ring
22 2fveq3 x = 1 R E A x = E A 1 R
23 fveq2 x = 1 R F x = F 1 R
24 22 23 eqeq12d x = 1 R E A x = F x E A 1 R = F 1 R
25 eqid 0 R = 0 R
26 eqid Base R = Base R
27 10 adantr φ x Base R I W
28 19 adantr φ x Base R R Ring
29 simpr φ x Base R x Base R
30 1 4 25 26 15 27 28 29 mplascl φ x Base R A x = y D if y = I × 0 x 0 R
31 30 fveq2d φ x Base R E A x = E y D if y = I × 0 x 0 R
32 11 adantr φ x Base R R CRing
33 12 adantr φ x Base R S CRing
34 13 adantr φ x Base R F R RingHom S
35 14 adantr φ x Base R G : I C
36 4 psrbag0 I W I × 0 D
37 10 36 syl φ I × 0 D
38 37 adantr φ x Base R I × 0 D
39 1 2 3 26 4 5 6 7 8 9 27 32 33 34 35 25 38 29 evlslem3 φ x Base R E y D if y = I × 0 x 0 R = F x · ˙ T I × 0 × ˙ f G
40 0zd φ x I 0
41 fvexd φ x I G x V
42 fconstmpt I × 0 = x I 0
43 42 a1i φ I × 0 = x I 0
44 14 feqmptd φ G = x I G x
45 10 40 41 43 44 offval2 φ I × 0 × ˙ f G = x I 0 × ˙ G x
46 14 ffvelcdmda φ x I G x C
47 5 3 mgpbas C = Base T
48 5 17 ringidval 1 S = 0 T
49 47 48 6 mulg0 G x C 0 × ˙ G x = 1 S
50 46 49 syl φ x I 0 × ˙ G x = 1 S
51 50 mpteq2dva φ x I 0 × ˙ G x = x I 1 S
52 45 51 eqtrd φ I × 0 × ˙ f G = x I 1 S
53 52 oveq2d φ T I × 0 × ˙ f G = T x I 1 S
54 5 crngmgp S CRing T CMnd
55 12 54 syl φ T CMnd
56 55 cmnmndd φ T Mnd
57 48 gsumz T Mnd I W T x I 1 S = 1 S
58 56 10 57 syl2anc φ T x I 1 S = 1 S
59 53 58 eqtrd φ T I × 0 × ˙ f G = 1 S
60 59 adantr φ x Base R T I × 0 × ˙ f G = 1 S
61 60 oveq2d φ x Base R F x · ˙ T I × 0 × ˙ f G = F x · ˙ 1 S
62 26 3 rhmf F R RingHom S F : Base R C
63 13 62 syl φ F : Base R C
64 63 ffvelcdmda φ x Base R F x C
65 3 7 17 ringridm S Ring F x C F x · ˙ 1 S = F x
66 21 64 65 syl2an2r φ x Base R F x · ˙ 1 S = F x
67 61 66 eqtrd φ x Base R F x · ˙ T I × 0 × ˙ f G = F x
68 31 39 67 3eqtrd φ x Base R E A x = F x
69 68 ralrimiva φ x Base R E A x = F x
70 eqid 1 R = 1 R
71 26 70 ringidcl R Ring 1 R Base R
72 19 71 syl φ 1 R Base R
73 24 69 72 rspcdva φ E A 1 R = F 1 R
74 1 mplassa I W R CRing P AssAlg
75 10 11 74 syl2anc φ P AssAlg
76 eqid Scalar P = Scalar P
77 15 76 asclrhm P AssAlg A Scalar P RingHom P
78 75 77 syl φ A Scalar P RingHom P
79 1 10 11 mplsca φ R = Scalar P
80 79 oveq1d φ R RingHom P = Scalar P RingHom P
81 78 80 eleqtrrd φ A R RingHom P
82 70 16 rhm1 A R RingHom P A 1 R = 1 P
83 81 82 syl φ A 1 R = 1 P
84 83 fveq2d φ E A 1 R = E 1 P
85 70 17 rhm1 F R RingHom S F 1 R = 1 S
86 13 85 syl φ F 1 R = 1 S
87 73 84 86 3eqtr3d φ E 1 P = 1 S
88 eqid + P = + P
89 eqid + S = + S
90 20 ringgrpd φ P Grp
91 21 ringgrpd φ S Grp
92 eqid 0 S = 0 S
93 ringcmn S Ring S CMnd
94 21 93 syl φ S CMnd
95 94 adantr φ p B S CMnd
96 ovex 0 I V
97 4 96 rabex2 D V
98 97 a1i φ p B D V
99 10 adantr φ p B I W
100 11 adantr φ p B R CRing
101 12 adantr φ p B S CRing
102 13 adantr φ p B F R RingHom S
103 14 adantr φ p B G : I C
104 simpr φ p B p B
105 1 2 3 4 5 6 7 8 9 99 100 101 102 103 104 evlslem6 φ p B b D F p b · ˙ T b × ˙ f G : D C finSupp 0 S b D F p b · ˙ T b × ˙ f G
106 105 simpld φ p B b D F p b · ˙ T b × ˙ f G : D C
107 105 simprd φ p B finSupp 0 S b D F p b · ˙ T b × ˙ f G
108 3 92 95 98 106 107 gsumcl φ p B S b D F p b · ˙ T b × ˙ f G C
109 108 9 fmptd φ E : B C
110 eqid + R = + R
111 simplrl φ x B y B b D x B
112 simplrr φ x B y B b D y B
113 1 2 110 88 111 112 mpladd φ x B y B b D x + P y = x + R f y
114 113 fveq1d φ x B y B b D x + P y b = x + R f y b
115 simprl φ x B y B x B
116 1 26 2 4 115 mplelf φ x B y B x : D Base R
117 116 ffnd φ x B y B x Fn D
118 117 adantr φ x B y B b D x Fn D
119 simprr φ x B y B y B
120 1 26 2 4 119 mplelf φ x B y B y : D Base R
121 120 ffnd φ x B y B y Fn D
122 121 adantr φ x B y B b D y Fn D
123 97 a1i φ x B y B b D D V
124 simpr φ x B y B b D b D
125 fnfvof x Fn D y Fn D D V b D x + R f y b = x b + R y b
126 118 122 123 124 125 syl22anc φ x B y B b D x + R f y b = x b + R y b
127 114 126 eqtrd φ x B y B b D x + P y b = x b + R y b
128 127 fveq2d φ x B y B b D F x + P y b = F x b + R y b
129 rhmghm F R RingHom S F R GrpHom S
130 13 129 syl φ F R GrpHom S
131 130 ad2antrr φ x B y B b D F R GrpHom S
132 116 ffvelcdmda φ x B y B b D x b Base R
133 120 ffvelcdmda φ x B y B b D y b Base R
134 26 110 89 ghmlin F R GrpHom S x b Base R y b Base R F x b + R y b = F x b + S F y b
135 131 132 133 134 syl3anc φ x B y B b D F x b + R y b = F x b + S F y b
136 128 135 eqtrd φ x B y B b D F x + P y b = F x b + S F y b
137 136 oveq1d φ x B y B b D F x + P y b · ˙ T b × ˙ f G = F x b + S F y b · ˙ T b × ˙ f G
138 21 ad2antrr φ x B y B b D S Ring
139 63 ad2antrr φ x B y B b D F : Base R C
140 139 132 ffvelcdmd φ x B y B b D F x b C
141 139 133 ffvelcdmd φ x B y B b D F y b C
142 55 ad2antrr φ x B y B b D T CMnd
143 14 ad2antrr φ x B y B b D G : I C
144 4 47 6 142 124 143 psrbagev2 φ x B y B b D T b × ˙ f G C
145 3 89 7 ringdir S Ring F x b C F y b C T b × ˙ f G C F x b + S F y b · ˙ T b × ˙ f G = F x b · ˙ T b × ˙ f G + S F y b · ˙ T b × ˙ f G
146 138 140 141 144 145 syl13anc φ x B y B b D F x b + S F y b · ˙ T b × ˙ f G = F x b · ˙ T b × ˙ f G + S F y b · ˙ T b × ˙ f G
147 137 146 eqtrd φ x B y B b D F x + P y b · ˙ T b × ˙ f G = F x b · ˙ T b × ˙ f G + S F y b · ˙ T b × ˙ f G
148 147 mpteq2dva φ x B y B b D F x + P y b · ˙ T b × ˙ f G = b D F x b · ˙ T b × ˙ f G + S F y b · ˙ T b × ˙ f G
149 97 a1i φ x B y B D V
150 ovexd φ x B y B b D F x b · ˙ T b × ˙ f G V
151 ovexd φ x B y B b D F y b · ˙ T b × ˙ f G V
152 eqidd φ x B y B b D F x b · ˙ T b × ˙ f G = b D F x b · ˙ T b × ˙ f G
153 eqidd φ x B y B b D F y b · ˙ T b × ˙ f G = b D F y b · ˙ T b × ˙ f G
154 149 150 151 152 153 offval2 φ x B y B b D F x b · ˙ T b × ˙ f G + S f b D F y b · ˙ T b × ˙ f G = b D F x b · ˙ T b × ˙ f G + S F y b · ˙ T b × ˙ f G
155 148 154 eqtr4d φ x B y B b D F x + P y b · ˙ T b × ˙ f G = b D F x b · ˙ T b × ˙ f G + S f b D F y b · ˙ T b × ˙ f G
156 155 oveq2d φ x B y B S b D F x + P y b · ˙ T b × ˙ f G = S b D F x b · ˙ T b × ˙ f G + S f b D F y b · ˙ T b × ˙ f G
157 94 adantr φ x B y B S CMnd
158 10 adantr φ x B y B I W
159 11 adantr φ x B y B R CRing
160 12 adantr φ x B y B S CRing
161 13 adantr φ x B y B F R RingHom S
162 14 adantr φ x B y B G : I C
163 1 2 3 4 5 6 7 8 9 158 159 160 161 162 115 evlslem6 φ x B y B b D F x b · ˙ T b × ˙ f G : D C finSupp 0 S b D F x b · ˙ T b × ˙ f G
164 163 simpld φ x B y B b D F x b · ˙ T b × ˙ f G : D C
165 1 2 3 4 5 6 7 8 9 158 159 160 161 162 119 evlslem6 φ x B y B b D F y b · ˙ T b × ˙ f G : D C finSupp 0 S b D F y b · ˙ T b × ˙ f G
166 165 simpld φ x B y B b D F y b · ˙ T b × ˙ f G : D C
167 163 simprd φ x B y B finSupp 0 S b D F x b · ˙ T b × ˙ f G
168 165 simprd φ x B y B finSupp 0 S b D F y b · ˙ T b × ˙ f G
169 3 92 89 157 149 164 166 167 168 gsumadd φ x B y B S b D F x b · ˙ T b × ˙ f G + S f b D F y b · ˙ T b × ˙ f G = S b D F x b · ˙ T b × ˙ f G + S S b D F y b · ˙ T b × ˙ f G
170 156 169 eqtrd φ x B y B S b D F x + P y b · ˙ T b × ˙ f G = S b D F x b · ˙ T b × ˙ f G + S S b D F y b · ˙ T b × ˙ f G
171 90 adantr φ x B y B P Grp
172 2 88 grpcl P Grp x B y B x + P y B
173 171 115 119 172 syl3anc φ x B y B x + P y B
174 fveq1 p = x + P y p b = x + P y b
175 174 fveq2d p = x + P y F p b = F x + P y b
176 175 oveq1d p = x + P y F p b · ˙ T b × ˙ f G = F x + P y b · ˙ T b × ˙ f G
177 176 mpteq2dv p = x + P y b D F p b · ˙ T b × ˙ f G = b D F x + P y b · ˙ T b × ˙ f G
178 177 oveq2d p = x + P y S b D F p b · ˙ T b × ˙ f G = S b D F x + P y b · ˙ T b × ˙ f G
179 ovex S b D F x + P y b · ˙ T b × ˙ f G V
180 178 9 179 fvmpt x + P y B E x + P y = S b D F x + P y b · ˙ T b × ˙ f G
181 173 180 syl φ x B y B E x + P y = S b D F x + P y b · ˙ T b × ˙ f G
182 fveq1 p = x p b = x b
183 182 fveq2d p = x F p b = F x b
184 183 oveq1d p = x F p b · ˙ T b × ˙ f G = F x b · ˙ T b × ˙ f G
185 184 mpteq2dv p = x b D F p b · ˙ T b × ˙ f G = b D F x b · ˙ T b × ˙ f G
186 185 oveq2d p = x S b D F p b · ˙ T b × ˙ f G = S b D F x b · ˙ T b × ˙ f G
187 ovex S b D F x b · ˙ T b × ˙ f G V
188 186 9 187 fvmpt x B E x = S b D F x b · ˙ T b × ˙ f G
189 115 188 syl φ x B y B E x = S b D F x b · ˙ T b × ˙ f G
190 fveq1 p = y p b = y b
191 190 fveq2d p = y F p b = F y b
192 191 oveq1d p = y F p b · ˙ T b × ˙ f G = F y b · ˙ T b × ˙ f G
193 192 mpteq2dv p = y b D F p b · ˙ T b × ˙ f G = b D F y b · ˙ T b × ˙ f G
194 193 oveq2d p = y S b D F p b · ˙ T b × ˙ f G = S b D F y b · ˙ T b × ˙ f G
195 ovex S b D F y b · ˙ T b × ˙ f G V
196 194 9 195 fvmpt y B E y = S b D F y b · ˙ T b × ˙ f G
197 196 ad2antll φ x B y B E y = S b D F y b · ˙ T b × ˙ f G
198 189 197 oveq12d φ x B y B E x + S E y = S b D F x b · ˙ T b × ˙ f G + S S b D F y b · ˙ T b × ˙ f G
199 170 181 198 3eqtr4d φ x B y B E x + P y = E x + S E y
200 2 3 88 89 90 91 109 199 isghmd φ E P GrpHom S
201 eqid mulGrp R = mulGrp R
202 201 5 rhmmhm F R RingHom S F mulGrp R MndHom T
203 13 202 syl φ F mulGrp R MndHom T
204 203 adantr φ x B y B z D w D F mulGrp R MndHom T
205 simprll φ x B y B z D w D x B
206 1 26 2 4 205 mplelf φ x B y B z D w D x : D Base R
207 simprrl φ x B y B z D w D z D
208 206 207 ffvelcdmd φ x B y B z D w D x z Base R
209 simprlr φ x B y B z D w D y B
210 1 26 2 4 209 mplelf φ x B y B z D w D y : D Base R
211 simprrr φ x B y B z D w D w D
212 210 211 ffvelcdmd φ x B y B z D w D y w Base R
213 201 26 mgpbas Base R = Base mulGrp R
214 eqid R = R
215 201 214 mgpplusg R = + mulGrp R
216 5 7 mgpplusg · ˙ = + T
217 213 215 216 mhmlin F mulGrp R MndHom T x z Base R y w Base R F x z R y w = F x z · ˙ F y w
218 204 208 212 217 syl3anc φ x B y B z D w D F x z R y w = F x z · ˙ F y w
219 56 ad2antrr φ z D w D v I T Mnd
220 simprl φ z D w D z D
221 4 psrbagf z D z : I 0
222 220 221 syl φ z D w D z : I 0
223 222 ffvelcdmda φ z D w D v I z v 0
224 4 psrbagf w D w : I 0
225 224 ad2antll φ z D w D w : I 0
226 225 ffvelcdmda φ z D w D v I w v 0
227 14 adantr φ z D w D G : I C
228 227 ffvelcdmda φ z D w D v I G v C
229 47 6 216 mulgnn0dir T Mnd z v 0 w v 0 G v C z v + w v × ˙ G v = z v × ˙ G v · ˙ w v × ˙ G v
230 219 223 226 228 229 syl13anc φ z D w D v I z v + w v × ˙ G v = z v × ˙ G v · ˙ w v × ˙ G v
231 230 mpteq2dva φ z D w D v I z v + w v × ˙ G v = v I z v × ˙ G v · ˙ w v × ˙ G v
232 10 adantr φ z D w D I W
233 ovexd φ z D w D v I z v + w v V
234 fvexd φ z D w D v I G v V
235 222 ffnd φ z D w D z Fn I
236 225 ffnd φ z D w D w Fn I
237 inidm I I = I
238 eqidd φ z D w D v I z v = z v
239 eqidd φ z D w D v I w v = w v
240 235 236 232 232 237 238 239 offval φ z D w D z + f w = v I z v + w v
241 14 feqmptd φ G = v I G v
242 241 adantr φ z D w D G = v I G v
243 232 233 234 240 242 offval2 φ z D w D z + f w × ˙ f G = v I z v + w v × ˙ G v
244 ovexd φ z D w D v I z v × ˙ G v V
245 ovexd φ z D w D v I w v × ˙ G v V
246 14 ffnd φ G Fn I
247 246 adantr φ z D w D G Fn I
248 eqidd φ z D w D v I G v = G v
249 235 247 232 232 237 238 248 offval φ z D w D z × ˙ f G = v I z v × ˙ G v
250 236 247 232 232 237 239 248 offval φ z D w D w × ˙ f G = v I w v × ˙ G v
251 232 244 245 249 250 offval2 φ z D w D z × ˙ f G · ˙ f w × ˙ f G = v I z v × ˙ G v · ˙ w v × ˙ G v
252 231 243 251 3eqtr4d φ z D w D z + f w × ˙ f G = z × ˙ f G · ˙ f w × ˙ f G
253 252 oveq2d φ z D w D T z + f w × ˙ f G = T z × ˙ f G · ˙ f w × ˙ f G
254 55 adantr φ z D w D T CMnd
255 4 47 6 48 254 220 227 psrbagev1 φ z D w D z × ˙ f G : I C finSupp 1 S z × ˙ f G
256 255 simpld φ z D w D z × ˙ f G : I C
257 simprr φ z D w D w D
258 4 47 6 48 254 257 227 psrbagev1 φ z D w D w × ˙ f G : I C finSupp 1 S w × ˙ f G
259 258 simpld φ z D w D w × ˙ f G : I C
260 255 simprd φ z D w D finSupp 1 S z × ˙ f G
261 258 simprd φ z D w D finSupp 1 S w × ˙ f G
262 47 48 216 254 232 256 259 260 261 gsumadd φ z D w D T z × ˙ f G · ˙ f w × ˙ f G = T z × ˙ f G · ˙ T w × ˙ f G
263 253 262 eqtrd φ z D w D T z + f w × ˙ f G = T z × ˙ f G · ˙ T w × ˙ f G
264 263 adantrl φ x B y B z D w D T z + f w × ˙ f G = T z × ˙ f G · ˙ T w × ˙ f G
265 218 264 oveq12d φ x B y B z D w D F x z R y w · ˙ T z + f w × ˙ f G = F x z · ˙ F y w · ˙ T z × ˙ f G · ˙ T w × ˙ f G
266 55 adantr φ x B y B z D w D T CMnd
267 63 adantr φ x B y B z D w D F : Base R C
268 267 208 ffvelcdmd φ x B y B z D w D F x z C
269 267 212 ffvelcdmd φ x B y B z D w D F y w C
270 4 47 6 254 220 227 psrbagev2 φ z D w D T z × ˙ f G C
271 270 adantrl φ x B y B z D w D T z × ˙ f G C
272 4 47 6 254 257 227 psrbagev2 φ z D w D T w × ˙ f G C
273 272 adantrl φ x B y B z D w D T w × ˙ f G C
274 47 216 cmn4 T CMnd F x z C F y w C T z × ˙ f G C T w × ˙ f G C F x z · ˙ F y w · ˙ T z × ˙ f G · ˙ T w × ˙ f G = F x z · ˙ T z × ˙ f G · ˙ F y w · ˙ T w × ˙ f G
275 266 268 269 271 273 274 syl122anc φ x B y B z D w D F x z · ˙ F y w · ˙ T z × ˙ f G · ˙ T w × ˙ f G = F x z · ˙ T z × ˙ f G · ˙ F y w · ˙ T w × ˙ f G
276 265 275 eqtrd φ x B y B z D w D F x z R y w · ˙ T z + f w × ˙ f G = F x z · ˙ T z × ˙ f G · ˙ F y w · ˙ T w × ˙ f G
277 10 adantr φ x B y B z D w D I W
278 11 adantr φ x B y B z D w D R CRing
279 12 adantr φ x B y B z D w D S CRing
280 13 adantr φ x B y B z D w D F R RingHom S
281 14 adantr φ x B y B z D w D G : I C
282 4 psrbagaddcl z D w D z + f w D
283 282 ad2antll φ x B y B z D w D z + f w D
284 19 adantr φ x B y B z D w D R Ring
285 26 214 ringcl R Ring x z Base R y w Base R x z R y w Base R
286 284 208 212 285 syl3anc φ x B y B z D w D x z R y w Base R
287 1 2 3 26 4 5 6 7 8 9 277 278 279 280 281 25 283 286 evlslem3 φ x B y B z D w D E v D if v = z + f w x z R y w 0 R = F x z R y w · ˙ T z + f w × ˙ f G
288 1 2 3 26 4 5 6 7 8 9 277 278 279 280 281 25 207 208 evlslem3 φ x B y B z D w D E v D if v = z x z 0 R = F x z · ˙ T z × ˙ f G
289 1 2 3 26 4 5 6 7 8 9 277 278 279 280 281 25 211 212 evlslem3 φ x B y B z D w D E v D if v = w y w 0 R = F y w · ˙ T w × ˙ f G
290 288 289 oveq12d φ x B y B z D w D E v D if v = z x z 0 R · ˙ E v D if v = w y w 0 R = F x z · ˙ T z × ˙ f G · ˙ F y w · ˙ T w × ˙ f G
291 276 287 290 3eqtr4d φ x B y B z D w D E v D if v = z + f w x z R y w 0 R = E v D if v = z x z 0 R · ˙ E v D if v = w y w 0 R
292 1 2 7 25 4 10 11 12 200 291 evlslem2 φ x B y B E x P y = E x · ˙ E y
293 2 16 17 18 7 20 21 87 292 3 88 89 109 199 isrhmd φ E P RingHom S
294 ovex S b D F p b · ˙ T b × ˙ f G V
295 294 9 fnmpti E Fn B
296 295 a1i φ E Fn B
297 26 2 rhmf A R RingHom P A : Base R B
298 81 297 syl φ A : Base R B
299 298 ffnd φ A Fn Base R
300 298 frnd φ ran A B
301 fnco E Fn B A Fn Base R ran A B E A Fn Base R
302 296 299 300 301 syl3anc φ E A Fn Base R
303 63 ffnd φ F Fn Base R
304 fvco2 A Fn Base R x Base R E A x = E A x
305 299 304 sylan φ x Base R E A x = E A x
306 305 68 eqtrd φ x Base R E A x = F x
307 302 303 306 eqfnfvd φ E A = F
308 1 8 2 10 19 mvrf2 φ V : I B
309 308 ffnd φ V Fn I
310 308 frnd φ ran V B
311 fnco E Fn B V Fn I ran V B E V Fn I
312 296 309 310 311 syl3anc φ E V Fn I
313 fvco2 V Fn I x I E V x = E V x
314 309 313 sylan φ x I E V x = E V x
315 10 adantr φ x I I W
316 11 adantr φ x I R CRing
317 simpr φ x I x I
318 8 4 25 70 315 316 317 mvrval φ x I V x = y D if y = z I if z = x 1 0 1 R 0 R
319 318 fveq2d φ x I E V x = E y D if y = z I if z = x 1 0 1 R 0 R
320 12 adantr φ x I S CRing
321 13 adantr φ x I F R RingHom S
322 14 adantr φ x I G : I C
323 4 psrbagsn I W z I if z = x 1 0 D
324 10 323 syl φ z I if z = x 1 0 D
325 324 adantr φ x I z I if z = x 1 0 D
326 72 adantr φ x I 1 R Base R
327 1 2 3 26 4 5 6 7 8 9 315 316 320 321 322 25 325 326 evlslem3 φ x I E y D if y = z I if z = x 1 0 1 R 0 R = F 1 R · ˙ T z I if z = x 1 0 × ˙ f G
328 86 adantr φ x I F 1 R = 1 S
329 1nn0 1 0
330 0nn0 0 0
331 329 330 ifcli if z = x 1 0 0
332 331 a1i φ z I if z = x 1 0 0
333 14 ffvelcdmda φ z I G z C
334 eqidd φ z I if z = x 1 0 = z I if z = x 1 0
335 14 feqmptd φ G = z I G z
336 10 332 333 334 335 offval2 φ z I if z = x 1 0 × ˙ f G = z I if z = x 1 0 × ˙ G z
337 oveq1 1 = if z = x 1 0 1 × ˙ G z = if z = x 1 0 × ˙ G z
338 337 eqeq1d 1 = if z = x 1 0 1 × ˙ G z = if z = x G z 1 S if z = x 1 0 × ˙ G z = if z = x G z 1 S
339 oveq1 0 = if z = x 1 0 0 × ˙ G z = if z = x 1 0 × ˙ G z
340 339 eqeq1d 0 = if z = x 1 0 0 × ˙ G z = if z = x G z 1 S if z = x 1 0 × ˙ G z = if z = x G z 1 S
341 333 adantr φ z I z = x G z C
342 47 6 mulg1 G z C 1 × ˙ G z = G z
343 341 342 syl φ z I z = x 1 × ˙ G z = G z
344 iftrue z = x if z = x G z 1 S = G z
345 344 adantl φ z I z = x if z = x G z 1 S = G z
346 343 345 eqtr4d φ z I z = x 1 × ˙ G z = if z = x G z 1 S
347 47 48 6 mulg0 G z C 0 × ˙ G z = 1 S
348 333 347 syl φ z I 0 × ˙ G z = 1 S
349 348 adantr φ z I ¬ z = x 0 × ˙ G z = 1 S
350 iffalse ¬ z = x if z = x G z 1 S = 1 S
351 350 adantl φ z I ¬ z = x if z = x G z 1 S = 1 S
352 349 351 eqtr4d φ z I ¬ z = x 0 × ˙ G z = if z = x G z 1 S
353 338 340 346 352 ifbothda φ z I if z = x 1 0 × ˙ G z = if z = x G z 1 S
354 353 mpteq2dva φ z I if z = x 1 0 × ˙ G z = z I if z = x G z 1 S
355 336 354 eqtrd φ z I if z = x 1 0 × ˙ f G = z I if z = x G z 1 S
356 355 adantr φ x I z I if z = x 1 0 × ˙ f G = z I if z = x G z 1 S
357 356 oveq2d φ x I T z I if z = x 1 0 × ˙ f G = T z I if z = x G z 1 S
358 56 adantr φ x I T Mnd
359 333 adantlr φ x I z I G z C
360 3 17 ringidcl S Ring 1 S C
361 21 360 syl φ 1 S C
362 361 ad2antrr φ x I z I 1 S C
363 359 362 ifcld φ x I z I if z = x G z 1 S C
364 363 fmpttd φ x I z I if z = x G z 1 S : I C
365 eldifsnneq z I x ¬ z = x
366 365 350 syl z I x if z = x G z 1 S = 1 S
367 366 adantl φ x I z I x if z = x G z 1 S = 1 S
368 367 315 suppss2 φ x I z I if z = x G z 1 S supp 1 S x
369 47 48 358 315 317 364 368 gsumpt φ x I T z I if z = x G z 1 S = z I if z = x G z 1 S x
370 fveq2 z = x G z = G x
371 344 370 eqtrd z = x if z = x G z 1 S = G x
372 eqid z I if z = x G z 1 S = z I if z = x G z 1 S
373 fvex G x V
374 371 372 373 fvmpt x I z I if z = x G z 1 S x = G x
375 374 adantl φ x I z I if z = x G z 1 S x = G x
376 357 369 375 3eqtrd φ x I T z I if z = x 1 0 × ˙ f G = G x
377 328 376 oveq12d φ x I F 1 R · ˙ T z I if z = x 1 0 × ˙ f G = 1 S · ˙ G x
378 3 7 17 ringlidm S Ring G x C 1 S · ˙ G x = G x
379 21 46 378 syl2an2r φ x I 1 S · ˙ G x = G x
380 377 379 eqtrd φ x I F 1 R · ˙ T z I if z = x 1 0 × ˙ f G = G x
381 319 327 380 3eqtrd φ x I E V x = G x
382 314 381 eqtrd φ x I E V x = G x
383 312 246 382 eqfnfvd φ E V = G
384 293 307 383 3jca φ E P RingHom S E A = F E V = G