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 ∈ ℕ 0 I | h -1 ℕ ∈ Fin
selvvvval.p ⊢ P = I mPoly R
selvvvval.b ⊢ B = Base P
selvvvval.r ⊢ φ → R ∈ CRing
selvvvval.j ⊢ φ → J ⊆ I
selvvvval.f ⊢ φ → F ∈ B
selvvvval.y ⊢ φ → Y ∈ D
Assertion selvvvval ⊢ φ → I selectVars R ⁡ J ⁡ F ⁡ Y ↾ J ⁡ Y ↾ I ∖ J = F ⁡ Y

Proof

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