Metamath Proof Explorer

Theorem extdgfialglem2

Description: Lemma for extdgfialg . (Contributed by Thierry Arnoux, 10-Jan-2026)

Ref Expression
Hypotheses extdgfialg.b ⊢ B = Base E
extdgfialg.d ⊢ D = dim ⁡ subringAlg ⁡ E ⁡ F
extdgfialg.e ⊢ φ → E ∈ Field
extdgfialg.f ⊢ φ → F ∈ SubDRing ⁡ E
extdgfialg.1 ⊢ φ → D ∈ ℕ 0
extdgfialglem1.2 ⊢ Z = 0 E
extdgfialglem1.3 ⊢ · ˙ = ⋅ E
extdgfialglem1.r ⊢ G = n ∈ 0 … D ⟼ n ⋅ mulGrp subringAlg ⁡ E ⁡ F X
extdgfialglem1.4 ⊢ φ → X ∈ B
extdgfialglem2.1 ⊢ φ → A : 0 … D ⟶ F
extdgfialglem2.2 ⊢ φ → finSupp Z⁡ A
extdgfialglem2.3 ⊢ φ → ∑ E A · ˙ f G = Z
extdgfialglem2.4 ⊢ φ → A ≠ 0 … D × Z
Assertion extdgfialglem2 ⊢ φ → X ∈ E IntgRing F

Proof

