Metamath Proof Explorer

Theorem selvvvval

Description: Recover the original polynomial from a selectVars application. (Contributed by SN, 15-Mar-2025)

Ref Expression
Hypotheses selvvvval.d ⊢D=h∈ℕ0I|h-1ℕ∈Fin
selvvvval.p ⊢P=ImPolyR
selvvvval.b ⊢B=BaseP
selvvvval.i ⊢φ→I∈V
selvvvval.r ⊢φ→R∈CRing
selvvvval.j ⊢φ→J⊆I
selvvvval.f ⊢φ→F∈B
selvvvval.y ⊢φ→Y∈D
Assertion selvvvval ⊢φ→IselectVarsR⁡J⁡F⁡Y↾J⁡Y↾I∖J=F⁡Y

Proof

Step Hyp Ref Expression
1 selvvvval.d ⊢D=h∈ℕ0I|h-1ℕ∈Fin
2 selvvvval.p ⊢P=ImPolyR
3 selvvvval.b ⊢B=BaseP
4 selvvvval.i ⊢φ→I∈V
5 selvvvval.r ⊢φ→R∈CRing
6 selvvvval.j ⊢φ→J⊆I
7 selvvvval.f ⊢φ→F∈B
8 selvvvval.y ⊢φ→Y∈D
9 eqid ⊢I∖JmPolyR=I∖JmPolyR
10 eqid ⊢JmPolyI∖JmPolyR=JmPolyI∖JmPolyR
11 eqid ⊢algSc⁡JmPolyI∖JmPolyR=algSc⁡JmPolyI∖JmPolyR
12 eqid ⊢algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR=algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR
13 2 3 9 10 11 12 4 5 6 7 selvval2 ⊢φ→IselectVarsR⁡J⁡F=IevalJmPolyI∖JmPolyR⁡algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∘F⁡z∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z
14 eqid ⊢IevalJmPolyI∖JmPolyR=IevalJmPolyI∖JmPolyR
15 eqid ⊢ImPolyJmPolyI∖JmPolyR=ImPolyJmPolyI∖JmPolyR
16 eqid ⊢BaseImPolyJmPolyI∖JmPolyR=BaseImPolyJmPolyI∖JmPolyR
17 eqid ⊢BaseJmPolyI∖JmPolyR=BaseJmPolyI∖JmPolyR
18 eqid ⊢mulGrpJmPolyI∖JmPolyR=mulGrpJmPolyI∖JmPolyR
19 eqid ⊢⋅mulGrpJmPolyI∖JmPolyR=⋅mulGrpJmPolyI∖JmPolyR
20 eqid ⊢⋅JmPolyI∖JmPolyR=⋅JmPolyI∖JmPolyR
21 4 6 ssexd ⊢φ→J∈V
22 4 difexd ⊢φ→I∖J∈V
23 9 22 5 mplcrngd ⊢φ→I∖JmPolyR∈CRing
24 10 21 23 mplcrngd ⊢φ→JmPolyI∖JmPolyR∈CRing
25 10 mplassa ⊢J∈V∧I∖JmPolyR∈CRing→JmPolyI∖JmPolyR∈AssAlg
26 21 23 25 syl2anc ⊢φ→JmPolyI∖JmPolyR∈AssAlg
27 eqid ⊢Scalar⁡JmPolyI∖JmPolyR=Scalar⁡JmPolyI∖JmPolyR
28 11 27 asclrhm ⊢JmPolyI∖JmPolyR∈AssAlg→algSc⁡JmPolyI∖JmPolyR∈Scalar⁡JmPolyI∖JmPolyRRingHomJmPolyI∖JmPolyR
29 26 28 syl ⊢φ→algSc⁡JmPolyI∖JmPolyR∈Scalar⁡JmPolyI∖JmPolyRRingHomJmPolyI∖JmPolyR
30 9 mplassa ⊢I∖J∈V∧R∈CRing→I∖JmPolyR∈AssAlg
31 22 5 30 syl2anc ⊢φ→I∖JmPolyR∈AssAlg
32 eqid ⊢algSc⁡I∖JmPolyR=algSc⁡I∖JmPolyR
33 eqid ⊢Scalar⁡I∖JmPolyR=Scalar⁡I∖JmPolyR
34 32 33 asclrhm ⊢I∖JmPolyR∈AssAlg→algSc⁡I∖JmPolyR∈Scalar⁡I∖JmPolyRRingHomI∖JmPolyR
35 31 34 syl ⊢φ→algSc⁡I∖JmPolyR∈Scalar⁡I∖JmPolyRRingHomI∖JmPolyR
36 9 22 5 mplsca ⊢φ→R=Scalar⁡I∖JmPolyR
37 36 eqcomd ⊢φ→Scalar⁡I∖JmPolyR=R
38 10 21 23 mplsca ⊢φ→I∖JmPolyR=Scalar⁡JmPolyI∖JmPolyR
39 37 38 oveq12d ⊢φ→Scalar⁡I∖JmPolyRRingHomI∖JmPolyR=RRingHomScalar⁡JmPolyI∖JmPolyR
40 35 39 eleqtrd ⊢φ→algSc⁡I∖JmPolyR∈RRingHomScalar⁡JmPolyI∖JmPolyR
41 rhmco ⊢algSc⁡JmPolyI∖JmPolyR∈Scalar⁡JmPolyI∖JmPolyRRingHomJmPolyI∖JmPolyR∧algSc⁡I∖JmPolyR∈RRingHomScalar⁡JmPolyI∖JmPolyR→algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∈RRingHomJmPolyI∖JmPolyR
42 29 40 41 syl2anc ⊢φ→algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∈RRingHomJmPolyI∖JmPolyR
43 rhmghm ⊢algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∈RRingHomJmPolyI∖JmPolyR→algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∈RGrpHomJmPolyI∖JmPolyR
44 ghmmhm ⊢algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∈RGrpHomJmPolyI∖JmPolyR→algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∈RMndHomJmPolyI∖JmPolyR
45 42 43 44 3syl ⊢φ→algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∈RMndHomJmPolyI∖JmPolyR
46 2 15 3 16 4 45 7 mhmcompl ⊢φ→algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∘F∈BaseImPolyJmPolyI∖JmPolyR
47 fvexd ⊢φ→BaseJmPolyI∖JmPolyR∈V
48 eqid ⊢JmVarI∖JmPolyR=JmVarI∖JmPolyR
49 23 crngringd ⊢φ→I∖JmPolyR∈Ring
50 10 48 17 21 49 mvrf2 ⊢φ→JmVarI∖JmPolyR:J⟶BaseJmPolyI∖JmPolyR
51 50 ffvelcdmda ⊢φ∧z∈J→JmVarI∖JmPolyR⁡z∈BaseJmPolyI∖JmPolyR
52 51 adantlr ⊢φ∧z∈I∧z∈J→JmVarI∖JmPolyR⁡z∈BaseJmPolyI∖JmPolyR
53 eldif ⊢z∈I∖J↔z∈I∧¬z∈J
54 eqid ⊢BaseI∖JmPolyR=BaseI∖JmPolyR
55 10 17 54 11 21 49 mplasclf ⊢φ→algSc⁡JmPolyI∖JmPolyR:BaseI∖JmPolyR⟶BaseJmPolyI∖JmPolyR
56 55 adantr ⊢φ∧z∈I∖J→algSc⁡JmPolyI∖JmPolyR:BaseI∖JmPolyR⟶BaseJmPolyI∖JmPolyR
57 eqid ⊢I∖JmVarR=I∖JmVarR
58 5 crngringd ⊢φ→R∈Ring
59 9 57 54 22 58 mvrf2 ⊢φ→I∖JmVarR:I∖J⟶BaseI∖JmPolyR
60 59 ffvelcdmda ⊢φ∧z∈I∖J→I∖JmVarR⁡z∈BaseI∖JmPolyR
61 56 60 ffvelcdmd ⊢φ∧z∈I∖J→algSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z∈BaseJmPolyI∖JmPolyR
62 53 61 sylan2br ⊢φ∧z∈I∧¬z∈J→algSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z∈BaseJmPolyI∖JmPolyR
63 62 anassrs ⊢φ∧z∈I∧¬z∈J→algSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z∈BaseJmPolyI∖JmPolyR
64 52 63 ifclda ⊢φ∧z∈I→ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z∈BaseJmPolyI∖JmPolyR
65 64 fmpttd ⊢φ→z∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z:I⟶BaseJmPolyI∖JmPolyR
66 47 4 65 elmapdd ⊢φ→z∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z∈BaseJmPolyI∖JmPolyRI
67 14 15 16 1 17 18 19 20 4 24 46 66 evlvvval ⊢φ→IevalJmPolyI∖JmPolyR⁡algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∘F⁡z∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z=∑JmPolyI∖JmPolyRg∈DalgSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∘F⁡g⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Ig⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k
68 eqid ⊢BaseR=BaseR
69 2 68 3 1 7 mplelf ⊢φ→F:D⟶BaseR
70 69 adantr ⊢φ∧g∈D→F:D⟶BaseR
71 simpr ⊢φ∧g∈D→g∈D
72 70 71 fvco3d ⊢φ∧g∈D→algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∘F⁡g=algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR⁡F⁡g
73 9 54 68 32 22 58 mplasclf ⊢φ→algSc⁡I∖JmPolyR:BaseR⟶BaseI∖JmPolyR
74 73 adantr ⊢φ∧g∈D→algSc⁡I∖JmPolyR:BaseR⟶BaseI∖JmPolyR
75 69 ffvelcdmda ⊢φ∧g∈D→F⁡g∈BaseR
76 74 75 fvco3d ⊢φ∧g∈D→algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR⁡F⁡g=algSc⁡JmPolyI∖JmPolyR⁡algSc⁡I∖JmPolyR⁡F⁡g
77 72 76 eqtrd ⊢φ∧g∈D→algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∘F⁡g=algSc⁡JmPolyI∖JmPolyR⁡algSc⁡I∖JmPolyR⁡F⁡g
78 18 17 mgpbas ⊢BaseJmPolyI∖JmPolyR=BasemulGrpJmPolyI∖JmPolyR
79 eqid ⊢0mulGrpJmPolyI∖JmPolyR=0mulGrpJmPolyI∖JmPolyR
80 18 20 mgpplusg ⊢⋅JmPolyI∖JmPolyR=+mulGrpJmPolyI∖JmPolyR
81 18 crngmgp ⊢JmPolyI∖JmPolyR∈CRing→mulGrpJmPolyI∖JmPolyR∈CMnd
82 24 81 syl ⊢φ→mulGrpJmPolyI∖JmPolyR∈CMnd
83 82 adantr ⊢φ∧g∈D→mulGrpJmPolyI∖JmPolyR∈CMnd
84 4 adantr ⊢φ∧g∈D→I∈V
85 82 cmnmndd ⊢φ→mulGrpJmPolyI∖JmPolyR∈Mnd
86 85 ad2antrr ⊢φ∧g∈D∧k∈I→mulGrpJmPolyI∖JmPolyR∈Mnd
87 1 psrbagf ⊢g∈D→g:I⟶ℕ0
88 87 adantl ⊢φ∧g∈D→g:I⟶ℕ0
89 88 ffvelcdmda ⊢φ∧g∈D∧k∈I→g⁡k∈ℕ0
90 eqid ⊢z∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z=z∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z
91 eleq1w ⊢z=k→z∈J↔k∈J
92 fveq2 ⊢z=k→JmVarI∖JmPolyR⁡z=JmVarI∖JmPolyR⁡k
93 fveq2 ⊢z=k→I∖JmVarR⁡z=I∖JmVarR⁡k
94 93 fveq2d ⊢z=k→algSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z=algSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
95 91 92 94 ifbieq12d ⊢z=k→ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z=ifk∈JJmVarI∖JmPolyR⁡kalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
96 simpr ⊢φ∧g∈D∧k∈I→k∈I
97 50 ffvelcdmda ⊢φ∧k∈J→JmVarI∖JmPolyR⁡k∈BaseJmPolyI∖JmPolyR
98 97 adantlr ⊢φ∧g∈D∧k∈J→JmVarI∖JmPolyR⁡k∈BaseJmPolyI∖JmPolyR
99 98 adantlr ⊢φ∧g∈D∧k∈I∧k∈J→JmVarI∖JmPolyR⁡k∈BaseJmPolyI∖JmPolyR
100 eldif ⊢k∈I∖J↔k∈I∧¬k∈J
101 55 adantr ⊢φ∧k∈I∖J→algSc⁡JmPolyI∖JmPolyR:BaseI∖JmPolyR⟶BaseJmPolyI∖JmPolyR
102 59 ffvelcdmda ⊢φ∧k∈I∖J→I∖JmVarR⁡k∈BaseI∖JmPolyR
103 101 102 ffvelcdmd ⊢φ∧k∈I∖J→algSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k∈BaseJmPolyI∖JmPolyR
104 100 103 sylan2br ⊢φ∧k∈I∧¬k∈J→algSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k∈BaseJmPolyI∖JmPolyR
105 104 anassrs ⊢φ∧k∈I∧¬k∈J→algSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k∈BaseJmPolyI∖JmPolyR
106 105 adantllr ⊢φ∧g∈D∧k∈I∧¬k∈J→algSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k∈BaseJmPolyI∖JmPolyR
107 99 106 ifclda ⊢φ∧g∈D∧k∈I→ifk∈JJmVarI∖JmPolyR⁡kalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k∈BaseJmPolyI∖JmPolyR
108 90 95 96 107 fvmptd3 ⊢φ∧g∈D∧k∈I→z∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=ifk∈JJmVarI∖JmPolyR⁡kalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
109 108 107 eqeltrd ⊢φ∧g∈D∧k∈I→z∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k∈BaseJmPolyI∖JmPolyR
110 78 19 86 89 109 mulgnn0cld ⊢φ∧g∈D∧k∈I→g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k∈BaseJmPolyI∖JmPolyR
111 110 fmpttd ⊢φ∧g∈D→k∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k:I⟶BaseJmPolyI∖JmPolyR
112 4 mptexd ⊢φ→k∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k∈V
113 112 adantr ⊢φ∧g∈D→k∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k∈V
114 fvexd ⊢φ∧g∈D→0mulGrpJmPolyI∖JmPolyR∈V
115 funmpt ⊢Fun⁡k∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k
116 115 a1i ⊢φ∧g∈D→Fun⁡k∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k
117 88 feqmptd ⊢φ∧g∈D→g=k∈I⟼g⁡k
118 1 psrbagfsupp ⊢g∈D→finSupp0⁡g
119 118 adantl ⊢φ∧g∈D→finSupp0⁡g
120 117 119 eqbrtrrd ⊢φ∧g∈D→finSupp0⁡k∈I⟼g⁡k
121 ssidd ⊢φ∧g∈D→k∈I⟼g⁡ksupp0⊆k∈I⟼g⁡ksupp0
122 78 79 19 mulg0 ⊢t∈BaseJmPolyI∖JmPolyR→0⋅mulGrpJmPolyI∖JmPolyRt=0mulGrpJmPolyI∖JmPolyR
123 122 adantl ⊢φ∧g∈D∧t∈BaseJmPolyI∖JmPolyR→0⋅mulGrpJmPolyI∖JmPolyRt=0mulGrpJmPolyI∖JmPolyR
124 0zd ⊢φ∧g∈D→0∈ℤ
125 121 123 89 109 124 suppssov1 ⊢φ∧g∈D→k∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡ksupp0mulGrpJmPolyI∖JmPolyR⊆k∈I⟼g⁡ksupp0
126 113 114 116 120 125 fsuppsssuppgd ⊢φ∧g∈D→finSupp0mulGrpJmPolyI∖JmPolyR⁡k∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k
127 disjdifr ⊢I∖J∩J=∅
128 127 a1i ⊢φ∧g∈D→I∖J∩J=∅
129 undifr ⊢J⊆I↔I∖J∪J=I
130 6 129 sylib ⊢φ→I∖J∪J=I
131 130 eqcomd ⊢φ→I=I∖J∪J
132 131 adantr ⊢φ∧g∈D→I=I∖J∪J
133 78 79 80 83 84 111 126 128 132 gsumsplit ⊢φ∧g∈D→∑mulGrpJmPolyI∖JmPolyRk∈Ig⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=∑mulGrpJmPolyI∖JmPolyRk∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k↾I∖J⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k↾J
134 difssd ⊢φ∧g∈D→I∖J⊆I
135 134 resmptd ⊢φ∧g∈D→k∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k↾I∖J=k∈I∖J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k
136 eldifi ⊢k∈I∖J→k∈I
137 136 adantl ⊢φ∧g∈D∧k∈I∖J→k∈I
138 136 107 sylan2 ⊢φ∧g∈D∧k∈I∖J→ifk∈JJmVarI∖JmPolyR⁡kalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k∈BaseJmPolyI∖JmPolyR
139 90 95 137 138 fvmptd3 ⊢φ∧g∈D∧k∈I∖J→z∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=ifk∈JJmVarI∖JmPolyR⁡kalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
140 eldifn ⊢k∈I∖J→¬k∈J
141 140 adantl ⊢φ∧g∈D∧k∈I∖J→¬k∈J
142 141 iffalsed ⊢φ∧g∈D∧k∈I∖J→ifk∈JJmVarI∖JmPolyR⁡kalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k=algSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
143 139 142 eqtrd ⊢φ∧g∈D∧k∈I∖J→z∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=algSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
144 143 oveq2d ⊢φ∧g∈D∧k∈I∖J→g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=g⁡k⋅mulGrpJmPolyI∖JmPolyRalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
145 144 mpteq2dva ⊢φ∧g∈D→k∈I∖J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=k∈I∖J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
146 135 145 eqtrd ⊢φ∧g∈D→k∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k↾I∖J=k∈I∖J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
147 146 oveq2d ⊢φ∧g∈D→∑mulGrpJmPolyI∖JmPolyRk∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k↾I∖J=∑mulGrpJmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpJmPolyI∖JmPolyRalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
148 6 adantr ⊢φ∧g∈D→J⊆I
149 148 resmptd ⊢φ∧g∈D→k∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k↾J=k∈J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k
150 6 sselda ⊢φ∧k∈J→k∈I
151 150 adantlr ⊢φ∧g∈D∧k∈J→k∈I
152 151 107 syldan ⊢φ∧g∈D∧k∈J→ifk∈JJmVarI∖JmPolyR⁡kalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k∈BaseJmPolyI∖JmPolyR
153 90 95 151 152 fvmptd3 ⊢φ∧g∈D∧k∈J→z∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=ifk∈JJmVarI∖JmPolyR⁡kalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
154 iftrue ⊢k∈J→ifk∈JJmVarI∖JmPolyR⁡kalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k=JmVarI∖JmPolyR⁡k
155 154 adantl ⊢φ∧g∈D∧k∈J→ifk∈JJmVarI∖JmPolyR⁡kalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k=JmVarI∖JmPolyR⁡k
156 153 155 eqtrd ⊢φ∧g∈D∧k∈J→z∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=JmVarI∖JmPolyR⁡k
157 156 oveq2d ⊢φ∧g∈D∧k∈J→g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=g⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
158 157 mpteq2dva ⊢φ∧g∈D→k∈J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=k∈J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
159 149 158 eqtrd ⊢φ∧g∈D→k∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k↾J=k∈J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
160 159 oveq2d ⊢φ∧g∈D→∑mulGrpJmPolyI∖JmPolyRk∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k↾J=∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
161 147 160 oveq12d ⊢φ∧g∈D→∑mulGrpJmPolyI∖JmPolyRk∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k↾I∖J⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈I⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k↾J=∑mulGrpJmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpJmPolyI∖JmPolyRalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
162 55 adantr ⊢φ∧g∈D→algSc⁡JmPolyI∖JmPolyR:BaseI∖JmPolyR⟶BaseJmPolyI∖JmPolyR
163 10 21 31 mplsca ⊢φ→I∖JmPolyR=Scalar⁡JmPolyI∖JmPolyR
164 163 fveq2d ⊢φ→mulGrpI∖JmPolyR=mulGrpScalar⁡JmPolyI∖JmPolyR
165 164 fveq2d ⊢φ→⋅mulGrpI∖JmPolyR=⋅mulGrpScalar⁡JmPolyI∖JmPolyR
166 165 ad2antrr ⊢φ∧g∈D∧k∈I∖J→⋅mulGrpI∖JmPolyR=⋅mulGrpScalar⁡JmPolyI∖JmPolyR
167 166 oveqd ⊢φ∧g∈D∧k∈I∖J→g⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k=g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k
168 eqid ⊢mulGrpI∖JmPolyR=mulGrpI∖JmPolyR
169 168 54 mgpbas ⊢BaseI∖JmPolyR=BasemulGrpI∖JmPolyR
170 eqid ⊢⋅mulGrpI∖JmPolyR=⋅mulGrpI∖JmPolyR
171 168 crngmgp ⊢I∖JmPolyR∈CRing→mulGrpI∖JmPolyR∈CMnd
172 23 171 syl ⊢φ→mulGrpI∖JmPolyR∈CMnd
173 172 cmnmndd ⊢φ→mulGrpI∖JmPolyR∈Mnd
174 173 ad2antrr ⊢φ∧g∈D∧k∈I∖J→mulGrpI∖JmPolyR∈Mnd
175 136 89 sylan2 ⊢φ∧g∈D∧k∈I∖J→g⁡k∈ℕ0
176 22 ad2antrr ⊢φ∧g∈D∧k∈I∖J→I∖J∈V
177 58 ad2antrr ⊢φ∧g∈D∧k∈I∖J→R∈Ring
178 simpr ⊢φ∧g∈D∧k∈I∖J→k∈I∖J
179 9 57 54 176 177 178 mvrcl ⊢φ∧g∈D∧k∈I∖J→I∖JmVarR⁡k∈BaseI∖JmPolyR
180 169 170 174 175 179 mulgnn0cld ⊢φ∧g∈D∧k∈I∖J→g⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k∈BaseI∖JmPolyR
181 167 180 eqeltrrd ⊢φ∧g∈D∧k∈I∖J→g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k∈BaseI∖JmPolyR
182 162 181 cofmpt ⊢φ∧g∈D→algSc⁡JmPolyI∖JmPolyR∘k∈I∖J⟼g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k=k∈I∖J⟼algSc⁡JmPolyI∖JmPolyR⁡g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k
183 eqid ⊢mulGrpScalar⁡JmPolyI∖JmPolyR=mulGrpScalar⁡JmPolyI∖JmPolyR
184 183 18 rhmmhm ⊢algSc⁡JmPolyI∖JmPolyR∈Scalar⁡JmPolyI∖JmPolyRRingHomJmPolyI∖JmPolyR→algSc⁡JmPolyI∖JmPolyR∈mulGrpScalar⁡JmPolyI∖JmPolyRMndHommulGrpJmPolyI∖JmPolyR
185 29 184 syl ⊢φ→algSc⁡JmPolyI∖JmPolyR∈mulGrpScalar⁡JmPolyI∖JmPolyRMndHommulGrpJmPolyI∖JmPolyR
186 185 ad2antrr ⊢φ∧g∈D∧k∈I∖J→algSc⁡JmPolyI∖JmPolyR∈mulGrpScalar⁡JmPolyI∖JmPolyRMndHommulGrpJmPolyI∖JmPolyR
187 163 fveq2d ⊢φ→BaseI∖JmPolyR=BaseScalar⁡JmPolyI∖JmPolyR
188 187 ad2antrr ⊢φ∧g∈D∧k∈I∖J→BaseI∖JmPolyR=BaseScalar⁡JmPolyI∖JmPolyR
189 179 188 eleqtrd ⊢φ∧g∈D∧k∈I∖J→I∖JmVarR⁡k∈BaseScalar⁡JmPolyI∖JmPolyR
190 eqid ⊢BaseScalar⁡JmPolyI∖JmPolyR=BaseScalar⁡JmPolyI∖JmPolyR
191 183 190 mgpbas ⊢BaseScalar⁡JmPolyI∖JmPolyR=BasemulGrpScalar⁡JmPolyI∖JmPolyR
192 eqid ⊢⋅mulGrpScalar⁡JmPolyI∖JmPolyR=⋅mulGrpScalar⁡JmPolyI∖JmPolyR
193 191 192 19 mhmmulg ⊢algSc⁡JmPolyI∖JmPolyR∈mulGrpScalar⁡JmPolyI∖JmPolyRMndHommulGrpJmPolyI∖JmPolyR∧g⁡k∈ℕ0∧I∖JmVarR⁡k∈BaseScalar⁡JmPolyI∖JmPolyR→algSc⁡JmPolyI∖JmPolyR⁡g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k=g⁡k⋅mulGrpJmPolyI∖JmPolyRalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
194 186 175 189 193 syl3anc ⊢φ∧g∈D∧k∈I∖J→algSc⁡JmPolyI∖JmPolyR⁡g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k=g⁡k⋅mulGrpJmPolyI∖JmPolyRalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
195 194 mpteq2dva ⊢φ∧g∈D→k∈I∖J⟼algSc⁡JmPolyI∖JmPolyR⁡g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k=k∈I∖J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
196 182 195 eqtrd ⊢φ∧g∈D→algSc⁡JmPolyI∖JmPolyR∘k∈I∖J⟼g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k=k∈I∖J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
197 196 oveq2d ⊢φ∧g∈D→∑mulGrpJmPolyI∖JmPolyRalgSc⁡JmPolyI∖JmPolyR∘k∈I∖J⟼g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k=∑mulGrpJmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpJmPolyI∖JmPolyRalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k
198 eqid ⊢0mulGrpScalar⁡JmPolyI∖JmPolyR=0mulGrpScalar⁡JmPolyI∖JmPolyR
199 163 23 eqeltrrd ⊢φ→Scalar⁡JmPolyI∖JmPolyR∈CRing
200 183 crngmgp ⊢Scalar⁡JmPolyI∖JmPolyR∈CRing→mulGrpScalar⁡JmPolyI∖JmPolyR∈CMnd
201 199 200 syl ⊢φ→mulGrpScalar⁡JmPolyI∖JmPolyR∈CMnd
202 201 adantr ⊢φ∧g∈D→mulGrpScalar⁡JmPolyI∖JmPolyR∈CMnd
203 85 adantr ⊢φ∧g∈D→mulGrpJmPolyI∖JmPolyR∈Mnd
204 22 adantr ⊢φ∧g∈D→I∖J∈V
205 185 adantr ⊢φ∧g∈D→algSc⁡JmPolyI∖JmPolyR∈mulGrpScalar⁡JmPolyI∖JmPolyRMndHommulGrpJmPolyI∖JmPolyR
206 38 49 eqeltrrd ⊢φ→Scalar⁡JmPolyI∖JmPolyR∈Ring
207 183 ringmgp ⊢Scalar⁡JmPolyI∖JmPolyR∈Ring→mulGrpScalar⁡JmPolyI∖JmPolyR∈Mnd
208 206 207 syl ⊢φ→mulGrpScalar⁡JmPolyI∖JmPolyR∈Mnd
209 208 ad2antrr ⊢φ∧g∈D∧k∈I∖J→mulGrpScalar⁡JmPolyI∖JmPolyR∈Mnd
210 191 192 209 175 189 mulgnn0cld ⊢φ∧g∈D∧k∈I∖J→g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k∈BaseScalar⁡JmPolyI∖JmPolyR
211 210 fmpttd ⊢φ∧g∈D→k∈I∖J⟼g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k:I∖J⟶BaseScalar⁡JmPolyI∖JmPolyR
212 22 mptexd ⊢φ→k∈I∖J⟼g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k∈V
213 212 adantr ⊢φ∧g∈D→k∈I∖J⟼g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k∈V
214 fvexd ⊢φ∧g∈D→0mulGrpScalar⁡JmPolyI∖JmPolyR∈V
215 funmpt ⊢Fun⁡k∈I∖J⟼g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k
216 215 a1i ⊢φ∧g∈D→Fun⁡k∈I∖J⟼g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k
217 120 134 124 fmptssfisupp ⊢φ∧g∈D→finSupp0⁡k∈I∖J⟼g⁡k
218 ssidd ⊢φ∧g∈D→k∈I∖J⟼g⁡ksupp0⊆k∈I∖J⟼g⁡ksupp0
219 187 eqimssd ⊢φ→BaseI∖JmPolyR⊆BaseScalar⁡JmPolyI∖JmPolyR
220 219 sselda ⊢φ∧u∈BaseI∖JmPolyR→u∈BaseScalar⁡JmPolyI∖JmPolyR
221 220 adantlr ⊢φ∧g∈D∧u∈BaseI∖JmPolyR→u∈BaseScalar⁡JmPolyI∖JmPolyR
222 191 198 192 mulg0 ⊢u∈BaseScalar⁡JmPolyI∖JmPolyR→0⋅mulGrpScalar⁡JmPolyI∖JmPolyRu=0mulGrpScalar⁡JmPolyI∖JmPolyR
223 221 222 syl ⊢φ∧g∈D∧u∈BaseI∖JmPolyR→0⋅mulGrpScalar⁡JmPolyI∖JmPolyRu=0mulGrpScalar⁡JmPolyI∖JmPolyR
224 102 adantlr ⊢φ∧g∈D∧k∈I∖J→I∖JmVarR⁡k∈BaseI∖JmPolyR
225 218 223 175 224 124 suppssov1 ⊢φ∧g∈D→k∈I∖J⟼g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡ksupp0mulGrpScalar⁡JmPolyI∖JmPolyR⊆k∈I∖J⟼g⁡ksupp0
226 213 214 216 217 225 fsuppsssuppgd ⊢φ∧g∈D→finSupp0mulGrpScalar⁡JmPolyI∖JmPolyR⁡k∈I∖J⟼g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k
227 191 198 202 203 204 205 211 226 gsummhm ⊢φ∧g∈D→∑mulGrpJmPolyI∖JmPolyRalgSc⁡JmPolyI∖JmPolyR∘k∈I∖J⟼g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k=algSc⁡JmPolyI∖JmPolyR⁡∑mulGrpScalar⁡JmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k
228 197 227 eqtr3d ⊢φ∧g∈D→∑mulGrpJmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpJmPolyI∖JmPolyRalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k=algSc⁡JmPolyI∖JmPolyR⁡∑mulGrpScalar⁡JmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k
229 228 oveq1d ⊢φ∧g∈D→∑mulGrpJmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpJmPolyI∖JmPolyRalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=algSc⁡JmPolyI∖JmPolyR⁡∑mulGrpScalar⁡JmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
230 26 adantr ⊢φ∧g∈D→JmPolyI∖JmPolyR∈AssAlg
231 59 adantr ⊢φ∧g∈D→I∖JmVarR:I∖J⟶BaseI∖JmPolyR
232 231 ffvelcdmda ⊢φ∧g∈D∧k∈I∖J→I∖JmVarR⁡k∈BaseI∖JmPolyR
233 218 223 175 232 124 suppssov1 ⊢φ∧g∈D→k∈I∖J⟼g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡ksupp0mulGrpScalar⁡JmPolyI∖JmPolyR⊆k∈I∖J⟼g⁡ksupp0
234 213 214 216 217 233 fsuppsssuppgd ⊢φ∧g∈D→finSupp0mulGrpScalar⁡JmPolyI∖JmPolyR⁡k∈I∖J⟼g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k
235 191 198 202 204 211 234 gsumcl ⊢φ∧g∈D→∑mulGrpScalar⁡JmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k∈BaseScalar⁡JmPolyI∖JmPolyR
236 21 adantr ⊢φ∧g∈D→J∈V
237 85 ad2antrr ⊢φ∧g∈D∧k∈J→mulGrpJmPolyI∖JmPolyR∈Mnd
238 151 89 syldan ⊢φ∧g∈D∧k∈J→g⁡k∈ℕ0
239 78 19 237 238 98 mulgnn0cld ⊢φ∧g∈D∧k∈J→g⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k∈BaseJmPolyI∖JmPolyR
240 239 fmpttd ⊢φ∧g∈D→k∈J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k:J⟶BaseJmPolyI∖JmPolyR
241 21 mptexd ⊢φ→k∈J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k∈V
242 241 adantr ⊢φ∧g∈D→k∈J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k∈V
243 funmpt ⊢Fun⁡k∈J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
244 243 a1i ⊢φ∧g∈D→Fun⁡k∈J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
245 120 148 124 fmptssfisupp ⊢φ∧g∈D→finSupp0⁡k∈J⟼g⁡k
246 ssidd ⊢φ∧g∈D→k∈J⟼g⁡ksupp0⊆k∈J⟼g⁡ksupp0
247 246 123 238 98 124 suppssov1 ⊢φ∧g∈D→k∈J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡ksupp0mulGrpJmPolyI∖JmPolyR⊆k∈J⟼g⁡ksupp0
248 242 114 244 245 247 fsuppsssuppgd ⊢φ∧g∈D→finSupp0mulGrpJmPolyI∖JmPolyR⁡k∈J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
249 78 79 83 236 240 248 gsumcl ⊢φ∧g∈D→∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k∈BaseJmPolyI∖JmPolyR
250 eqid ⊢⋅JmPolyI∖JmPolyR=⋅JmPolyI∖JmPolyR
251 11 27 190 17 20 250 asclmul1 ⊢JmPolyI∖JmPolyR∈AssAlg∧∑mulGrpScalar⁡JmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k∈BaseScalar⁡JmPolyI∖JmPolyR∧∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k∈BaseJmPolyI∖JmPolyR→algSc⁡JmPolyI∖JmPolyR⁡∑mulGrpScalar⁡JmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=∑mulGrpScalar⁡JmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
252 230 235 249 251 syl3anc ⊢φ∧g∈D→algSc⁡JmPolyI∖JmPolyR⁡∑mulGrpScalar⁡JmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=∑mulGrpScalar⁡JmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
253 229 252 eqtrd ⊢φ∧g∈D→∑mulGrpJmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpJmPolyI∖JmPolyRalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=∑mulGrpScalar⁡JmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
254 133 161 253 3eqtrd ⊢φ∧g∈D→∑mulGrpJmPolyI∖JmPolyRk∈Ig⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=∑mulGrpScalar⁡JmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
255 165 oveqd ⊢φ→g⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k=g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k
256 255 mpteq2dv ⊢φ→k∈I∖J⟼g⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k=k∈I∖J⟼g⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k
257 164 256 oveq12d ⊢φ→∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k=∑mulGrpScalar⁡JmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k
258 257 eqcomd ⊢φ→∑mulGrpScalar⁡JmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k=∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k
259 258 adantr ⊢φ∧g∈D→∑mulGrpScalar⁡JmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k=∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k
260 259 oveq1d ⊢φ∧g∈D→∑mulGrpScalar⁡JmPolyI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpScalar⁡JmPolyI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
261 254 260 eqtrd ⊢φ∧g∈D→∑mulGrpJmPolyI∖JmPolyRk∈Ig⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
262 77 261 oveq12d ⊢φ∧g∈D→algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∘F⁡g⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Ig⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=algSc⁡JmPolyI∖JmPolyR⁡algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
263 74 75 ffvelcdmd ⊢φ∧g∈D→algSc⁡I∖JmPolyR⁡F⁡g∈BaseI∖JmPolyR
264 187 adantr ⊢φ∧g∈D→BaseI∖JmPolyR=BaseScalar⁡JmPolyI∖JmPolyR
265 263 264 eleqtrd ⊢φ∧g∈D→algSc⁡I∖JmPolyR⁡F⁡g∈BaseScalar⁡JmPolyI∖JmPolyR
266 10 21 49 mpllmodd ⊢φ→JmPolyI∖JmPolyR∈LMod
267 266 adantr ⊢φ∧g∈D→JmPolyI∖JmPolyR∈LMod
268 eqid ⊢0mulGrpI∖JmPolyR=0mulGrpI∖JmPolyR
269 172 adantr ⊢φ∧g∈D→mulGrpI∖JmPolyR∈CMnd
270 180 fmpttd ⊢φ∧g∈D→k∈I∖J⟼g⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k:I∖J⟶BaseI∖JmPolyR
271 22 mptexd ⊢φ→k∈I∖J⟼g⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k∈V
272 271 adantr ⊢φ∧g∈D→k∈I∖J⟼g⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k∈V
273 fvexd ⊢φ∧g∈D→0mulGrpI∖JmPolyR∈V
274 funmpt ⊢Fun⁡k∈I∖J⟼g⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k
275 274 a1i ⊢φ∧g∈D→Fun⁡k∈I∖J⟼g⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k
276 169 268 170 mulg0 ⊢e∈BaseI∖JmPolyR→0⋅mulGrpI∖JmPolyRe=0mulGrpI∖JmPolyR
277 276 adantl ⊢φ∧g∈D∧e∈BaseI∖JmPolyR→0⋅mulGrpI∖JmPolyRe=0mulGrpI∖JmPolyR
278 218 277 175 179 124 suppssov1 ⊢φ∧g∈D→k∈I∖J⟼g⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡ksupp0mulGrpI∖JmPolyR⊆k∈I∖J⟼g⁡ksupp0
279 272 273 275 217 278 fsuppsssuppgd ⊢φ∧g∈D→finSupp0mulGrpI∖JmPolyR⁡k∈I∖J⟼g⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k
280 169 268 269 204 270 279 gsumcl ⊢φ∧g∈D→∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k∈BaseI∖JmPolyR
281 280 264 eleqtrd ⊢φ∧g∈D→∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k∈BaseScalar⁡JmPolyI∖JmPolyR
282 17 27 250 190 267 281 249 lmodvscld ⊢φ∧g∈D→∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k∈BaseJmPolyI∖JmPolyR
283 11 27 190 17 20 250 asclmul1 ⊢JmPolyI∖JmPolyR∈AssAlg∧algSc⁡I∖JmPolyR⁡F⁡g∈BaseScalar⁡JmPolyI∖JmPolyR∧∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k∈BaseJmPolyI∖JmPolyR→algSc⁡JmPolyI∖JmPolyR⁡algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
284 230 265 282 283 syl3anc ⊢φ∧g∈D→algSc⁡JmPolyI∖JmPolyR⁡algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
285 262 284 eqtrd ⊢φ∧g∈D→algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∘F⁡g⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Ig⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
286 285 mpteq2dva ⊢φ→g∈D⟼algSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∘F⁡g⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Ig⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
287 286 oveq2d ⊢φ→∑JmPolyI∖JmPolyRg∈DalgSc⁡JmPolyI∖JmPolyR∘algSc⁡I∖JmPolyR∘F⁡g⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Ig⁡k⋅mulGrpJmPolyI∖JmPolyRz∈I⟼ifz∈JJmVarI∖JmPolyR⁡zalgSc⁡JmPolyI∖JmPolyR⁡I∖JmVarR⁡z⁡k=∑JmPolyI∖JmPolyRg∈DalgSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
288 13 67 287 3eqtrd ⊢φ→IselectVarsR⁡J⁡F=∑JmPolyI∖JmPolyRg∈DalgSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
289 288 fveq1d ⊢φ→IselectVarsR⁡J⁡F⁡Y↾J=∑JmPolyI∖JmPolyRg∈DalgSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J
290 289 fveq1d ⊢φ→IselectVarsR⁡J⁡F⁡Y↾J⁡Y↾I∖J=∑JmPolyI∖JmPolyRg∈DalgSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J⁡Y↾I∖J
291 eqid ⊢0I∖JmPolyR=0I∖JmPolyR
292 49 ringcmnd ⊢φ→I∖JmPolyR∈CMnd
293 5 crnggrpd ⊢φ→R∈Grp
294 293 grpmndd ⊢φ→R∈Mnd
295 ovex ⊢ℕ0I∈V
296 1 295 rabex2 ⊢D∈V
297 296 a1i ⊢φ→D∈V
298 eqid ⊢y∈ℕ0I∖J|y-1ℕ∈Fin=y∈ℕ0I∖J|y-1ℕ∈Fin
299 eqid ⊢v∈BaseI∖JmPolyR⟼v⁡Y↾I∖J=v∈BaseI∖JmPolyR⟼v⁡Y↾I∖J
300 difssd ⊢φ→I∖J⊆I
301 1 298 4 300 8 psrbagres ⊢φ→Y↾I∖J∈y∈ℕ0I∖J|y-1ℕ∈Fin
302 9 54 298 299 22 293 301 mplmapghm ⊢φ→v∈BaseI∖JmPolyR⟼v⁡Y↾I∖J∈I∖JmPolyRGrpHomR
303 ghmmhm ⊢v∈BaseI∖JmPolyR⟼v⁡Y↾I∖J∈I∖JmPolyRGrpHomR→v∈BaseI∖JmPolyR⟼v⁡Y↾I∖J∈I∖JmPolyRMndHomR
304 302 303 syl ⊢φ→v∈BaseI∖JmPolyR⟼v⁡Y↾I∖J∈I∖JmPolyRMndHomR
305 eqid ⊢x∈ℕ0J|x-1ℕ∈Fin=x∈ℕ0J|x-1ℕ∈Fin
306 simpr ⊢φ∧w∈BaseJmPolyI∖JmPolyR→w∈BaseJmPolyI∖JmPolyR
307 10 54 17 305 306 mplelf ⊢φ∧w∈BaseJmPolyI∖JmPolyR→w:x∈ℕ0J|x-1ℕ∈Fin⟶BaseI∖JmPolyR
308 1 305 4 6 8 psrbagres ⊢φ→Y↾J∈x∈ℕ0J|x-1ℕ∈Fin
309 308 adantr ⊢φ∧w∈BaseJmPolyI∖JmPolyR→Y↾J∈x∈ℕ0J|x-1ℕ∈Fin
310 307 309 ffvelcdmd ⊢φ∧w∈BaseJmPolyI∖JmPolyR→w⁡Y↾J∈BaseI∖JmPolyR
311 310 fmpttd ⊢φ→w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J:BaseJmPolyI∖JmPolyR⟶BaseI∖JmPolyR
312 17 27 250 190 267 265 282 lmodvscld ⊢φ∧g∈D→algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k∈BaseJmPolyI∖JmPolyR
313 312 fmpttd ⊢φ→g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k:D⟶BaseJmPolyI∖JmPolyR
314 311 313 fcod ⊢φ→w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k:D⟶BaseI∖JmPolyR
315 fvexd ⊢φ→0I∖JmPolyR∈V
316 24 crngringd ⊢φ→JmPolyI∖JmPolyR∈Ring
317 eqid ⊢0JmPolyI∖JmPolyR=0JmPolyI∖JmPolyR
318 17 317 ring0cl ⊢JmPolyI∖JmPolyR∈Ring→0JmPolyI∖JmPolyR∈BaseJmPolyI∖JmPolyR
319 316 318 syl ⊢φ→0JmPolyI∖JmPolyR∈BaseJmPolyI∖JmPolyR
320 ssidd ⊢φ→BaseJmPolyI∖JmPolyR⊆BaseJmPolyI∖JmPolyR
321 296 mptex ⊢g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k∈V
322 321 a1i ⊢φ→g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k∈V
323 fvexd ⊢φ→0JmPolyI∖JmPolyR∈V
324 funmpt ⊢Fun⁡g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
325 324 a1i ⊢φ→Fun⁡g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
326 296 mptex ⊢g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g∈V
327 326 a1i ⊢φ→g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g∈V
328 fvexd ⊢φ→0Scalar⁡JmPolyI∖JmPolyR∈V
329 funmpt ⊢Fun⁡g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g
330 329 a1i ⊢φ→Fun⁡g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g
331 eqid ⊢0R=0R
332 2 3 331 7 5 mplelsfi ⊢φ→finSupp0R⁡F
333 ssidd ⊢φ→Fsupp0R⊆Fsupp0R
334 fvexd ⊢φ→0R∈V
335 69 333 7 334 suppssrg ⊢φ∧g∈D∖supp0R⁡F→F⁡g=0R
336 335 fveq2d ⊢φ∧g∈D∖supp0R⁡F→algSc⁡I∖JmPolyR⁡F⁡g=algSc⁡I∖JmPolyR⁡0R
337 9 32 331 291 22 58 mplascl0 ⊢φ→algSc⁡I∖JmPolyR⁡0R=0I∖JmPolyR
338 163 fveq2d ⊢φ→0I∖JmPolyR=0Scalar⁡JmPolyI∖JmPolyR
339 337 338 eqtrd ⊢φ→algSc⁡I∖JmPolyR⁡0R=0Scalar⁡JmPolyI∖JmPolyR
340 339 adantr ⊢φ∧g∈D∖supp0R⁡F→algSc⁡I∖JmPolyR⁡0R=0Scalar⁡JmPolyI∖JmPolyR
341 336 340 eqtrd ⊢φ∧g∈D∖supp0R⁡F→algSc⁡I∖JmPolyR⁡F⁡g=0Scalar⁡JmPolyI∖JmPolyR
342 341 297 suppss2 ⊢φ→g∈D⟼algSc⁡I∖JmPolyR⁡F⁡gsupp0Scalar⁡JmPolyI∖JmPolyR⊆Fsupp0R
343 327 328 330 332 342 fsuppsssuppgd ⊢φ→finSupp0Scalar⁡JmPolyI∖JmPolyR⁡g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g
344 ssidd ⊢φ→g∈D⟼algSc⁡I∖JmPolyR⁡F⁡gsupp0Scalar⁡JmPolyI∖JmPolyR⊆g∈D⟼algSc⁡I∖JmPolyR⁡F⁡gsupp0Scalar⁡JmPolyI∖JmPolyR
345 eqid ⊢0Scalar⁡JmPolyI∖JmPolyR=0Scalar⁡JmPolyI∖JmPolyR
346 17 27 250 345 317 lmod0vs ⊢JmPolyI∖JmPolyR∈LMod∧f∈BaseJmPolyI∖JmPolyR→0Scalar⁡JmPolyI∖JmPolyR⋅JmPolyI∖JmPolyRf=0JmPolyI∖JmPolyR
347 266 346 sylan ⊢φ∧f∈BaseJmPolyI∖JmPolyR→0Scalar⁡JmPolyI∖JmPolyR⋅JmPolyI∖JmPolyRf=0JmPolyI∖JmPolyR
348 344 347 263 282 328 suppssov1 ⊢φ→g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡ksupp0JmPolyI∖JmPolyR⊆g∈D⟼algSc⁡I∖JmPolyR⁡F⁡gsupp0Scalar⁡JmPolyI∖JmPolyR
349 322 323 325 343 348 fsuppsssuppgd ⊢φ→finSupp0JmPolyI∖JmPolyR⁡g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
350 eqid ⊢w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J=w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J
351 23 crnggrpd ⊢φ→I∖JmPolyR∈Grp
352 10 17 305 350 21 351 308 mplmapghm ⊢φ→w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∈JmPolyI∖JmPolyRGrpHomI∖JmPolyR
353 ghmmhm ⊢w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∈JmPolyI∖JmPolyRGrpHomI∖JmPolyR→w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∈JmPolyI∖JmPolyRMndHomI∖JmPolyR
354 352 353 syl ⊢φ→w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∈JmPolyI∖JmPolyRMndHomI∖JmPolyR
355 317 291 mhm0 ⊢w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∈JmPolyI∖JmPolyRMndHomI∖JmPolyR→w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J⁡0JmPolyI∖JmPolyR=0I∖JmPolyR
356 354 355 syl ⊢φ→w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J⁡0JmPolyI∖JmPolyR=0I∖JmPolyR
357 315 319 313 311 320 297 47 349 356 fsuppcor ⊢φ→finSupp0I∖JmPolyR⁡w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
358 54 291 292 294 297 304 314 357 gsummhm ⊢φ→∑Rv∈BaseI∖JmPolyR⟼v⁡Y↾I∖J∘w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=v∈BaseI∖JmPolyR⟼v⁡Y↾I∖J⁡∑I∖JmPolyRw∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
359 fveq1 ⊢v=∑I∖JmPolyRw∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k→v⁡Y↾I∖J=∑I∖JmPolyRw∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾I∖J
360 54 291 292 297 314 357 gsumcl ⊢φ→∑I∖JmPolyRw∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k∈BaseI∖JmPolyR
361 fvexd ⊢φ→∑I∖JmPolyRw∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾I∖J∈V
362 299 359 360 361 fvmptd3 ⊢φ→v∈BaseI∖JmPolyR⟼v⁡Y↾I∖J⁡∑I∖JmPolyRw∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=∑I∖JmPolyRw∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾I∖J
363 316 ringcmnd ⊢φ→JmPolyI∖JmPolyR∈CMnd
364 351 grpmndd ⊢φ→I∖JmPolyR∈Mnd
365 17 317 363 364 297 354 313 349 gsummhm ⊢φ→∑I∖JmPolyRw∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J⁡∑JmPolyI∖JmPolyRg∈DalgSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
366 fveq1 ⊢w=∑JmPolyI∖JmPolyRg∈DalgSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k→w⁡Y↾J=∑JmPolyI∖JmPolyRg∈DalgSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J
367 17 317 363 297 313 349 gsumcl ⊢φ→∑JmPolyI∖JmPolyRg∈DalgSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k∈BaseJmPolyI∖JmPolyR
368 fvexd ⊢φ→∑JmPolyI∖JmPolyRg∈DalgSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J∈V
369 350 366 367 368 fvmptd3 ⊢φ→w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J⁡∑JmPolyI∖JmPolyRg∈DalgSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=∑JmPolyI∖JmPolyRg∈DalgSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J
370 365 369 eqtrd ⊢φ→∑I∖JmPolyRw∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=∑JmPolyI∖JmPolyRg∈DalgSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J
371 370 fveq1d ⊢φ→∑I∖JmPolyRw∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾I∖J=∑JmPolyI∖JmPolyRg∈DalgSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J⁡Y↾I∖J
372 358 362 371 3eqtrrd ⊢φ→∑JmPolyI∖JmPolyRg∈DalgSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J⁡Y↾I∖J=∑Rv∈BaseI∖JmPolyR⟼v⁡Y↾I∖J∘w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
373 10 54 17 305 312 mplelf ⊢φ∧g∈D→algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k:x∈ℕ0J|x-1ℕ∈Fin⟶BaseI∖JmPolyR
374 308 adantr ⊢φ∧g∈D→Y↾J∈x∈ℕ0J|x-1ℕ∈Fin
375 373 374 ffvelcdmd ⊢φ∧g∈D→algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J∈BaseI∖JmPolyR
376 eqidd ⊢φ→g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
377 eqidd ⊢φ→w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J=w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J
378 fveq1 ⊢w=algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k→w⁡Y↾J=algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J
379 312 376 377 378 fmptco ⊢φ→w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J
380 eqidd ⊢φ→v∈BaseI∖JmPolyR⟼v⁡Y↾I∖J=v∈BaseI∖JmPolyR⟼v⁡Y↾I∖J
381 fveq1 ⊢v=algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J→v⁡Y↾I∖J=algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J⁡Y↾I∖J
382 375 379 380 381 fmptco ⊢φ→v∈BaseI∖JmPolyR⟼v⁡Y↾I∖J∘w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J⁡Y↾I∖J
383 eqid ⊢⋅I∖JmPolyR=⋅I∖JmPolyR
384 10 250 54 17 383 305 263 282 374 mplvscaval ⊢φ∧g∈D→algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J=algSc⁡I∖JmPolyR⁡F⁡g⋅I∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J
385 10 250 54 17 383 305 280 249 374 mplvscaval ⊢φ∧g∈D→∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J=∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J
386 385 oveq2d ⊢φ∧g∈D→algSc⁡I∖JmPolyR⁡F⁡g⋅I∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J=algSc⁡I∖JmPolyR⁡F⁡g⋅I∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J
387 31 adantr ⊢φ∧g∈D→I∖JmPolyR∈AssAlg
388 36 fveq2d ⊢φ→BaseR=BaseScalar⁡I∖JmPolyR
389 388 adantr ⊢φ∧g∈D→BaseR=BaseScalar⁡I∖JmPolyR
390 75 389 eleqtrd ⊢φ∧g∈D→F⁡g∈BaseScalar⁡I∖JmPolyR
391 49 adantr ⊢φ∧g∈D→I∖JmPolyR∈Ring
392 10 54 17 305 249 mplelf ⊢φ∧g∈D→∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k:x∈ℕ0J|x-1ℕ∈Fin⟶BaseI∖JmPolyR
393 392 374 ffvelcdmd ⊢φ∧g∈D→∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J∈BaseI∖JmPolyR
394 54 383 391 280 393 ringcld ⊢φ∧g∈D→∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J∈BaseI∖JmPolyR
395 eqid ⊢BaseScalar⁡I∖JmPolyR=BaseScalar⁡I∖JmPolyR
396 eqid ⊢⋅I∖JmPolyR=⋅I∖JmPolyR
397 32 33 395 54 383 396 asclmul1 ⊢I∖JmPolyR∈AssAlg∧F⁡g∈BaseScalar⁡I∖JmPolyR∧∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J∈BaseI∖JmPolyR→algSc⁡I∖JmPolyR⁡F⁡g⋅I∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J=F⁡g⋅I∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J
398 387 390 394 397 syl3anc ⊢φ∧g∈D→algSc⁡I∖JmPolyR⁡F⁡g⋅I∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J=F⁡g⋅I∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J
399 384 386 398 3eqtrd ⊢φ∧g∈D→algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J=F⁡g⋅I∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J
400 399 fveq1d ⊢φ∧g∈D→algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J⁡Y↾I∖J=F⁡g⋅I∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J⁡Y↾I∖J
401 eqid ⊢⋅R=⋅R
402 301 adantr ⊢φ∧g∈D→Y↾I∖J∈y∈ℕ0I∖J|y-1ℕ∈Fin
403 9 396 68 54 401 298 75 394 402 mplvscaval ⊢φ∧g∈D→F⁡g⋅I∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J⁡Y↾I∖J=F⁡g⋅R∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J⁡Y↾I∖J
404 eqid ⊢1R=1R
405 5 adantr ⊢φ∧g∈D→R∈CRing
406 1 298 84 134 71 psrbagres ⊢φ∧g∈D→g↾I∖J∈y∈ℕ0I∖J|y-1ℕ∈Fin
407 9 298 331 404 204 168 170 57 405 406 mplcoe2 ⊢φ∧g∈D→i∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R=∑mulGrpI∖JmPolyRk∈I∖Jg↾I∖J⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k
408 178 fvresd ⊢φ∧g∈D∧k∈I∖J→g↾I∖J⁡k=g⁡k
409 408 oveq1d ⊢φ∧g∈D∧k∈I∖J→g↾I∖J⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k=g⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k
410 409 mpteq2dva ⊢φ∧g∈D→k∈I∖J⟼g↾I∖J⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k=k∈I∖J⟼g⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k
411 410 oveq2d ⊢φ∧g∈D→∑mulGrpI∖JmPolyRk∈I∖Jg↾I∖J⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k=∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k
412 407 411 eqtrd ⊢φ∧g∈D→i∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R=∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k
413 eqid ⊢j∈x∈ℕ0J|x-1ℕ∈Fin⟼ifj=g↾J1I∖JmPolyR0I∖JmPolyR=j∈x∈ℕ0J|x-1ℕ∈Fin⟼ifj=g↾J1I∖JmPolyR0I∖JmPolyR
414 eqeq1 ⊢j=Y↾J→j=g↾J↔Y↾J=g↾J
415 414 ifbid ⊢j=Y↾J→ifj=g↾J1I∖JmPolyR0I∖JmPolyR=ifY↾J=g↾J1I∖JmPolyR0I∖JmPolyR
416 fvexd ⊢φ∧g∈D→1I∖JmPolyR∈V
417 fvexd ⊢φ∧g∈D→0I∖JmPolyR∈V
418 416 417 ifcld ⊢φ∧g∈D→ifY↾J=g↾J1I∖JmPolyR0I∖JmPolyR∈V
419 413 415 374 418 fvmptd3 ⊢φ∧g∈D→j∈x∈ℕ0J|x-1ℕ∈Fin⟼ifj=g↾J1I∖JmPolyR0I∖JmPolyR⁡Y↾J=ifY↾J=g↾J1I∖JmPolyR0I∖JmPolyR
420 eqid ⊢1I∖JmPolyR=1I∖JmPolyR
421 23 adantr ⊢φ∧g∈D→I∖JmPolyR∈CRing
422 1 305 84 148 71 psrbagres ⊢φ∧g∈D→g↾J∈x∈ℕ0J|x-1ℕ∈Fin
423 10 305 291 420 236 18 19 48 421 422 mplcoe2 ⊢φ∧g∈D→j∈x∈ℕ0J|x-1ℕ∈Fin⟼ifj=g↾J1I∖JmPolyR0I∖JmPolyR=∑mulGrpJmPolyI∖JmPolyRk∈Jg↾J⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
424 simpr ⊢φ∧g∈D∧k∈J→k∈J
425 424 fvresd ⊢φ∧g∈D∧k∈J→g↾J⁡k=g⁡k
426 425 oveq1d ⊢φ∧g∈D∧k∈J→g↾J⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=g⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
427 426 mpteq2dva ⊢φ∧g∈D→k∈J⟼g↾J⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=k∈J⟼g⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
428 427 oveq2d ⊢φ∧g∈D→∑mulGrpJmPolyI∖JmPolyRk∈Jg↾J⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
429 423 428 eqtrd ⊢φ∧g∈D→j∈x∈ℕ0J|x-1ℕ∈Fin⟼ifj=g↾J1I∖JmPolyR0I∖JmPolyR=∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k
430 429 fveq1d ⊢φ∧g∈D→j∈x∈ℕ0J|x-1ℕ∈Fin⟼ifj=g↾J1I∖JmPolyR0I∖JmPolyR⁡Y↾J=∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J
431 419 430 eqtr3d ⊢φ∧g∈D→ifY↾J=g↾J1I∖JmPolyR0I∖JmPolyR=∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J
432 412 431 oveq12d ⊢φ∧g∈D→i∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyRifY↾J=g↾J1I∖JmPolyR0I∖JmPolyR=∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J
433 432 eqcomd ⊢φ∧g∈D→∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J=i∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyRifY↾J=g↾J1I∖JmPolyR0I∖JmPolyR
434 433 fveq1d ⊢φ∧g∈D→∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J⁡Y↾I∖J=i∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyRifY↾J=g↾J1I∖JmPolyR0I∖JmPolyR⁡Y↾I∖J
435 434 oveq2d ⊢φ∧g∈D→F⁡g⋅R∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J⁡Y↾I∖J=F⁡g⋅Ri∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyRifY↾J=g↾J1I∖JmPolyR0I∖JmPolyR⁡Y↾I∖J
436 ovif2 ⊢i∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyRifY↾J=g↾J1I∖JmPolyR0I∖JmPolyR=ifY↾J=g↾Ji∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR1I∖JmPolyRi∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR0I∖JmPolyR
437 436 fveq1i ⊢i∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyRifY↾J=g↾J1I∖JmPolyR0I∖JmPolyR⁡Y↾I∖J=ifY↾J=g↾Ji∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR1I∖JmPolyRi∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR0I∖JmPolyR⁡Y↾I∖J
438 iffv ⊢ifY↾J=g↾Ji∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR1I∖JmPolyRi∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR0I∖JmPolyR⁡Y↾I∖J=ifY↾J=g↾Ji∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR1I∖JmPolyR⁡Y↾I∖Ji∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR0I∖JmPolyR⁡Y↾I∖J
439 eqeq1 ⊢i=Y↾I∖J→i=g↾I∖J↔Y↾I∖J=g↾I∖J
440 439 ifbid ⊢i=Y↾I∖J→ifi=g↾I∖J1R0R=ifY↾I∖J=g↾I∖J1R0R
441 58 adantr ⊢φ∧g∈D→R∈Ring
442 9 54 331 404 298 204 441 406 mplmon ⊢φ∧g∈D→i∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R∈BaseI∖JmPolyR
443 54 383 420 391 442 ringridmd ⊢φ∧g∈D→i∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR1I∖JmPolyR=i∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R
444 fvexd ⊢φ∧g∈D→1R∈V
445 fvexd ⊢φ∧g∈D→0R∈V
446 444 445 ifcld ⊢φ∧g∈D→ifY↾I∖J=g↾I∖J1R0R∈V
447 440 443 402 446 fvmptd4 ⊢φ∧g∈D→i∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR1I∖JmPolyR⁡Y↾I∖J=ifY↾I∖J=g↾I∖J1R0R
448 54 383 291 391 442 ringrzd ⊢φ∧g∈D→i∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR0I∖JmPolyR=0I∖JmPolyR
449 448 fveq1d ⊢φ∧g∈D→i∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR0I∖JmPolyR⁡Y↾I∖J=0I∖JmPolyR⁡Y↾I∖J
450 9 298 331 291 22 293 mpl0 ⊢φ→0I∖JmPolyR=y∈ℕ0I∖J|y-1ℕ∈Fin×0R
451 450 adantr ⊢φ∧g∈D→0I∖JmPolyR=y∈ℕ0I∖J|y-1ℕ∈Fin×0R
452 451 fveq1d ⊢φ∧g∈D→0I∖JmPolyR⁡Y↾I∖J=y∈ℕ0I∖J|y-1ℕ∈Fin×0R⁡Y↾I∖J
453 fvex ⊢0R∈V
454 453 fvconst2 ⊢Y↾I∖J∈y∈ℕ0I∖J|y-1ℕ∈Fin→y∈ℕ0I∖J|y-1ℕ∈Fin×0R⁡Y↾I∖J=0R
455 402 454 syl ⊢φ∧g∈D→y∈ℕ0I∖J|y-1ℕ∈Fin×0R⁡Y↾I∖J=0R
456 449 452 455 3eqtrd ⊢φ∧g∈D→i∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR0I∖JmPolyR⁡Y↾I∖J=0R
457 447 456 ifeq12d ⊢φ∧g∈D→ifY↾J=g↾Ji∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR1I∖JmPolyR⁡Y↾I∖Ji∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR0I∖JmPolyR⁡Y↾I∖J=ifY↾J=g↾JifY↾I∖J=g↾I∖J1R0R0R
458 438 457 eqtrid ⊢φ∧g∈D→ifY↾J=g↾Ji∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR1I∖JmPolyRi∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyR0I∖JmPolyR⁡Y↾I∖J=ifY↾J=g↾JifY↾I∖J=g↾I∖J1R0R0R
459 437 458 eqtrid ⊢φ∧g∈D→i∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyRifY↾J=g↾J1I∖JmPolyR0I∖JmPolyR⁡Y↾I∖J=ifY↾J=g↾JifY↾I∖J=g↾I∖J1R0R0R
460 459 oveq2d ⊢φ∧g∈D→F⁡g⋅Ri∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyRifY↾J=g↾J1I∖JmPolyR0I∖JmPolyR⁡Y↾I∖J=F⁡g⋅RifY↾J=g↾JifY↾I∖J=g↾I∖J1R0R0R
461 ifan ⊢ifY↾J=g↾J∧Y↾I∖J=g↾I∖J1R0R=ifY↾J=g↾JifY↾I∖J=g↾I∖J1R0R0R
462 461 oveq2i ⊢F⁡g⋅RifY↾J=g↾J∧Y↾I∖J=g↾I∖J1R0R=F⁡g⋅RifY↾J=g↾JifY↾I∖J=g↾I∖J1R0R0R
463 1 psrbagf ⊢Y∈D→Y:I⟶ℕ0
464 8 463 syl ⊢φ→Y:I⟶ℕ0
465 464 ffnd ⊢φ→YFnI
466 465 adantr ⊢φ∧g∈D→YFnI
467 undif ⊢J⊆I↔J∪I∖J=I
468 6 467 sylib ⊢φ→J∪I∖J=I
469 468 adantr ⊢φ∧g∈D→J∪I∖J=I
470 469 fneq2d ⊢φ∧g∈D→YFnJ∪I∖J↔YFnI
471 466 470 mpbird ⊢φ∧g∈D→YFnJ∪I∖J
472 88 ffnd ⊢φ∧g∈D→gFnI
473 469 fneq2d ⊢φ∧g∈D→gFnJ∪I∖J↔gFnI
474 472 473 mpbird ⊢φ∧g∈D→gFnJ∪I∖J
475 eqfnun ⊢YFnJ∪I∖J∧gFnJ∪I∖J→Y=g↔Y↾J=g↾J∧Y↾I∖J=g↾I∖J
476 471 474 475 syl2anc ⊢φ∧g∈D→Y=g↔Y↾J=g↾J∧Y↾I∖J=g↾I∖J
477 476 ifbid ⊢φ∧g∈D→ifY=g1R0R=ifY↾J=g↾J∧Y↾I∖J=g↾I∖J1R0R
478 477 oveq2d ⊢φ∧g∈D→F⁡g⋅RifY=g1R0R=F⁡g⋅RifY↾J=g↾J∧Y↾I∖J=g↾I∖J1R0R
479 ovif2 ⊢F⁡g⋅RifY=g1R0R=ifY=gF⁡g⋅R1RF⁡g⋅R0R
480 478 479 eqtr3di ⊢φ∧g∈D→F⁡g⋅RifY↾J=g↾J∧Y↾I∖J=g↾I∖J1R0R=ifY=gF⁡g⋅R1RF⁡g⋅R0R
481 462 480 eqtr3id ⊢φ∧g∈D→F⁡g⋅RifY↾J=g↾JifY↾I∖J=g↾I∖J1R0R0R=ifY=gF⁡g⋅R1RF⁡g⋅R0R
482 460 481 eqtrd ⊢φ∧g∈D→F⁡g⋅Ri∈y∈ℕ0I∖J|y-1ℕ∈Fin⟼ifi=g↾I∖J1R0R⋅I∖JmPolyRifY↾J=g↾J1I∖JmPolyR0I∖JmPolyR⁡Y↾I∖J=ifY=gF⁡g⋅R1RF⁡g⋅R0R
483 68 401 404 441 75 ringridmd ⊢φ∧g∈D→F⁡g⋅R1R=F⁡g
484 68 401 331 441 75 ringrzd ⊢φ∧g∈D→F⁡g⋅R0R=0R
485 483 484 ifeq12d ⊢φ∧g∈D→ifY=gF⁡g⋅R1RF⁡g⋅R0R=ifY=gF⁡g0R
486 435 482 485 3eqtrd ⊢φ∧g∈D→F⁡g⋅R∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅I∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J⁡Y↾I∖J=ifY=gF⁡g0R
487 400 403 486 3eqtrd ⊢φ∧g∈D→algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J⁡Y↾I∖J=ifY=gF⁡g0R
488 487 mpteq2dva ⊢φ→g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k⁡Y↾J⁡Y↾I∖J=g∈D⟼ifY=gF⁡g0R
489 382 488 eqtrd ⊢φ→v∈BaseI∖JmPolyR⟼v⁡Y↾I∖J∘w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=g∈D⟼ifY=gF⁡g0R
490 489 oveq2d ⊢φ→∑Rv∈BaseI∖JmPolyR⟼v⁡Y↾I∖J∘w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=∑Rg∈DifY=gF⁡g0R
491 58 ringcmnd ⊢φ→R∈CMnd
492 68 331 ring0cl ⊢R∈Ring→0R∈BaseR
493 58 492 syl ⊢φ→0R∈BaseR
494 493 adantr ⊢φ∧g∈D→0R∈BaseR
495 75 494 ifcld ⊢φ∧g∈D→ifY=gF⁡g0R∈BaseR
496 495 fmpttd ⊢φ→g∈D⟼ifY=gF⁡g0R:D⟶BaseR
497 eldifsnneq ⊢g∈D∖Y→¬g=Y
498 497 neqcomd ⊢g∈D∖Y→¬Y=g
499 498 iffalsed ⊢g∈D∖Y→ifY=gF⁡g0R=0R
500 499 adantl ⊢φ∧g∈D∖Y→ifY=gF⁡g0R=0R
501 500 297 suppss2 ⊢φ→g∈D⟼ifY=gF⁡g0Rsupp0R⊆Y
502 297 mptexd ⊢φ→g∈D⟼ifY=gF⁡g0R∈V
503 funmpt ⊢Fun⁡g∈D⟼ifY=gF⁡g0R
504 503 a1i ⊢φ→Fun⁡g∈D⟼ifY=gF⁡g0R
505 snfi ⊢Y∈Fin
506 505 a1i ⊢φ→Y∈Fin
507 506 501 ssfid ⊢φ→g∈D⟼ifY=gF⁡g0Rsupp0R∈Fin
508 502 493 504 507 isfsuppd ⊢φ→finSupp0R⁡g∈D⟼ifY=gF⁡g0R
509 68 331 491 297 496 501 508 gsumres ⊢φ→∑Rg∈D⟼ifY=gF⁡g0R↾Y=∑Rg∈DifY=gF⁡g0R
510 8 snssd ⊢φ→Y⊆D
511 510 resmptd ⊢φ→g∈D⟼ifY=gF⁡g0R↾Y=g∈Y⟼ifY=gF⁡g0R
512 511 oveq2d ⊢φ→∑Rg∈D⟼ifY=gF⁡g0R↾Y=∑Rg∈YifY=gF⁡g0R
513 69 8 ffvelcdmd ⊢φ→F⁡Y∈BaseR
514 iftrue ⊢Y=g→ifY=gF⁡g0R=F⁡g
515 fveq2 ⊢g=Y→F⁡g=F⁡Y
516 515 eqcoms ⊢Y=g→F⁡g=F⁡Y
517 514 516 eqtrd ⊢Y=g→ifY=gF⁡g0R=F⁡Y
518 517 eqcoms ⊢g=Y→ifY=gF⁡g0R=F⁡Y
519 68 518 gsumsn ⊢R∈Mnd∧Y∈D∧F⁡Y∈BaseR→∑Rg∈YifY=gF⁡g0R=F⁡Y
520 294 8 513 519 syl3anc ⊢φ→∑Rg∈YifY=gF⁡g0R=F⁡Y
521 512 520 eqtrd ⊢φ→∑Rg∈D⟼ifY=gF⁡g0R↾Y=F⁡Y
522 490 509 521 3eqtr2d ⊢φ→∑Rv∈BaseI∖JmPolyR⟼v⁡Y↾I∖J∘w∈BaseJmPolyI∖JmPolyR⟼w⁡Y↾J∘g∈D⟼algSc⁡I∖JmPolyR⁡F⁡g⋅JmPolyI∖JmPolyR∑mulGrpI∖JmPolyRk∈I∖Jg⁡k⋅mulGrpI∖JmPolyRI∖JmVarR⁡k⋅JmPolyI∖JmPolyR∑mulGrpJmPolyI∖JmPolyRk∈Jg⁡k⋅mulGrpJmPolyI∖JmPolyRJmVarI∖JmPolyR⁡k=F⁡Y
523 290 372 522 3eqtrd ⊢φ→IselectVarsR⁡J⁡F⁡Y↾J⁡Y↾I∖J=F⁡Y