Metamath Proof Explorer

Theorem evlslem2

Description: A linear function on the polynomial ring which is multiplicative on scaled monomials is generally multiplicative. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 11-Apr-2024)

Ref Expression
Hypotheses evlslem2.p ⊢P=ImPolyR
evlslem2.b ⊢B=BaseP
evlslem2.m ⊢·˙=⋅S
evlslem2.z ⊢0˙=0R
evlslem2.d ⊢D=h∈ℕ0I|h-1ℕ∈Fin
evlslem2.i ⊢φ→I∈W
evlslem2.r ⊢φ→R∈CRing
evlslem2.s ⊢φ→S∈CRing
evlslem2.e1 ⊢φ→E∈PGrpHomS
evlslem2.e2 ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→E⁡k∈D⟼ifk=j+fix⁡j⋅Ry⁡i0˙=E⁡k∈D⟼ifk=jx⁡j0˙·˙E⁡k∈D⟼ifk=iy⁡i0˙
Assertion evlslem2 ⊢φ∧x∈B∧y∈B→E⁡x⋅Py=E⁡x·˙E⁡y

Proof

Step Hyp Ref Expression
1 evlslem2.p ⊢P=ImPolyR
2 evlslem2.b ⊢B=BaseP
3 evlslem2.m ⊢·˙=⋅S
4 evlslem2.z ⊢0˙=0R
5 evlslem2.d ⊢D=h∈ℕ0I|h-1ℕ∈Fin
6 evlslem2.i ⊢φ→I∈W
7 evlslem2.r ⊢φ→R∈CRing
8 evlslem2.s ⊢φ→S∈CRing
9 evlslem2.e1 ⊢φ→E∈PGrpHomS
10 evlslem2.e2 ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→E⁡k∈D⟼ifk=j+fix⁡j⋅Ry⁡i0˙=E⁡k∈D⟼ifk=jx⁡j0˙·˙E⁡k∈D⟼ifk=iy⁡i0˙
11 eqid ⊢⋅P=⋅P
12 eqid ⊢0P=0P
13 ovex ⊢ℕ0I∈V
14 5 13 rabex2 ⊢D∈V
15 14 a1i ⊢φ∧x∈B∧y∈B→D∈V
16 crngring ⊢R∈CRing→R∈Ring
17 7 16 syl ⊢φ→R∈Ring
18 1 mplring ⊢I∈W∧R∈Ring→P∈Ring
19 6 17 18 syl2anc ⊢φ→P∈Ring
20 19 adantr ⊢φ∧x∈B∧y∈B→P∈Ring
21 eqid ⊢BaseR=BaseR
22 6 ad2antrr ⊢φ∧x∈B∧y∈B∧j∈D→I∈W
23 17 ad2antrr ⊢φ∧x∈B∧y∈B∧j∈D→R∈Ring
24 simprl ⊢φ∧x∈B∧y∈B→x∈B
25 1 21 2 5 24 mplelf ⊢φ∧x∈B∧y∈B→x:D⟶BaseR
26 25 ffvelcdmda ⊢φ∧x∈B∧y∈B∧j∈D→x⁡j∈BaseR
27 simpr ⊢φ∧x∈B∧y∈B∧j∈D→j∈D
28 1 5 4 21 22 23 2 26 27 mplmon2cl ⊢φ∧x∈B∧y∈B∧j∈D→k∈D⟼ifk=jx⁡j0˙∈B
29 6 ad2antrr ⊢φ∧x∈B∧y∈B∧i∈D→I∈W
30 17 ad2antrr ⊢φ∧x∈B∧y∈B∧i∈D→R∈Ring
31 simprr ⊢φ∧x∈B∧y∈B→y∈B
32 1 21 2 5 31 mplelf ⊢φ∧x∈B∧y∈B→y:D⟶BaseR
33 32 ffvelcdmda ⊢φ∧x∈B∧y∈B∧i∈D→y⁡i∈BaseR
34 simpr ⊢φ∧x∈B∧y∈B∧i∈D→i∈D
35 1 5 4 21 29 30 2 33 34 mplmon2cl ⊢φ∧x∈B∧y∈B∧i∈D→k∈D⟼ifk=iy⁡i0˙∈B
36 14 mptex ⊢j∈D⟼k∈D⟼ifk=jy⁡j0˙∈V
37 funmpt ⊢Fun⁡j∈D⟼k∈D⟼ifk=jy⁡j0˙
38 fvex ⊢0P∈V
39 36 37 38 3pm3.2i ⊢j∈D⟼k∈D⟼ifk=jy⁡j0˙∈V∧Fun⁡j∈D⟼k∈D⟼ifk=jy⁡j0˙∧0P∈V
40 39 a1i ⊢φ∧y∈B→j∈D⟼k∈D⟼ifk=jy⁡j0˙∈V∧Fun⁡j∈D⟼k∈D⟼ifk=jy⁡j0˙∧0P∈V
41 simpr ⊢φ∧y∈B→y∈B
42 7 adantr ⊢φ∧y∈B→R∈CRing
43 1 2 4 41 42 mplelsfi ⊢φ∧y∈B→finSupp0˙⁡y
44 43 fsuppimpd ⊢φ∧y∈B→ysupp0˙∈Fin
45 1 21 2 5 41 mplelf ⊢φ∧y∈B→y:D⟶BaseR
46 ssidd ⊢φ∧y∈B→ysupp0˙⊆ysupp0˙
47 14 a1i ⊢φ∧y∈B→D∈V
48 4 fvexi ⊢0˙∈V
49 48 a1i ⊢φ∧y∈B→0˙∈V
50 45 46 47 49 suppssr ⊢φ∧y∈B∧j∈D∖supp0˙⁡y→y⁡j=0˙
51 50 ifeq1d ⊢φ∧y∈B∧j∈D∖supp0˙⁡y→ifk=jy⁡j0˙=ifk=j0˙0˙
52 ifid ⊢ifk=j0˙0˙=0˙
53 51 52 eqtrdi ⊢φ∧y∈B∧j∈D∖supp0˙⁡y→ifk=jy⁡j0˙=0˙
54 53 mpteq2dv ⊢φ∧y∈B∧j∈D∖supp0˙⁡y→k∈D⟼ifk=jy⁡j0˙=k∈D⟼0˙
55 ringgrp ⊢R∈Ring→R∈Grp
56 17 55 syl ⊢φ→R∈Grp
57 1 5 4 12 6 56 mpl0 ⊢φ→0P=D×0˙
58 fconstmpt ⊢D×0˙=k∈D⟼0˙
59 57 58 eqtrdi ⊢φ→0P=k∈D⟼0˙
60 59 ad2antrr ⊢φ∧y∈B∧j∈D∖supp0˙⁡y→0P=k∈D⟼0˙
61 54 60 eqtr4d ⊢φ∧y∈B∧j∈D∖supp0˙⁡y→k∈D⟼ifk=jy⁡j0˙=0P
62 61 47 suppss2 ⊢φ∧y∈B→j∈D⟼k∈D⟼ifk=jy⁡j0˙supp0P⊆ysupp0˙
63 suppssfifsupp ⊢j∈D⟼k∈D⟼ifk=jy⁡j0˙∈V∧Fun⁡j∈D⟼k∈D⟼ifk=jy⁡j0˙∧0P∈V∧ysupp0˙∈Fin∧j∈D⟼k∈D⟼ifk=jy⁡j0˙supp0P⊆ysupp0˙→finSupp0P⁡j∈D⟼k∈D⟼ifk=jy⁡j0˙
64 40 44 62 63 syl12anc ⊢φ∧y∈B→finSupp0P⁡j∈D⟼k∈D⟼ifk=jy⁡j0˙
65 64 ralrimiva ⊢φ→∀y∈BfinSupp0P⁡j∈D⟼k∈D⟼ifk=jy⁡j0˙
66 fveq1 ⊢y=x→y⁡j=x⁡j
67 66 ifeq1d ⊢y=x→ifk=jy⁡j0˙=ifk=jx⁡j0˙
68 67 mpteq2dv ⊢y=x→k∈D⟼ifk=jy⁡j0˙=k∈D⟼ifk=jx⁡j0˙
69 68 mpteq2dv ⊢y=x→j∈D⟼k∈D⟼ifk=jy⁡j0˙=j∈D⟼k∈D⟼ifk=jx⁡j0˙
70 69 breq1d ⊢y=x→finSupp0P⁡j∈D⟼k∈D⟼ifk=jy⁡j0˙↔finSupp0P⁡j∈D⟼k∈D⟼ifk=jx⁡j0˙
71 70 cbvralvw ⊢∀y∈BfinSupp0P⁡j∈D⟼k∈D⟼ifk=jy⁡j0˙↔∀x∈BfinSupp0P⁡j∈D⟼k∈D⟼ifk=jx⁡j0˙
72 65 71 sylib ⊢φ→∀x∈BfinSupp0P⁡j∈D⟼k∈D⟼ifk=jx⁡j0˙
73 72 r19.21bi ⊢φ∧x∈B→finSupp0P⁡j∈D⟼k∈D⟼ifk=jx⁡j0˙
74 73 adantrr ⊢φ∧x∈B∧y∈B→finSupp0P⁡j∈D⟼k∈D⟼ifk=jx⁡j0˙
75 equequ2 ⊢i=j→k=i↔k=j
76 fveq2 ⊢i=j→y⁡i=y⁡j
77 75 76 ifbieq1d ⊢i=j→ifk=iy⁡i0˙=ifk=jy⁡j0˙
78 77 mpteq2dv ⊢i=j→k∈D⟼ifk=iy⁡i0˙=k∈D⟼ifk=jy⁡j0˙
79 78 cbvmptv ⊢i∈D⟼k∈D⟼ifk=iy⁡i0˙=j∈D⟼k∈D⟼ifk=jy⁡j0˙
80 64 adantrl ⊢φ∧x∈B∧y∈B→finSupp0P⁡j∈D⟼k∈D⟼ifk=jy⁡j0˙
81 79 80 eqbrtrid ⊢φ∧x∈B∧y∈B→finSupp0P⁡i∈D⟼k∈D⟼ifk=iy⁡i0˙
82 2 11 12 15 15 20 28 35 74 81 gsumdixp ⊢φ∧x∈B∧y∈B→∑Pj∈Dk∈D⟼ifk=jx⁡j0˙⋅P∑Pi∈Dk∈D⟼ifk=iy⁡i0˙=∑Pj∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙
83 82 fveq2d ⊢φ∧x∈B∧y∈B→E⁡∑Pj∈Dk∈D⟼ifk=jx⁡j0˙⋅P∑Pi∈Dk∈D⟼ifk=iy⁡i0˙=E⁡∑Pj∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙
84 ringcmn ⊢P∈Ring→P∈CMnd
85 19 84 syl ⊢φ→P∈CMnd
86 85 adantr ⊢φ∧x∈B∧y∈B→P∈CMnd
87 crngring ⊢S∈CRing→S∈Ring
88 8 87 syl ⊢φ→S∈Ring
89 88 adantr ⊢φ∧x∈B∧y∈B→S∈Ring
90 ringmnd ⊢S∈Ring→S∈Mnd
91 89 90 syl ⊢φ∧x∈B∧y∈B→S∈Mnd
92 14 14 xpex ⊢D×D∈V
93 92 a1i ⊢φ∧x∈B∧y∈B→D×D∈V
94 ghmmhm ⊢E∈PGrpHomS→E∈PMndHomS
95 9 94 syl ⊢φ→E∈PMndHomS
96 95 adantr ⊢φ∧x∈B∧y∈B→E∈PMndHomS
97 19 ad2antrr ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→P∈Ring
98 28 adantrr ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→k∈D⟼ifk=jx⁡j0˙∈B
99 35 adantrl ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→k∈D⟼ifk=iy⁡i0˙∈B
100 2 11 ringcl ⊢P∈Ring∧k∈D⟼ifk=jx⁡j0˙∈B∧k∈D⟼ifk=iy⁡i0˙∈B→k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙∈B
101 97 98 99 100 syl3anc ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙∈B
102 101 ralrimivva ⊢φ∧x∈B∧y∈B→∀j∈D∀i∈Dk∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙∈B
103 eqid ⊢j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙=j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙
104 103 fmpo ⊢∀j∈D∀i∈Dk∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙∈B↔j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙:D×D⟶B
105 102 104 sylib ⊢φ∧x∈B∧y∈B→j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙:D×D⟶B
106 14 14 mpoex ⊢j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙∈V
107 103 mpofun ⊢Fun⁡j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙
108 106 107 38 3pm3.2i ⊢j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙∈V∧Fun⁡j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙∧0P∈V
109 108 a1i ⊢φ∧x∈B∧y∈B→j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙∈V∧Fun⁡j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙∧0P∈V
110 74 fsuppimpd ⊢φ∧x∈B∧y∈B→j∈D⟼k∈D⟼ifk=jx⁡j0˙supp0P∈Fin
111 81 fsuppimpd ⊢φ∧x∈B∧y∈B→i∈D⟼k∈D⟼ifk=iy⁡i0˙supp0P∈Fin
112 xpfi ⊢j∈D⟼k∈D⟼ifk=jx⁡j0˙supp0P∈Fin∧i∈D⟼k∈D⟼ifk=iy⁡i0˙supp0P∈Fin→supp0P⁡j∈D⟼k∈D⟼ifk=jx⁡j0˙×supp0P⁡i∈D⟼k∈D⟼ifk=iy⁡i0˙∈Fin
113 110 111 112 syl2anc ⊢φ∧x∈B∧y∈B→supp0P⁡j∈D⟼k∈D⟼ifk=jx⁡j0˙×supp0P⁡i∈D⟼k∈D⟼ifk=iy⁡i0˙∈Fin
114 2 12 11 20 28 35 15 15 evlslem4 ⊢φ∧x∈B∧y∈B→j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙supp0P⊆supp0P⁡j∈D⟼k∈D⟼ifk=jx⁡j0˙×supp0P⁡i∈D⟼k∈D⟼ifk=iy⁡i0˙
115 suppssfifsupp ⊢j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙∈V∧Fun⁡j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙∧0P∈V∧supp0P⁡j∈D⟼k∈D⟼ifk=jx⁡j0˙×supp0P⁡i∈D⟼k∈D⟼ifk=iy⁡i0˙∈Fin∧j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙supp0P⊆supp0P⁡j∈D⟼k∈D⟼ifk=jx⁡j0˙×supp0P⁡i∈D⟼k∈D⟼ifk=iy⁡i0˙→finSupp0P⁡j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙
116 109 113 114 115 syl12anc ⊢φ∧x∈B∧y∈B→finSupp0P⁡j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙
117 2 12 86 91 93 96 105 116 gsummhm ⊢φ∧x∈B∧y∈B→∑SE∘j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙=E⁡∑Pj∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙
118 6 ad2antrr ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→I∈W
119 7 ad2antrr ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→R∈CRing
120 eqid ⊢⋅R=⋅R
121 simprl ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→j∈D
122 simprr ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→i∈D
123 26 adantrr ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→x⁡j∈BaseR
124 33 adantrl ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→y⁡i∈BaseR
125 1 5 4 21 118 119 11 120 121 122 123 124 mplmon2mul ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙=k∈D⟼ifk=j+fix⁡j⋅Ry⁡i0˙
126 125 fveq2d ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→E⁡k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙=E⁡k∈D⟼ifk=j+fix⁡j⋅Ry⁡i0˙
127 10 anassrs ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→E⁡k∈D⟼ifk=j+fix⁡j⋅Ry⁡i0˙=E⁡k∈D⟼ifk=jx⁡j0˙·˙E⁡k∈D⟼ifk=iy⁡i0˙
128 126 127 eqtrd ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→E⁡k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙=E⁡k∈D⟼ifk=jx⁡j0˙·˙E⁡k∈D⟼ifk=iy⁡i0˙
129 128 3impb ⊢φ∧x∈B∧y∈B∧j∈D∧i∈D→E⁡k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙=E⁡k∈D⟼ifk=jx⁡j0˙·˙E⁡k∈D⟼ifk=iy⁡i0˙
130 129 mpoeq3dva ⊢φ∧x∈B∧y∈B→j∈D,i∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙=j∈D,i∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙·˙E⁡k∈D⟼ifk=iy⁡i0˙
131 130 oveq2d ⊢φ∧x∈B∧y∈B→∑Sj∈D,i∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙=∑Sj∈D,i∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙·˙E⁡k∈D⟼ifk=iy⁡i0˙
132 eqidd ⊢φ∧x∈B∧y∈B→j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙=j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙
133 eqid ⊢BaseS=BaseS
134 2 133 ghmf ⊢E∈PGrpHomS→E:B⟶BaseS
135 9 134 syl ⊢φ→E:B⟶BaseS
136 135 feqmptd ⊢φ→E=z∈B⟼E⁡z
137 136 adantr ⊢φ∧x∈B∧y∈B→E=z∈B⟼E⁡z
138 fveq2 ⊢z=k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙→E⁡z=E⁡k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙
139 101 132 137 138 fmpoco ⊢φ∧x∈B∧y∈B→E∘j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙=j∈D,i∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙
140 139 oveq2d ⊢φ∧x∈B∧y∈B→∑SE∘j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙=∑Sj∈D,i∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙
141 eqidd ⊢φ∧x∈B∧y∈B→j∈D⟼k∈D⟼ifk=jx⁡j0˙=j∈D⟼k∈D⟼ifk=jx⁡j0˙
142 fveq2 ⊢z=k∈D⟼ifk=jx⁡j0˙→E⁡z=E⁡k∈D⟼ifk=jx⁡j0˙
143 28 141 137 142 fmptco ⊢φ∧x∈B∧y∈B→E∘j∈D⟼k∈D⟼ifk=jx⁡j0˙=j∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙
144 143 oveq2d ⊢φ∧x∈B∧y∈B→∑SE∘j∈D⟼k∈D⟼ifk=jx⁡j0˙=∑Sj∈DE⁡k∈D⟼ifk=jx⁡j0˙
145 eqidd ⊢φ∧x∈B∧y∈B→i∈D⟼k∈D⟼ifk=iy⁡i0˙=i∈D⟼k∈D⟼ifk=iy⁡i0˙
146 fveq2 ⊢z=k∈D⟼ifk=iy⁡i0˙→E⁡z=E⁡k∈D⟼ifk=iy⁡i0˙
147 35 145 137 146 fmptco ⊢φ∧x∈B∧y∈B→E∘i∈D⟼k∈D⟼ifk=iy⁡i0˙=i∈D⟼E⁡k∈D⟼ifk=iy⁡i0˙
148 147 oveq2d ⊢φ∧x∈B∧y∈B→∑SE∘i∈D⟼k∈D⟼ifk=iy⁡i0˙=∑Si∈DE⁡k∈D⟼ifk=iy⁡i0˙
149 144 148 oveq12d ⊢φ∧x∈B∧y∈B→∑SE∘j∈D⟼k∈D⟼ifk=jx⁡j0˙·˙∑SE∘i∈D⟼k∈D⟼ifk=iy⁡i0˙=∑Sj∈DE⁡k∈D⟼ifk=jx⁡j0˙·˙∑Si∈DE⁡k∈D⟼ifk=iy⁡i0˙
150 eqid ⊢0S=0S
151 135 ad2antrr ⊢φ∧x∈B∧y∈B∧j∈D→E:B⟶BaseS
152 151 28 ffvelcdmd ⊢φ∧x∈B∧y∈B∧j∈D→E⁡k∈D⟼ifk=jx⁡j0˙∈BaseS
153 135 ad2antrr ⊢φ∧x∈B∧y∈B∧i∈D→E:B⟶BaseS
154 153 35 ffvelcdmd ⊢φ∧x∈B∧y∈B∧i∈D→E⁡k∈D⟼ifk=iy⁡i0˙∈BaseS
155 14 mptex ⊢j∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙∈V
156 funmpt ⊢Fun⁡j∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙
157 fvex ⊢0S∈V
158 155 156 157 3pm3.2i ⊢j∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙∈V∧Fun⁡j∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙∧0S∈V
159 158 a1i ⊢φ∧x∈B∧y∈B→j∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙∈V∧Fun⁡j∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙∧0S∈V
160 ssidd ⊢φ→j∈D⟼k∈D⟼ifk=jx⁡j0˙supp0P⊆j∈D⟼k∈D⟼ifk=jx⁡j0˙supp0P
161 12 150 ghmid ⊢E∈PGrpHomS→E⁡0P=0S
162 9 161 syl ⊢φ→E⁡0P=0S
163 14 mptex ⊢k∈D⟼ifk=jx⁡j0˙∈V
164 163 a1i ⊢φ∧j∈D→k∈D⟼ifk=jx⁡j0˙∈V
165 38 a1i ⊢φ→0P∈V
166 160 162 164 165 suppssfv ⊢φ→j∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙supp0S⊆j∈D⟼k∈D⟼ifk=jx⁡j0˙supp0P
167 166 adantr ⊢φ∧x∈B∧y∈B→j∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙supp0S⊆j∈D⟼k∈D⟼ifk=jx⁡j0˙supp0P
168 suppssfifsupp ⊢j∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙∈V∧Fun⁡j∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙∧0S∈V∧j∈D⟼k∈D⟼ifk=jx⁡j0˙supp0P∈Fin∧j∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙supp0S⊆j∈D⟼k∈D⟼ifk=jx⁡j0˙supp0P→finSupp0S⁡j∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙
169 159 110 167 168 syl12anc ⊢φ∧x∈B∧y∈B→finSupp0S⁡j∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙
170 14 mptex ⊢i∈D⟼E⁡k∈D⟼ifk=iy⁡i0˙∈V
171 funmpt ⊢Fun⁡i∈D⟼E⁡k∈D⟼ifk=iy⁡i0˙
172 170 171 157 3pm3.2i ⊢i∈D⟼E⁡k∈D⟼ifk=iy⁡i0˙∈V∧Fun⁡i∈D⟼E⁡k∈D⟼ifk=iy⁡i0˙∧0S∈V
173 172 a1i ⊢φ∧x∈B∧y∈B→i∈D⟼E⁡k∈D⟼ifk=iy⁡i0˙∈V∧Fun⁡i∈D⟼E⁡k∈D⟼ifk=iy⁡i0˙∧0S∈V
174 ssidd ⊢φ→i∈D⟼k∈D⟼ifk=iy⁡i0˙supp0P⊆i∈D⟼k∈D⟼ifk=iy⁡i0˙supp0P
175 14 mptex ⊢k∈D⟼ifk=iy⁡i0˙∈V
176 175 a1i ⊢φ∧i∈D→k∈D⟼ifk=iy⁡i0˙∈V
177 174 162 176 165 suppssfv ⊢φ→i∈D⟼E⁡k∈D⟼ifk=iy⁡i0˙supp0S⊆i∈D⟼k∈D⟼ifk=iy⁡i0˙supp0P
178 177 adantr ⊢φ∧x∈B∧y∈B→i∈D⟼E⁡k∈D⟼ifk=iy⁡i0˙supp0S⊆i∈D⟼k∈D⟼ifk=iy⁡i0˙supp0P
179 suppssfifsupp ⊢i∈D⟼E⁡k∈D⟼ifk=iy⁡i0˙∈V∧Fun⁡i∈D⟼E⁡k∈D⟼ifk=iy⁡i0˙∧0S∈V∧i∈D⟼k∈D⟼ifk=iy⁡i0˙supp0P∈Fin∧i∈D⟼E⁡k∈D⟼ifk=iy⁡i0˙supp0S⊆i∈D⟼k∈D⟼ifk=iy⁡i0˙supp0P→finSupp0S⁡i∈D⟼E⁡k∈D⟼ifk=iy⁡i0˙
180 173 111 178 179 syl12anc ⊢φ∧x∈B∧y∈B→finSupp0S⁡i∈D⟼E⁡k∈D⟼ifk=iy⁡i0˙
181 133 3 150 15 15 89 152 154 169 180 gsumdixp ⊢φ∧x∈B∧y∈B→∑Sj∈DE⁡k∈D⟼ifk=jx⁡j0˙·˙∑Si∈DE⁡k∈D⟼ifk=iy⁡i0˙=∑Sj∈D,i∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙·˙E⁡k∈D⟼ifk=iy⁡i0˙
182 149 181 eqtrd ⊢φ∧x∈B∧y∈B→∑SE∘j∈D⟼k∈D⟼ifk=jx⁡j0˙·˙∑SE∘i∈D⟼k∈D⟼ifk=iy⁡i0˙=∑Sj∈D,i∈D⟼E⁡k∈D⟼ifk=jx⁡j0˙·˙E⁡k∈D⟼ifk=iy⁡i0˙
183 131 140 182 3eqtr4d ⊢φ∧x∈B∧y∈B→∑SE∘j∈D,i∈D⟼k∈D⟼ifk=jx⁡j0˙⋅Pk∈D⟼ifk=iy⁡i0˙=∑SE∘j∈D⟼k∈D⟼ifk=jx⁡j0˙·˙∑SE∘i∈D⟼k∈D⟼ifk=iy⁡i0˙
184 83 117 183 3eqtr2d ⊢φ∧x∈B∧y∈B→E⁡∑Pj∈Dk∈D⟼ifk=jx⁡j0˙⋅P∑Pi∈Dk∈D⟼ifk=iy⁡i0˙=∑SE∘j∈D⟼k∈D⟼ifk=jx⁡j0˙·˙∑SE∘i∈D⟼k∈D⟼ifk=iy⁡i0˙
185 6 adantr ⊢φ∧x∈B∧y∈B→I∈W
186 17 adantr ⊢φ∧x∈B∧y∈B→R∈Ring
187 1 5 4 2 185 186 24 mplcoe4 ⊢φ∧x∈B∧y∈B→x=∑Pj∈Dk∈D⟼ifk=jx⁡j0˙
188 1 5 4 2 185 186 31 mplcoe4 ⊢φ∧x∈B∧y∈B→y=∑Pi∈Dk∈D⟼ifk=iy⁡i0˙
189 187 188 oveq12d ⊢φ∧x∈B∧y∈B→x⋅Py=∑Pj∈Dk∈D⟼ifk=jx⁡j0˙⋅P∑Pi∈Dk∈D⟼ifk=iy⁡i0˙
190 189 fveq2d ⊢φ∧x∈B∧y∈B→E⁡x⋅Py=E⁡∑Pj∈Dk∈D⟼ifk=jx⁡j0˙⋅P∑Pi∈Dk∈D⟼ifk=iy⁡i0˙
191 187 fveq2d ⊢φ∧x∈B∧y∈B→E⁡x=E⁡∑Pj∈Dk∈D⟼ifk=jx⁡j0˙
192 28 fmpttd ⊢φ∧x∈B∧y∈B→j∈D⟼k∈D⟼ifk=jx⁡j0˙:D⟶B
193 2 12 86 91 15 96 192 74 gsummhm ⊢φ∧x∈B∧y∈B→∑SE∘j∈D⟼k∈D⟼ifk=jx⁡j0˙=E⁡∑Pj∈Dk∈D⟼ifk=jx⁡j0˙
194 191 193 eqtr4d ⊢φ∧x∈B∧y∈B→E⁡x=∑SE∘j∈D⟼k∈D⟼ifk=jx⁡j0˙
195 188 fveq2d ⊢φ∧x∈B∧y∈B→E⁡y=E⁡∑Pi∈Dk∈D⟼ifk=iy⁡i0˙
196 35 fmpttd ⊢φ∧x∈B∧y∈B→i∈D⟼k∈D⟼ifk=iy⁡i0˙:D⟶B
197 2 12 86 91 15 96 196 81 gsummhm ⊢φ∧x∈B∧y∈B→∑SE∘i∈D⟼k∈D⟼ifk=iy⁡i0˙=E⁡∑Pi∈Dk∈D⟼ifk=iy⁡i0˙
198 195 197 eqtr4d ⊢φ∧x∈B∧y∈B→E⁡y=∑SE∘i∈D⟼k∈D⟼ifk=iy⁡i0˙
199 194 198 oveq12d ⊢φ∧x∈B∧y∈B→E⁡x·˙E⁡y=∑SE∘j∈D⟼k∈D⟼ifk=jx⁡j0˙·˙∑SE∘i∈D⟼k∈D⟼ifk=iy⁡i0˙
200 184 190 199 3eqtr4d ⊢φ∧x∈B∧y∈B→E⁡x⋅Py=E⁡x·˙E⁡y