Metamath Proof Explorer

Theorem extdgfialglem2

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

Ref Expression
Hypotheses extdgfialg.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
extdgfialg.d ⊢ 𝐷 = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) )
extdgfialg.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
extdgfialg.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
extdgfialg.1 ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
extdgfialglem1.2 ⊢ 𝑍 = ( 0g ‘ 𝐸 )
extdgfialglem1.3 ⊢ · = ( .r ‘ 𝐸 )
extdgfialglem1.r ⊢ 𝐺 = ( 𝑛 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑋 ) )
extdgfialglem1.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
extdgfialglem2.1 ⊢ ( 𝜑 → 𝐴 : ( 0 ... 𝐷 ) ⟶ 𝐹 )
extdgfialglem2.2 ⊢ ( 𝜑 → 𝐴 finSupp 𝑍 )
extdgfialglem2.3 ⊢ ( 𝜑 → ( 𝐸 Σg ( 𝐴 ∘f · 𝐺 ) ) = 𝑍 )
extdgfialglem2.4 ⊢ ( 𝜑 → 𝐴 ≠ ( ( 0 ... 𝐷 ) × { 𝑍 } ) )
Assertion extdgfialglem2 ( 𝜑 → 𝑋 ∈ ( 𝐸 IntgRing 𝐹 ) )

Proof

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