Step Hyp Ref Expression
1 extdgfialg.b ⊢ B = Base E
2 extdgfialg.d ⊢ D = dim ⁡ subringAlg ⁡ E ⁡ F
3 extdgfialg.e ⊢ φ → E ∈ Field
4 extdgfialg.f ⊢ φ → F ∈ SubDRing ⁡ E
5 extdgfialg.1 ⊢ φ → D ∈ ℕ 0
6 extdgfialglem1.2 ⊢ Z = 0 E
7 extdgfialglem1.3 ⊢ · ˙ = ⋅ E
8 extdgfialglem1.r ⊢ G = n ∈ 0 … D ⟼ n ⋅ mulGrp subringAlg ⁡ E ⁡ F X
9 extdgfialglem1.4 ⊢ φ → X ∈ B
10 extdgfialglem2.1 ⊢ φ → A : 0 … D ⟶ F
11 extdgfialglem2.2 ⊢ φ → finSupp Z⁡ A
12 extdgfialglem2.3 ⊢ φ → ∑ E A · ˙ f G = Z
13 extdgfialglem2.4 ⊢ φ → A ≠ 0 … D × Z
14 eqid ⊢ E evalSub 1 F = E evalSub 1 F
15 eqid ⊢ 0 Poly 1 ⁡ E = 0 Poly 1 ⁡ E
16 eqid ⊢ Base Poly 1 ⁡ E ↾ 𝑠 F = Base Poly 1 ⁡ E ↾ 𝑠 F
17 eqid ⊢ 0 Poly 1 ⁡ E ↾ 𝑠 F = 0 Poly 1 ⁡ E ↾ 𝑠 F
18 sdrgsubrg ⊢ F ∈ SubDRing ⁡ E → F ∈ SubRing ⁡ E
19 4 18 syl ⊢ φ → F ∈ SubRing ⁡ E
20 eqid ⊢ E ↾ 𝑠 F = E ↾ 𝑠 F
21 20 subrgring ⊢ F ∈ SubRing ⁡ E → E ↾ 𝑠 F ∈ Ring
22 19 21 syl ⊢ φ → E ↾ 𝑠 F ∈ Ring
23 eqid ⊢ Poly 1 ⁡ E ↾ 𝑠 F = Poly 1 ⁡ E ↾ 𝑠 F
24 23 ply1ring ⊢ E ↾ 𝑠 F ∈ Ring → Poly 1 ⁡ E ↾ 𝑠 F ∈ Ring
25 22 24 syl ⊢ φ → Poly 1 ⁡ E ↾ 𝑠 F ∈ Ring
26 25 ringcmnd ⊢ φ → Poly 1 ⁡ E ↾ 𝑠 F ∈ CMnd
27 fzfid ⊢ φ → 0 … D ∈ Fin
28 eqid ⊢ Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F = Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F
29 eqid ⊢ ⋅ Poly 1 ⁡ E ↾ 𝑠 F = ⋅ Poly 1 ⁡ E ↾ 𝑠 F
30 eqid ⊢ Base Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F = Base Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F
31 23 ply1lmod ⊢ E ↾ 𝑠 F ∈ Ring → Poly 1 ⁡ E ↾ 𝑠 F ∈ LMod
32 22 31 syl ⊢ φ → Poly 1 ⁡ E ↾ 𝑠 F ∈ LMod
33 32 adantr ⊢ φ ∧ n ∈ 0 … D → Poly 1 ⁡ E ↾ 𝑠 F ∈ LMod
34 10 ffvelcdmda ⊢ φ ∧ n ∈ 0 … D → A ⁡ n ∈ F
35 1 sdrgss ⊢ F ∈ SubDRing ⁡ E → F ⊆ B
36 4 35 syl ⊢ φ → F ⊆ B
37 20 1 ressbas2 ⊢ F ⊆ B → F = Base E ↾ 𝑠 F
38 36 37 syl ⊢ φ → F = Base E ↾ 𝑠 F
39 ovex ⊢ E ↾ 𝑠 F ∈ V
40 23 ply1sca ⊢ E ↾ 𝑠 F ∈ V → E ↾ 𝑠 F = Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F
41 39 40 ax-mp ⊢ E ↾ 𝑠 F = Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F
42 41 fveq2i ⊢ Base E ↾ 𝑠 F = Base Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F
43 38 42 eqtr2di ⊢ φ → Base Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F = F
44 43 adantr ⊢ φ ∧ n ∈ 0 … D → Base Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F = F
45 34 44 eleqtrrd ⊢ φ ∧ n ∈ 0 … D → A ⁡ n ∈ Base Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F
46 eqid ⊢ mulGrp Poly 1 ⁡ E ↾ 𝑠 F = mulGrp Poly 1 ⁡ E ↾ 𝑠 F
47 46 16 mgpbas ⊢ Base Poly 1 ⁡ E ↾ 𝑠 F = Base mulGrp Poly 1 ⁡ E ↾ 𝑠 F
48 eqid ⊢ ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F = ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F
49 46 ringmgp ⊢ Poly 1 ⁡ E ↾ 𝑠 F ∈ Ring → mulGrp Poly 1 ⁡ E ↾ 𝑠 F ∈ Mnd
50 25 49 syl ⊢ φ → mulGrp Poly 1 ⁡ E ↾ 𝑠 F ∈ Mnd
51 50 adantr ⊢ φ ∧ n ∈ 0 … D → mulGrp Poly 1 ⁡ E ↾ 𝑠 F ∈ Mnd
52 fz0ssnn0 ⊢ 0 … D ⊆ ℕ 0
53 52 a1i ⊢ φ → 0 … D ⊆ ℕ 0
54 53 sselda ⊢ φ ∧ n ∈ 0 … D → n ∈ ℕ 0
55 eqid ⊢ var 1 ⁡ E ↾ 𝑠 F = var 1 ⁡ E ↾ 𝑠 F
56 55 23 16 vr1cl ⊢ E ↾ 𝑠 F ∈ Ring → var 1 ⁡ E ↾ 𝑠 F ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
57 22 56 syl ⊢ φ → var 1 ⁡ E ↾ 𝑠 F ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
58 57 adantr ⊢ φ ∧ n ∈ 0 … D → var 1 ⁡ E ↾ 𝑠 F ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
59 47 48 51 54 58 mulgnn0cld ⊢ φ ∧ n ∈ 0 … D → n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
60 16 28 29 30 33 45 59 lmodvscld ⊢ φ ∧ n ∈ 0 … D → A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
61 60 fmpttd ⊢ φ → n ∈ 0 … D ⟼ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F : 0 … D ⟶ Base Poly 1 ⁡ E ↾ 𝑠 F
62 eqid ⊢ n ∈ 0 … D ⟼ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = n ∈ 0 … D ⟼ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F
63 fvexd ⊢ φ → 0 Poly 1 ⁡ E ↾ 𝑠 F ∈ V
64 62 27 60 63 fsuppmptdm ⊢ φ → finSupp 0 Poly 1 ⁡ E ↾ 𝑠 F ⁡ n ∈ 0 … D ⟼ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F
65 16 17 26 27 61 64 gsumcl ⊢ φ → ∑ Poly 1 ⁡ E ↾ 𝑠 F n = 0 D A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
66 3 fldcrngd ⊢ φ → E ∈ CRing
67 14 23 16 66 19 evls1dm ⊢ φ → dom ⁡ E evalSub 1 F = Base Poly 1 ⁡ E ↾ 𝑠 F
68 65 67 eleqtrrd ⊢ φ → ∑ Poly 1 ⁡ E ↾ 𝑠 F n = 0 D A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ∈ dom ⁡ E evalSub 1 F
69 eqid ⊢ Base E ↾ 𝑠 F = Base E ↾ 𝑠 F
70 eqid ⊢ 0 E ↾ 𝑠 F = 0 E ↾ 𝑠 F
71 10 ffvelcdmda ⊢ φ ∧ m ∈ 0 … D → A ⁡ m ∈ F
72 71 adantlr ⊢ φ ∧ m ∈ ℕ 0 ∧ m ∈ 0 … D → A ⁡ m ∈ F
73 38 ad2antrr ⊢ φ ∧ m ∈ ℕ 0 ∧ m ∈ 0 … D → F = Base E ↾ 𝑠 F
74 72 73 eleqtrd ⊢ φ ∧ m ∈ ℕ 0 ∧ m ∈ 0 … D → A ⁡ m ∈ Base E ↾ 𝑠 F
75 subrgsubg ⊢ F ∈ SubRing ⁡ E → F ∈ SubGrp ⁡ E
76 19 75 syl ⊢ φ → F ∈ SubGrp ⁡ E
77 6 subg0cl ⊢ F ∈ SubGrp ⁡ E → Z ∈ F
78 76 77 syl ⊢ φ → Z ∈ F
79 78 38 eleqtrd ⊢ φ → Z ∈ Base E ↾ 𝑠 F
80 79 ad2antrr ⊢ φ ∧ m ∈ ℕ 0 ∧ ¬ m ∈ 0 … D → Z ∈ Base E ↾ 𝑠 F
81 74 80 ifclda ⊢ φ ∧ m ∈ ℕ 0 → if m ∈ 0 … D A ⁡ m Z ∈ Base E ↾ 𝑠 F
82 81 ralrimiva ⊢ φ → ∀ m ∈ ℕ 0 if m ∈ 0 … D A ⁡ m Z ∈ Base E ↾ 𝑠 F
83 eqid ⊢ m ∈ ℕ 0 ⟼ if m ∈ 0 … D A ⁡ m Z = m ∈ ℕ 0 ⟼ if m ∈ 0 … D A ⁡ m Z
84 nn0ex ⊢ ℕ 0 ∈ V
85 84 a1i ⊢ φ → ℕ 0 ∈ V
86 83 85 27 71 78 mptiffisupp ⊢ φ → finSupp Z⁡ m ∈ ℕ 0 ⟼ if m ∈ 0 … D A ⁡ m Z
87 66 crngringd ⊢ φ → E ∈ Ring
88 87 ringcmnd ⊢ φ → E ∈ CMnd
89 88 cmnmndd ⊢ φ → E ∈ Mnd
90 20 1 6 ress0g ⊢ E ∈ Mnd ∧ Z ∈ F ∧ F ⊆ B → Z = 0 E ↾ 𝑠 F
91 89 78 36 90 syl3anc ⊢ φ → Z = 0 E ↾ 𝑠 F
92 86 91 breqtrd ⊢ φ → finSupp 0 E ↾ 𝑠 F⁡ m ∈ ℕ 0 ⟼ if m ∈ 0 … D A ⁡ m Z
93 79 ralrimivw ⊢ φ → ∀ m ∈ ℕ 0 Z ∈ Base E ↾ 𝑠 F
94 fconstmpt ⊢ ℕ 0 × Z = m ∈ ℕ 0 ⟼ Z
95 85 78 fczfsuppd ⊢ φ → finSupp Z⁡ ℕ 0 × Z
96 94 95 eqbrtrrid ⊢ φ → finSupp Z⁡ m ∈ ℕ 0 ⟼ Z
97 96 91 breqtrd ⊢ φ → finSupp 0 E ↾ 𝑠 F⁡ m ∈ ℕ 0 ⟼ Z
98 simpr ⊢ φ ∧ m ∈ ℕ 0 ∖ 0 … D → m ∈ ℕ 0 ∖ 0 … D
99 98 eldifbd ⊢ φ ∧ m ∈ ℕ 0 ∖ 0 … D → ¬ m ∈ 0 … D
100 99 iffalsed ⊢ φ ∧ m ∈ ℕ 0 ∖ 0 … D → if m ∈ 0 … D A ⁡ m Z = Z
101 91 adantr ⊢ φ ∧ m ∈ ℕ 0 ∖ 0 … D → Z = 0 E ↾ 𝑠 F
102 100 101 eqtrd ⊢ φ ∧ m ∈ ℕ 0 ∖ 0 … D → if m ∈ 0 … D A ⁡ m Z = 0 E ↾ 𝑠 F
103 102 oveq1d ⊢ φ ∧ m ∈ ℕ 0 ∖ 0 … D → if m ∈ 0 … D A ⁡ m Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = 0 E ↾ 𝑠 F ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F
104 32 adantr ⊢ φ ∧ m ∈ ℕ 0 ∖ 0 … D → Poly 1 ⁡ E ↾ 𝑠 F ∈ LMod
105 50 adantr ⊢ φ ∧ m ∈ ℕ 0 ∖ 0 … D → mulGrp Poly 1 ⁡ E ↾ 𝑠 F ∈ Mnd
106 98 eldifad ⊢ φ ∧ m ∈ ℕ 0 ∖ 0 … D → m ∈ ℕ 0
107 57 adantr ⊢ φ ∧ m ∈ ℕ 0 ∖ 0 … D → var 1 ⁡ E ↾ 𝑠 F ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
108 47 48 105 106 107 mulgnn0cld ⊢ φ ∧ m ∈ ℕ 0 ∖ 0 … D → m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
109 16 41 29 70 17 lmod0vs ⊢ Poly 1 ⁡ E ↾ 𝑠 F ∈ LMod ∧ m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ∈ Base Poly 1 ⁡ E ↾ 𝑠 F → 0 E ↾ 𝑠 F ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = 0 Poly 1 ⁡ E ↾ 𝑠 F
110 104 108 109 syl2anc ⊢ φ ∧ m ∈ ℕ 0 ∖ 0 … D → 0 E ↾ 𝑠 F ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = 0 Poly 1 ⁡ E ↾ 𝑠 F
111 103 110 eqtrd ⊢ φ ∧ m ∈ ℕ 0 ∖ 0 … D → if m ∈ 0 … D A ⁡ m Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = 0 Poly 1 ⁡ E ↾ 𝑠 F
112 32 adantr ⊢ φ ∧ m ∈ ℕ 0 → Poly 1 ⁡ E ↾ 𝑠 F ∈ LMod
113 50 adantr ⊢ φ ∧ m ∈ ℕ 0 → mulGrp Poly 1 ⁡ E ↾ 𝑠 F ∈ Mnd
114 simpr ⊢ φ ∧ m ∈ ℕ 0 → m ∈ ℕ 0
115 57 adantr ⊢ φ ∧ m ∈ ℕ 0 → var 1 ⁡ E ↾ 𝑠 F ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
116 47 48 113 114 115 mulgnn0cld ⊢ φ ∧ m ∈ ℕ 0 → m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
117 16 41 29 69 112 81 116 lmodvscld ⊢ φ ∧ m ∈ ℕ 0 → if m ∈ 0 … D A ⁡ m Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
118 16 17 26 85 111 27 117 53 gsummptres2 ⊢ φ → ∑ Poly 1 ⁡ E ↾ 𝑠 F m ∈ ℕ 0 if m ∈ 0 … D A ⁡ m Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = ∑ Poly 1 ⁡ E ↾ 𝑠 F m = 0 D if m ∈ 0 … D A ⁡ m Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F
119 eleq1w ⊢ m = n → m ∈ 0 … D ↔ n ∈ 0 … D
120 fveq2 ⊢ m = n → A ⁡ m = A ⁡ n
121 119 120 ifbieq1d ⊢ m = n → if m ∈ 0 … D A ⁡ m Z = if n ∈ 0 … D A ⁡ n Z
122 oveq1 ⊢ m = n → m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F
123 121 122 oveq12d ⊢ m = n → if m ∈ 0 … D A ⁡ m Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = if n ∈ 0 … D A ⁡ n Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F
124 123 cbvmptv ⊢ m ∈ 0 … D ⟼ if m ∈ 0 … D A ⁡ m Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = n ∈ 0 … D ⟼ if n ∈ 0 … D A ⁡ n Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F
125 simpr ⊢ φ ∧ n ∈ 0 … D → n ∈ 0 … D
126 125 iftrued ⊢ φ ∧ n ∈ 0 … D → if n ∈ 0 … D A ⁡ n Z = A ⁡ n
127 126 oveq1d ⊢ φ ∧ n ∈ 0 … D → if n ∈ 0 … D A ⁡ n Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F
128 127 mpteq2dva ⊢ φ → n ∈ 0 … D ⟼ if n ∈ 0 … D A ⁡ n Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = n ∈ 0 … D ⟼ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F
129 124 128 eqtrid ⊢ φ → m ∈ 0 … D ⟼ if m ∈ 0 … D A ⁡ m Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = n ∈ 0 … D ⟼ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F
130 129 oveq2d ⊢ φ → ∑ Poly 1 ⁡ E ↾ 𝑠 F m = 0 D if m ∈ 0 … D A ⁡ m Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = ∑ Poly 1 ⁡ E ↾ 𝑠 F n = 0 D A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F
131 118 130 eqtr2d ⊢ φ → ∑ Poly 1 ⁡ E ↾ 𝑠 F n = 0 D A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = ∑ Poly 1 ⁡ E ↾ 𝑠 F m ∈ ℕ 0 if m ∈ 0 … D A ⁡ m Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F
132 26 cmnmndd ⊢ φ → Poly 1 ⁡ E ↾ 𝑠 F ∈ Mnd
133 17 gsumz ⊢ Poly 1 ⁡ E ↾ 𝑠 F ∈ Mnd ∧ ℕ 0 ∈ V → ∑ Poly 1 ⁡ E ↾ 𝑠 F m ∈ ℕ 0 0 Poly 1 ⁡ E ↾ 𝑠 F = 0 Poly 1 ⁡ E ↾ 𝑠 F
134 132 85 133 syl2anc ⊢ φ → ∑ Poly 1 ⁡ E ↾ 𝑠 F m ∈ ℕ 0 0 Poly 1 ⁡ E ↾ 𝑠 F = 0 Poly 1 ⁡ E ↾ 𝑠 F
135 91 adantr ⊢ φ ∧ m ∈ ℕ 0 → Z = 0 E ↾ 𝑠 F
136 135 oveq1d ⊢ φ ∧ m ∈ ℕ 0 → Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = 0 E ↾ 𝑠 F ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F
137 112 116 109 syl2anc ⊢ φ ∧ m ∈ ℕ 0 → 0 E ↾ 𝑠 F ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = 0 Poly 1 ⁡ E ↾ 𝑠 F
138 136 137 eqtrd ⊢ φ ∧ m ∈ ℕ 0 → Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = 0 Poly 1 ⁡ E ↾ 𝑠 F
139 138 mpteq2dva ⊢ φ → m ∈ ℕ 0 ⟼ Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = m ∈ ℕ 0 ⟼ 0 Poly 1 ⁡ E ↾ 𝑠 F
140 139 oveq2d ⊢ φ → ∑ Poly 1 ⁡ E ↾ 𝑠 F m ∈ ℕ 0 Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = ∑ Poly 1 ⁡ E ↾ 𝑠 F m ∈ ℕ 0 0 Poly 1 ⁡ E ↾ 𝑠 F
141 eqid ⊢ Poly 1 ⁡ E = Poly 1 ⁡ E
142 141 20 23 16 19 15 ressply10g ⊢ φ → 0 Poly 1 ⁡ E = 0 Poly 1 ⁡ E ↾ 𝑠 F
143 134 140 142 3eqtr4rd ⊢ φ → 0 Poly 1 ⁡ E = ∑ Poly 1 ⁡ E ↾ 𝑠 F m ∈ ℕ 0 Z ⋅ Poly 1 ⁡ E ↾ 𝑠 F m ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F
144 23 55 48 22 69 29 70 82 92 93 97 131 143 gsumply1eq ⊢ φ → ∑ Poly 1 ⁡ E ↾ 𝑠 F n = 0 D A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = 0 Poly 1 ⁡ E ↔ ∀ m ∈ ℕ 0 if m ∈ 0 … D A ⁡ m Z = Z
145 10 ffnd ⊢ φ → A Fn 0 … D
146 145 adantr ⊢ φ ∧ ∀ m ∈ ℕ 0 if m ∈ 0 … D A ⁡ m Z = Z → A Fn 0 … D
147 126 adantlr ⊢ φ ∧ ∀ m ∈ ℕ 0 if m ∈ 0 … D A ⁡ m Z = Z ∧ n ∈ 0 … D → if n ∈ 0 … D A ⁡ n Z = A ⁡ n
148 121 eqeq1d ⊢ m = n → if m ∈ 0 … D A ⁡ m Z = Z ↔ if n ∈ 0 … D A ⁡ n Z = Z
149 simplr ⊢ φ ∧ ∀ m ∈ ℕ 0 if m ∈ 0 … D A ⁡ m Z = Z ∧ n ∈ 0 … D → ∀ m ∈ ℕ 0 if m ∈ 0 … D A ⁡ m Z = Z
150 52 a1i ⊢ φ ∧ ∀ m ∈ ℕ 0 if m ∈ 0 … D A ⁡ m Z = Z → 0 … D ⊆ ℕ 0
151 150 sselda ⊢ φ ∧ ∀ m ∈ ℕ 0 if m ∈ 0 … D A ⁡ m Z = Z ∧ n ∈ 0 … D → n ∈ ℕ 0
152 148 149 151 rspcdva ⊢ φ ∧ ∀ m ∈ ℕ 0 if m ∈ 0 … D A ⁡ m Z = Z ∧ n ∈ 0 … D → if n ∈ 0 … D A ⁡ n Z = Z
153 147 152 eqtr3d ⊢ φ ∧ ∀ m ∈ ℕ 0 if m ∈ 0 … D A ⁡ m Z = Z ∧ n ∈ 0 … D → A ⁡ n = Z
154 146 153 fconst7v ⊢ φ ∧ ∀ m ∈ ℕ 0 if m ∈ 0 … D A ⁡ m Z = Z → A = 0 … D × Z
155 154 ex ⊢ φ → ∀ m ∈ ℕ 0 if m ∈ 0 … D A ⁡ m Z = Z → A = 0 … D × Z
156 144 155 sylbid ⊢ φ → ∑ Poly 1 ⁡ E ↾ 𝑠 F n = 0 D A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = 0 Poly 1 ⁡ E → A = 0 … D × Z
157 156 necon3d ⊢ φ → A ≠ 0 … D × Z → ∑ Poly 1 ⁡ E ↾ 𝑠 F n = 0 D A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ≠ 0 Poly 1 ⁡ E
158 13 157 mpd ⊢ φ → ∑ Poly 1 ⁡ E ↾ 𝑠 F n = 0 D A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ≠ 0 Poly 1 ⁡ E
159 eqid ⊢ E ↑ 𝑠 B = E ↑ 𝑠 B
160 14 1 23 17 20 159 16 66 19 60 53 64 evls1gsumadd ⊢ φ → E evalSub 1 F ⁡ ∑ Poly 1 ⁡ E ↾ 𝑠 F n = 0 D A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = ∑ E ↑ 𝑠 B n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F
161 160 fveq1d ⊢ φ → E evalSub 1 F ⁡ ∑ Poly 1 ⁡ E ↾ 𝑠 F n = 0 D A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ X = ∑ E ↑ 𝑠 B n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ X
162 66 adantr ⊢ φ ∧ n ∈ 0 … D → E ∈ CRing
163 19 adantr ⊢ φ ∧ n ∈ 0 … D → F ∈ SubRing ⁡ E
164 14 23 16 162 163 1 60 evls1fvf ⊢ φ ∧ n ∈ 0 … D → E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F : B ⟶ B
165 164 feqmptd ⊢ φ ∧ n ∈ 0 … D → E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = x ∈ B ⟼ E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x
166 165 mpteq2dva ⊢ φ → n ∈ 0 … D ⟼ E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = n ∈ 0 … D ⟼ x ∈ B ⟼ E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x
167 166 oveq2d ⊢ φ → ∑ E ↑ 𝑠 B n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F = ∑ E ↑ 𝑠 B n = 0 D x ∈ B ⟼ E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x
168 167 fveq1d ⊢ φ → ∑ E ↑ 𝑠 B n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ X = ∑ E ↑ 𝑠 B n = 0 D x ∈ B ⟼ E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x ⁡ X
169 eqid ⊢ 0 E ↑ 𝑠 B = 0 E ↑ 𝑠 B
170 1 fvexi ⊢ B ∈ V
171 170 a1i ⊢ φ → B ∈ V
172 162 adantr ⊢ φ ∧ n ∈ 0 … D ∧ x ∈ B → E ∈ CRing
173 163 adantr ⊢ φ ∧ n ∈ 0 … D ∧ x ∈ B → F ∈ SubRing ⁡ E
174 simpr ⊢ φ ∧ n ∈ 0 … D ∧ x ∈ B → x ∈ B
175 60 adantr ⊢ φ ∧ n ∈ 0 … D ∧ x ∈ B → A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
176 14 23 1 16 172 173 174 175 evls1fvcl ⊢ φ ∧ n ∈ 0 … D ∧ x ∈ B → E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x ∈ B
177 176 an32s ⊢ φ ∧ x ∈ B ∧ n ∈ 0 … D → E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x ∈ B
178 177 anasss ⊢ φ ∧ x ∈ B ∧ n ∈ 0 … D → E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x ∈ B
179 eqid ⊢ n ∈ 0 … D ⟼ x ∈ B ⟼ E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x = n ∈ 0 … D ⟼ x ∈ B ⟼ E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x
180 170 a1i ⊢ φ ∧ n ∈ 0 … D → B ∈ V
181 180 mptexd ⊢ φ ∧ n ∈ 0 … D → x ∈ B ⟼ E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x ∈ V
182 fvexd ⊢ φ → 0 E ↑ 𝑠 B ∈ V
183 179 27 181 182 fsuppmptdm ⊢ φ → finSupp 0 E ↑ 𝑠 B⁡ n ∈ 0 … D ⟼ x ∈ B ⟼ E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x
184 159 1 169 171 27 88 178 183 pwsgsum ⊢ φ → ∑ E ↑ 𝑠 B n = 0 D x ∈ B ⟼ E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x = x ∈ B ⟼ ∑ E n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x
185 184 fveq1d ⊢ φ → ∑ E ↑ 𝑠 B n = 0 D x ∈ B ⟼ E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x ⁡ X = x ∈ B ⟼ ∑ E n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x ⁡ X
186 168 185 eqtrd ⊢ φ → ∑ E ↑ 𝑠 B n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ X = x ∈ B ⟼ ∑ E n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x ⁡ X
187 fveq2 ⊢ x = X → E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x = E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ X
188 187 mpteq2dv ⊢ x = X → n ∈ 0 … D ⟼ E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x = n ∈ 0 … D ⟼ E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ X
189 188 oveq2d ⊢ x = X → ∑ E n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x = ∑ E n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ X
190 eqidd ⊢ φ → x ∈ B ⟼ ∑ E n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x = x ∈ B ⟼ ∑ E n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x
191 ovexd ⊢ φ → ∑ E n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ X ∈ V
192 189 190 9 191 fvmptd4 ⊢ φ → x ∈ B ⟼ ∑ E n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ x ⁡ X = ∑ E n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ X
193 eqid ⊢ ⋅ mulGrp E = ⋅ mulGrp E
194 9 adantr ⊢ φ ∧ n ∈ 0 … D → X ∈ B
195 14 1 23 20 55 48 193 29 7 162 163 34 54 194 evls1monply1 ⊢ φ ∧ n ∈ 0 … D → E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ X = A ⁡ n · ˙ n ⋅ mulGrp E X
196 195 mpteq2dva ⊢ φ → n ∈ 0 … D ⟼ E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ X = n ∈ 0 … D ⟼ A ⁡ n · ˙ n ⋅ mulGrp E X
197 nfv ⊢ Ⅎ n φ
198 ovexd ⊢ φ ∧ n ∈ 0 … D → n ⋅ mulGrp subringAlg ⁡ E ⁡ F X ∈ V
199 197 198 8 fnmptd ⊢ φ → G Fn 0 … D
200 inidm ⊢ 0 … D ∩ 0 … D = 0 … D
201 eqidd ⊢ φ ∧ n ∈ 0 … D → A ⁡ n = A ⁡ n
202 8 fvmpt2 ⊢ n ∈ 0 … D ∧ n ⋅ mulGrp subringAlg ⁡ E ⁡ F X ∈ V → G ⁡ n = n ⋅ mulGrp subringAlg ⁡ E ⁡ F X
203 125 198 202 syl2anc ⊢ φ ∧ n ∈ 0 … D → G ⁡ n = n ⋅ mulGrp subringAlg ⁡ E ⁡ F X
204 eqid ⊢ subringAlg ⁡ E ⁡ F = subringAlg ⁡ E ⁡ F
205 36 1 sseqtrdi ⊢ φ → F ⊆ Base E
206 204 87 205 srapwov ⊢ φ → ⋅ mulGrp E = ⋅ mulGrp subringAlg ⁡ E ⁡ F
207 206 oveqd ⊢ φ → n ⋅ mulGrp E X = n ⋅ mulGrp subringAlg ⁡ E ⁡ F X
208 207 adantr ⊢ φ ∧ n ∈ 0 … D → n ⋅ mulGrp E X = n ⋅ mulGrp subringAlg ⁡ E ⁡ F X
209 203 208 eqtr4d ⊢ φ ∧ n ∈ 0 … D → G ⁡ n = n ⋅ mulGrp E X
210 145 199 27 27 200 201 209 offval ⊢ φ → A · ˙ f G = n ∈ 0 … D ⟼ A ⁡ n · ˙ n ⋅ mulGrp E X
211 196 210 eqtr4d ⊢ φ → n ∈ 0 … D ⟼ E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ X = A · ˙ f G
212 211 oveq2d ⊢ φ → ∑ E n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ X = ∑ E A · ˙ f G
213 186 192 212 3eqtrd ⊢ φ → ∑ E ↑ 𝑠 B n = 0 D E evalSub 1 F ⁡ A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ X = ∑ E A · ˙ f G
214 161 213 12 3eqtrd ⊢ φ → E evalSub 1 F ⁡ ∑ Poly 1 ⁡ E ↾ 𝑠 F n = 0 D A ⁡ n ⋅ Poly 1 ⁡ E ↾ 𝑠 F n ⋅ mulGrp Poly 1 ⁡ E ↾ 𝑠 F var 1 ⁡ E ↾ 𝑠 F ⁡ X = Z
215 14 15 6 3 4 1 68 158 214 9 irngnzply1lem ⊢ φ → X ∈ E IntgRing F