Metamath Proof Explorer

Theorem plypf1

Description: Write the set of complex polynomials in a subring in terms of the abstract polynomial construction. (Contributed by Mario Carneiro, 3-Jul-2015) (Proof shortened by AV, 29-Sep-2019)

Ref Expression
Hypotheses plypf1.r ⊢ 𝑅 = ( ℂfld ↾s 𝑆 )
plypf1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
plypf1.a ⊢ 𝐴 = ( Base ‘ 𝑃 )
plypf1.e ⊢ 𝐸 = ( eval1 ‘ ℂfld )
Assertion plypf1 ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( Poly ‘ 𝑆 ) = ( 𝐸 “ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 plypf1.r ⊢ 𝑅 = ( ℂfld ↾s 𝑆 )
2 plypf1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 plypf1.a ⊢ 𝐴 = ( Base ‘ 𝑃 )
4 plypf1.e ⊢ 𝐸 = ( eval1 ‘ ℂfld )
5 elply ⊢ ( 𝑓 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
6 5 simprbi ⊢ ( 𝑓 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
7 eqid ⊢ ( ℂfld ↑s ℂ ) = ( ℂfld ↑s ℂ )
8 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
9 eqid ⊢ ( 0g ‘ ( ℂfld ↑s ℂ ) ) = ( 0g ‘ ( ℂfld ↑s ℂ ) )
10 cnex ⊢ ℂ ∈ V
11 10 a1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ℂ ∈ V )
12 fzfid ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( 0 ... 𝑛 ) ∈ Fin )
13 cnring ⊢ ℂfld ∈ Ring
14 ringcmn ⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
15 13 14 mp1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ℂfld ∈ CMnd )
16 8 subrgss ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 𝑆 ⊆ ℂ )
17 16 ad2antrr ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝑆 ⊆ ℂ )
18 elmapi ⊢ ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) → 𝑎 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
19 18 ad2antll ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → 𝑎 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
20 subrgsubg ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 𝑆 ∈ ( SubGrp ‘ ℂfld ) )
21 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
22 21 subg0cl ⊢ ( 𝑆 ∈ ( SubGrp ‘ ℂfld ) → 0 ∈ 𝑆 )
23 20 22 syl ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 0 ∈ 𝑆 )
24 23 adantr ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → 0 ∈ 𝑆 )
25 24 snssd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → { 0 } ⊆ 𝑆 )
26 ssequn2 ⊢ ( { 0 } ⊆ 𝑆 ↔ ( 𝑆 ∪ { 0 } ) = 𝑆 )
27 25 26 sylib ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( 𝑆 ∪ { 0 } ) = 𝑆 )
28 27 feq3d ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( 𝑎 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ↔ 𝑎 : ℕ0 ⟶ 𝑆 ) )
29 19 28 mpbid ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → 𝑎 : ℕ0 ⟶ 𝑆 )
30 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → 𝑘 ∈ ℕ0 )
31 ffvelrn ⊢ ( ( 𝑎 : ℕ0 ⟶ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑎 ‘ 𝑘 ) ∈ 𝑆 )
32 29 30 31 syl2an ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑎 ‘ 𝑘 ) ∈ 𝑆 )
33 17 32 sseldd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑎 ‘ 𝑘 ) ∈ ℂ )
34 33 adantrl ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ) → ( 𝑎 ‘ 𝑘 ) ∈ ℂ )
35 simprl ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ) → 𝑧 ∈ ℂ )
36 30 ad2antll ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ) → 𝑘 ∈ ℕ0 )
37 expcl ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
38 35 36 37 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
39 34 38 mulcld ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ) → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
40 eqid ⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( 𝑧 ∈ ℂ ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( 𝑧 ∈ ℂ ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
41 10 mptex ⊢ ( 𝑧 ∈ ℂ ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ V
42 41 a1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑧 ∈ ℂ ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ V )
43 fvex ⊢ ( 0g ‘ ( ℂfld ↑s ℂ ) ) ∈ V
44 43 a1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( 0g ‘ ( ℂfld ↑s ℂ ) ) ∈ V )
45 40 12 42 44 fsuppmptdm ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( 𝑧 ∈ ℂ ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) finSupp ( 0g ‘ ( ℂfld ↑s ℂ ) ) )
46 7 8 9 11 12 15 39 45 pwsgsum ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( ( ℂfld ↑s ℂ ) Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( 𝑧 ∈ ℂ ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) = ( 𝑧 ∈ ℂ ↦ ( ℂfld Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
47 fzfid ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) → ( 0 ... 𝑛 ) ∈ Fin )
48 39 anassrs ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
49 47 48 gsumfsum ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) → ( ℂfld Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
50 49 mpteq2dva ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( 𝑧 ∈ ℂ ↦ ( ℂfld Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
51 46 50 eqtrd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( ( ℂfld ↑s ℂ ) Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( 𝑧 ∈ ℂ ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
52 7 pwsring ⊢ ( ( ℂfld ∈ Ring ∧ ℂ ∈ V ) → ( ℂfld ↑s ℂ ) ∈ Ring )
53 13 10 52 mp2an ⊢ ( ℂfld ↑s ℂ ) ∈ Ring
54 ringcmn ⊢ ( ( ℂfld ↑s ℂ ) ∈ Ring → ( ℂfld ↑s ℂ ) ∈ CMnd )
55 53 54 mp1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( ℂfld ↑s ℂ ) ∈ CMnd )
56 cncrng ⊢ ℂfld ∈ CRing
57 eqid ⊢ ( Poly1 ‘ ℂfld ) = ( Poly1 ‘ ℂfld )
58 4 57 7 8 evl1rhm ⊢ ( ℂfld ∈ CRing → 𝐸 ∈ ( ( Poly1 ‘ ℂfld ) RingHom ( ℂfld ↑s ℂ ) ) )
59 56 58 ax-mp ⊢ 𝐸 ∈ ( ( Poly1 ‘ ℂfld ) RingHom ( ℂfld ↑s ℂ ) )
60 57 1 2 3 subrgply1 ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 𝐴 ∈ ( SubRing ‘ ( Poly1 ‘ ℂfld ) ) )
61 60 adantr ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → 𝐴 ∈ ( SubRing ‘ ( Poly1 ‘ ℂfld ) ) )
62 rhmima ⊢ ( ( 𝐸 ∈ ( ( Poly1 ‘ ℂfld ) RingHom ( ℂfld ↑s ℂ ) ) ∧ 𝐴 ∈ ( SubRing ‘ ( Poly1 ‘ ℂfld ) ) ) → ( 𝐸 “ 𝐴 ) ∈ ( SubRing ‘ ( ℂfld ↑s ℂ ) ) )
63 59 61 62 sylancr ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( 𝐸 “ 𝐴 ) ∈ ( SubRing ‘ ( ℂfld ↑s ℂ ) ) )
64 subrgsubg ⊢ ( ( 𝐸 “ 𝐴 ) ∈ ( SubRing ‘ ( ℂfld ↑s ℂ ) ) → ( 𝐸 “ 𝐴 ) ∈ ( SubGrp ‘ ( ℂfld ↑s ℂ ) ) )
65 subgsubm ⊢ ( ( 𝐸 “ 𝐴 ) ∈ ( SubGrp ‘ ( ℂfld ↑s ℂ ) ) → ( 𝐸 “ 𝐴 ) ∈ ( SubMnd ‘ ( ℂfld ↑s ℂ ) ) )
66 63 64 65 3syl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( 𝐸 “ 𝐴 ) ∈ ( SubMnd ‘ ( ℂfld ↑s ℂ ) ) )
67 eqid ⊢ ( Base ‘ ( ℂfld ↑s ℂ ) ) = ( Base ‘ ( ℂfld ↑s ℂ ) )
68 13 a1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ℂfld ∈ Ring )
69 10 a1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ℂ ∈ V )
70 fconst6g ⊢ ( ( 𝑎 ‘ 𝑘 ) ∈ ℂ → ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) : ℂ ⟶ ℂ )
71 33 70 syl ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) : ℂ ⟶ ℂ )
72 7 8 67 pwselbasb ⊢ ( ( ℂfld ∈ Ring ∧ ℂ ∈ V ) → ( ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) ∈ ( Base ‘ ( ℂfld ↑s ℂ ) ) ↔ ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) : ℂ ⟶ ℂ ) )
73 13 10 72 mp2an ⊢ ( ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) ∈ ( Base ‘ ( ℂfld ↑s ℂ ) ) ↔ ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) : ℂ ⟶ ℂ )
74 71 73 sylibr ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) ∈ ( Base ‘ ( ℂfld ↑s ℂ ) ) )
75 38 anass1rs ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑧 ∈ ℂ ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
76 75 fmpttd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) : ℂ ⟶ ℂ )
77 7 8 67 pwselbasb ⊢ ( ( ℂfld ∈ Ring ∧ ℂ ∈ V ) → ( ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) ∈ ( Base ‘ ( ℂfld ↑s ℂ ) ) ↔ ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) : ℂ ⟶ ℂ ) )
78 13 10 77 mp2an ⊢ ( ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) ∈ ( Base ‘ ( ℂfld ↑s ℂ ) ) ↔ ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) : ℂ ⟶ ℂ )
79 76 78 sylibr ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) ∈ ( Base ‘ ( ℂfld ↑s ℂ ) ) )
80 cnfldmul ⊢ · = ( .r ‘ ℂfld )
81 eqid ⊢ ( .r ‘ ( ℂfld ↑s ℂ ) ) = ( .r ‘ ( ℂfld ↑s ℂ ) )
82 7 67 68 69 74 79 80 81 pwsmulrval ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) ( .r ‘ ( ℂfld ↑s ℂ ) ) ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) ) = ( ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) ∘f · ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) ) )
83 33 adantr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑧 ∈ ℂ ) → ( 𝑎 ‘ 𝑘 ) ∈ ℂ )
84 fconstmpt ⊢ ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) = ( 𝑧 ∈ ℂ ↦ ( 𝑎 ‘ 𝑘 ) )
85 84 a1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) = ( 𝑧 ∈ ℂ ↦ ( 𝑎 ‘ 𝑘 ) ) )
86 eqidd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) )
87 69 83 75 85 86 offval2 ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) ∘f · ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
88 82 87 eqtrd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) ( .r ‘ ( ℂfld ↑s ℂ ) ) ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
89 63 adantr ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐸 “ 𝐴 ) ∈ ( SubRing ‘ ( ℂfld ↑s ℂ ) ) )
90 eqid ⊢ ( algSc ‘ ( Poly1 ‘ ℂfld ) ) = ( algSc ‘ ( Poly1 ‘ ℂfld ) )
91 4 57 8 90 evl1sca ⊢ ( ( ℂfld ∈ CRing ∧ ( 𝑎 ‘ 𝑘 ) ∈ ℂ ) → ( 𝐸 ‘ ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ ( 𝑎 ‘ 𝑘 ) ) ) = ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) )
92 56 33 91 sylancr ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐸 ‘ ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ ( 𝑎 ‘ 𝑘 ) ) ) = ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) )
93 eqid ⊢ ( Base ‘ ( Poly1 ‘ ℂfld ) ) = ( Base ‘ ( Poly1 ‘ ℂfld ) )
94 93 67 rhmf ⊢ ( 𝐸 ∈ ( ( Poly1 ‘ ℂfld ) RingHom ( ℂfld ↑s ℂ ) ) → 𝐸 : ( Base ‘ ( Poly1 ‘ ℂfld ) ) ⟶ ( Base ‘ ( ℂfld ↑s ℂ ) ) )
95 59 94 ax-mp ⊢ 𝐸 : ( Base ‘ ( Poly1 ‘ ℂfld ) ) ⟶ ( Base ‘ ( ℂfld ↑s ℂ ) )
96 ffn ⊢ ( 𝐸 : ( Base ‘ ( Poly1 ‘ ℂfld ) ) ⟶ ( Base ‘ ( ℂfld ↑s ℂ ) ) → 𝐸 Fn ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
97 95 96 mp1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝐸 Fn ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
98 93 subrgss ⊢ ( 𝐴 ∈ ( SubRing ‘ ( Poly1 ‘ ℂfld ) ) → 𝐴 ⊆ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
99 60 98 syl ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 𝐴 ⊆ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
100 99 ad2antrr ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝐴 ⊆ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
101 simpll ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝑆 ∈ ( SubRing ‘ ℂfld ) )
102 57 90 1 2 101 3 8 33 subrg1asclcl ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ ( 𝑎 ‘ 𝑘 ) ) ∈ 𝐴 ↔ ( 𝑎 ‘ 𝑘 ) ∈ 𝑆 ) )
103 32 102 mpbird ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ ( 𝑎 ‘ 𝑘 ) ) ∈ 𝐴 )
104 fnfvima ⊢ ( ( 𝐸 Fn ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ 𝐴 ⊆ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ ( 𝑎 ‘ 𝑘 ) ) ∈ 𝐴 ) → ( 𝐸 ‘ ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ ( 𝑎 ‘ 𝑘 ) ) ) ∈ ( 𝐸 “ 𝐴 ) )
105 97 100 103 104 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐸 ‘ ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ ( 𝑎 ‘ 𝑘 ) ) ) ∈ ( 𝐸 “ 𝐴 ) )
106 92 105 eqeltrrd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) ∈ ( 𝐸 “ 𝐴 ) )
107 67 subrgss ⊢ ( ( 𝐸 “ 𝐴 ) ∈ ( SubRing ‘ ( ℂfld ↑s ℂ ) ) → ( 𝐸 “ 𝐴 ) ⊆ ( Base ‘ ( ℂfld ↑s ℂ ) ) )
108 89 107 syl ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐸 “ 𝐴 ) ⊆ ( Base ‘ ( ℂfld ↑s ℂ ) ) )
109 60 ad2antrr ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝐴 ∈ ( SubRing ‘ ( Poly1 ‘ ℂfld ) ) )
110 eqid ⊢ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) = ( mulGrp ‘ ( Poly1 ‘ ℂfld ) )
111 110 subrgsubm ⊢ ( 𝐴 ∈ ( SubRing ‘ ( Poly1 ‘ ℂfld ) ) → 𝐴 ∈ ( SubMnd ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) )
112 109 111 syl ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝐴 ∈ ( SubMnd ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) )
113 30 adantl ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝑘 ∈ ℕ0 )
114 eqid ⊢ ( var1 ‘ ℂfld ) = ( var1 ‘ ℂfld )
115 114 101 1 2 3 subrgvr1cl ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( var1 ‘ ℂfld ) ∈ 𝐴 )
116 eqid ⊢ ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) )
117 116 submmulgcl ⊢ ( ( 𝐴 ∈ ( SubMnd ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ∧ 𝑘 ∈ ℕ0 ∧ ( var1 ‘ ℂfld ) ∈ 𝐴 ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ∈ 𝐴 )
118 112 113 115 117 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ∈ 𝐴 )
119 fnfvima ⊢ ( ( 𝐸 Fn ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ 𝐴 ⊆ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ∈ 𝐴 ) → ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ∈ ( 𝐸 “ 𝐴 ) )
120 97 100 118 119 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ∈ ( 𝐸 “ 𝐴 ) )
121 108 120 sseldd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ∈ ( Base ‘ ( ℂfld ↑s ℂ ) ) )
122 7 8 67 68 69 121 pwselbas ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) : ℂ ⟶ ℂ )
123 122 feqmptd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) = ( 𝑧 ∈ ℂ ↦ ( ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ‘ 𝑧 ) ) )
124 56 a1i ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑧 ∈ ℂ ) → ℂfld ∈ CRing )
125 simpr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
126 4 114 8 57 93 124 125 evl1vard ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑧 ∈ ℂ ) → ( ( var1 ‘ ℂfld ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ ( ( 𝐸 ‘ ( var1 ‘ ℂfld ) ) ‘ 𝑧 ) = 𝑧 ) )
127 eqid ⊢ ( .g ‘ ( mulGrp ‘ ℂfld ) ) = ( .g ‘ ( mulGrp ‘ ℂfld ) )
128 113 adantr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑧 ∈ ℂ ) → 𝑘 ∈ ℕ0 )
129 4 57 8 93 124 125 126 116 127 128 evl1expd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ ( ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ‘ 𝑧 ) = ( 𝑘 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑧 ) ) )
130 129 simprd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ‘ 𝑧 ) = ( 𝑘 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑧 ) )
131 cnfldexp ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑧 ) = ( 𝑧 ↑ 𝑘 ) )
132 125 128 131 syl2anc ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑧 ∈ ℂ ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑧 ) = ( 𝑧 ↑ 𝑘 ) )
133 130 132 eqtrd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ‘ 𝑧 ) = ( 𝑧 ↑ 𝑘 ) )
134 133 mpteq2dva ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑧 ∈ ℂ ↦ ( ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ‘ 𝑧 ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) )
135 123 134 eqtrd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) )
136 135 120 eqeltrrd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) ∈ ( 𝐸 “ 𝐴 ) )
137 81 subrgmcl ⊢ ( ( ( 𝐸 “ 𝐴 ) ∈ ( SubRing ‘ ( ℂfld ↑s ℂ ) ) ∧ ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) ∈ ( 𝐸 “ 𝐴 ) ∧ ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) ∈ ( 𝐸 “ 𝐴 ) ) → ( ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) ( .r ‘ ( ℂfld ↑s ℂ ) ) ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( 𝐸 “ 𝐴 ) )
138 89 106 136 137 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ℂ × { ( 𝑎 ‘ 𝑘 ) } ) ( .r ‘ ( ℂfld ↑s ℂ ) ) ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( 𝐸 “ 𝐴 ) )
139 88 138 eqeltrrd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑧 ∈ ℂ ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( 𝐸 “ 𝐴 ) )
140 139 fmpttd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( 𝑧 ∈ ℂ ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) : ( 0 ... 𝑛 ) ⟶ ( 𝐸 “ 𝐴 ) )
141 40 12 139 44 fsuppmptdm ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( 𝑧 ∈ ℂ ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) finSupp ( 0g ‘ ( ℂfld ↑s ℂ ) ) )
142 9 55 12 66 140 141 gsumsubmcl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( ( ℂfld ↑s ℂ ) Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( 𝑧 ∈ ℂ ↦ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ∈ ( 𝐸 “ 𝐴 ) )
143 51 142 eqeltrrd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( 𝐸 “ 𝐴 ) )
144 eleq1 ⊢ ( 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → ( 𝑓 ∈ ( 𝐸 “ 𝐴 ) ↔ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( 𝐸 “ 𝐴 ) ) )
145 143 144 syl5ibrcom ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → 𝑓 ∈ ( 𝐸 “ 𝐴 ) ) )
146 145 rexlimdvva ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → 𝑓 ∈ ( 𝐸 “ 𝐴 ) ) )
147 6 146 syl5 ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( 𝑓 ∈ ( Poly ‘ 𝑆 ) → 𝑓 ∈ ( 𝐸 “ 𝐴 ) ) )
148 ffun ⊢ ( 𝐸 : ( Base ‘ ( Poly1 ‘ ℂfld ) ) ⟶ ( Base ‘ ( ℂfld ↑s ℂ ) ) → Fun 𝐸 )
149 95 148 ax-mp ⊢ Fun 𝐸
150 fvelima ⊢ ( ( Fun 𝐸 ∧ 𝑓 ∈ ( 𝐸 “ 𝐴 ) ) → ∃ 𝑎 ∈ 𝐴 ( 𝐸 ‘ 𝑎 ) = 𝑓 )
151 149 150 mpan ⊢ ( 𝑓 ∈ ( 𝐸 “ 𝐴 ) → ∃ 𝑎 ∈ 𝐴 ( 𝐸 ‘ 𝑎 ) = 𝑓 )
152 99 sselda ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
153 eqid ⊢ ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) = ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) )
154 eqid ⊢ ( coe1 ‘ 𝑎 ) = ( coe1 ‘ 𝑎 )
155 57 114 93 153 110 116 154 ply1coe ⊢ ( ( ℂfld ∈ Ring ∧ 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ) → 𝑎 = ( ( Poly1 ‘ ℂfld ) Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ) )
156 13 152 155 sylancr ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 = ( ( Poly1 ‘ ℂfld ) Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ) )
157 156 fveq2d ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐸 ‘ 𝑎 ) = ( 𝐸 ‘ ( ( Poly1 ‘ ℂfld ) Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ) ) )
158 eqid ⊢ ( 0g ‘ ( Poly1 ‘ ℂfld ) ) = ( 0g ‘ ( Poly1 ‘ ℂfld ) )
159 57 ply1ring ⊢ ( ℂfld ∈ Ring → ( Poly1 ‘ ℂfld ) ∈ Ring )
160 13 159 ax-mp ⊢ ( Poly1 ‘ ℂfld ) ∈ Ring
161 ringcmn ⊢ ( ( Poly1 ‘ ℂfld ) ∈ Ring → ( Poly1 ‘ ℂfld ) ∈ CMnd )
162 160 161 mp1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( Poly1 ‘ ℂfld ) ∈ CMnd )
163 ringmnd ⊢ ( ( ℂfld ↑s ℂ ) ∈ Ring → ( ℂfld ↑s ℂ ) ∈ Mnd )
164 53 163 mp1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ℂfld ↑s ℂ ) ∈ Mnd )
165 nn0ex ⊢ ℕ0 ∈ V
166 165 a1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ℕ0 ∈ V )
167 rhmghm ⊢ ( 𝐸 ∈ ( ( Poly1 ‘ ℂfld ) RingHom ( ℂfld ↑s ℂ ) ) → 𝐸 ∈ ( ( Poly1 ‘ ℂfld ) GrpHom ( ℂfld ↑s ℂ ) ) )
168 59 167 ax-mp ⊢ 𝐸 ∈ ( ( Poly1 ‘ ℂfld ) GrpHom ( ℂfld ↑s ℂ ) )
169 ghmmhm ⊢ ( 𝐸 ∈ ( ( Poly1 ‘ ℂfld ) GrpHom ( ℂfld ↑s ℂ ) ) → 𝐸 ∈ ( ( Poly1 ‘ ℂfld ) MndHom ( ℂfld ↑s ℂ ) ) )
170 168 169 mp1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → 𝐸 ∈ ( ( Poly1 ‘ ℂfld ) MndHom ( ℂfld ↑s ℂ ) ) )
171 57 ply1lmod ⊢ ( ℂfld ∈ Ring → ( Poly1 ‘ ℂfld ) ∈ LMod )
172 13 171 mp1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( Poly1 ‘ ℂfld ) ∈ LMod )
173 16 ad2antrr ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑆 ⊆ ℂ )
174 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
175 154 3 2 174 coe1f ⊢ ( 𝑎 ∈ 𝐴 → ( coe1 ‘ 𝑎 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
176 1 subrgbas ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 𝑆 = ( Base ‘ 𝑅 ) )
177 176 feq3d ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( ( coe1 ‘ 𝑎 ) : ℕ0 ⟶ 𝑆 ↔ ( coe1 ‘ 𝑎 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) ) )
178 175 177 syl5ibr ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( 𝑎 ∈ 𝐴 → ( coe1 ‘ 𝑎 ) : ℕ0 ⟶ 𝑆 ) )
179 178 imp ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( coe1 ‘ 𝑎 ) : ℕ0 ⟶ 𝑆 )
180 179 ffvelrnda ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ∈ 𝑆 )
181 173 180 sseldd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ∈ ℂ )
182 110 ringmgp ⊢ ( ( Poly1 ‘ ℂfld ) ∈ Ring → ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ∈ Mnd )
183 160 182 mp1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ∈ Mnd )
184 simpr ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
185 114 57 93 vr1cl ⊢ ( ℂfld ∈ Ring → ( var1 ‘ ℂfld ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
186 13 185 mp1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( var1 ‘ ℂfld ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
187 110 93 mgpbas ⊢ ( Base ‘ ( Poly1 ‘ ℂfld ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) )
188 187 116 mulgnn0cl ⊢ ( ( ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ∈ Mnd ∧ 𝑘 ∈ ℕ0 ∧ ( var1 ‘ ℂfld ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
189 183 184 186 188 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
190 57 ply1sca ⊢ ( ℂfld ∈ Ring → ℂfld = ( Scalar ‘ ( Poly1 ‘ ℂfld ) ) )
191 13 190 ax-mp ⊢ ℂfld = ( Scalar ‘ ( Poly1 ‘ ℂfld ) )
192 93 191 153 8 lmodvscl ⊢ ( ( ( Poly1 ‘ ℂfld ) ∈ LMod ∧ ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ∈ ℂ ∧ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
193 172 181 189 192 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
194 193 fmpttd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) : ℕ0 ⟶ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
195 165 mptex ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ∈ V
196 funmpt ⊢ Fun ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) )
197 fvex ⊢ ( 0g ‘ ( Poly1 ‘ ℂfld ) ) ∈ V
198 195 196 197 3pm3.2i ⊢ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ∧ ( 0g ‘ ( Poly1 ‘ ℂfld ) ) ∈ V )
199 198 a1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ∧ ( 0g ‘ ( Poly1 ‘ ℂfld ) ) ∈ V ) )
200 154 93 57 21 coe1sfi ⊢ ( 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) → ( coe1 ‘ 𝑎 ) finSupp 0 )
201 152 200 syl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( coe1 ‘ 𝑎 ) finSupp 0 )
202 201 fsuppimpd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( coe1 ‘ 𝑎 ) supp 0 ) ∈ Fin )
203 179 feqmptd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( coe1 ‘ 𝑎 ) = ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ) )
204 203 oveq1d ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( coe1 ‘ 𝑎 ) supp 0 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ) supp 0 ) )
205 eqimss2 ⊢ ( ( ( coe1 ‘ 𝑎 ) supp 0 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ) supp 0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ) supp 0 ) ⊆ ( ( coe1 ‘ 𝑎 ) supp 0 ) )
206 204 205 syl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ) supp 0 ) ⊆ ( ( coe1 ‘ 𝑎 ) supp 0 ) )
207 13 171 mp1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( Poly1 ‘ ℂfld ) ∈ LMod )
208 93 191 153 21 158 lmod0vs ⊢ ( ( ( Poly1 ‘ ℂfld ) ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ) → ( 0 ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) 𝑥 ) = ( 0g ‘ ( Poly1 ‘ ℂfld ) ) )
209 207 208 sylan ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ) → ( 0 ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) 𝑥 ) = ( 0g ‘ ( Poly1 ‘ ℂfld ) ) )
210 c0ex ⊢ 0 ∈ V
211 210 a1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → 0 ∈ V )
212 206 209 180 189 211 suppssov1 ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) supp ( 0g ‘ ( Poly1 ‘ ℂfld ) ) ) ⊆ ( ( coe1 ‘ 𝑎 ) supp 0 ) )
213 suppssfifsupp ⊢ ( ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ∧ ( 0g ‘ ( Poly1 ‘ ℂfld ) ) ∈ V ) ∧ ( ( ( coe1 ‘ 𝑎 ) supp 0 ) ∈ Fin ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) supp ( 0g ‘ ( Poly1 ‘ ℂfld ) ) ) ⊆ ( ( coe1 ‘ 𝑎 ) supp 0 ) ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) finSupp ( 0g ‘ ( Poly1 ‘ ℂfld ) ) )
214 199 202 212 213 syl12anc ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) finSupp ( 0g ‘ ( Poly1 ‘ ℂfld ) ) )
215 93 158 162 164 166 170 194 214 gsummhm ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ℂfld ↑s ℂ ) Σg ( 𝐸 ∘ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ) ) = ( 𝐸 ‘ ( ( Poly1 ‘ ℂfld ) Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ) ) )
216 95 a1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → 𝐸 : ( Base ‘ ( Poly1 ‘ ℂfld ) ) ⟶ ( Base ‘ ( ℂfld ↑s ℂ ) ) )
217 216 193 cofmpt ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐸 ∘ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ) )
218 13 a1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ℂfld ∈ Ring )
219 10 a1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ℂ ∈ V )
220 95 ffvelrni ⊢ ( ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) → ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ∈ ( Base ‘ ( ℂfld ↑s ℂ ) ) )
221 193 220 syl ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ∈ ( Base ‘ ( ℂfld ↑s ℂ ) ) )
222 7 8 67 218 219 221 pwselbas ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) : ℂ ⟶ ℂ )
223 222 feqmptd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) = ( 𝑧 ∈ ℂ ↦ ( ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ‘ 𝑧 ) ) )
224 56 a1i ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ℂfld ∈ CRing )
225 simpr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
226 4 114 8 57 93 224 225 evl1vard ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( ( var1 ‘ ℂfld ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ ( ( 𝐸 ‘ ( var1 ‘ ℂfld ) ) ‘ 𝑧 ) = 𝑧 ) )
227 184 adantr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → 𝑘 ∈ ℕ0 )
228 4 57 8 93 224 225 226 116 127 227 evl1expd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ ( ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ‘ 𝑧 ) = ( 𝑘 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑧 ) ) )
229 225 227 131 syl2anc ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑧 ) = ( 𝑧 ↑ 𝑘 ) )
230 229 eqeq2d ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( ( ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ‘ 𝑧 ) = ( 𝑘 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑧 ) ↔ ( ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ‘ 𝑧 ) = ( 𝑧 ↑ 𝑘 ) ) )
231 230 anbi2d ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( ( ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ ( ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ‘ 𝑧 ) = ( 𝑘 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑧 ) ) ↔ ( ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ ( ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ‘ 𝑧 ) = ( 𝑧 ↑ 𝑘 ) ) ) )
232 228 231 mpbid ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ ( ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ‘ 𝑧 ) = ( 𝑧 ↑ 𝑘 ) ) )
233 181 adantr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ∈ ℂ )
234 4 57 8 93 224 225 232 233 153 80 evl1vsd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ ( ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ‘ 𝑧 ) = ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
235 234 simprd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ‘ 𝑧 ) = ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
236 235 mpteq2dva ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ ( ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ‘ 𝑧 ) ) = ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
237 223 236 eqtrd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) = ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
238 237 mpteq2dva ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
239 217 238 eqtrd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐸 ∘ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
240 239 oveq2d ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ℂfld ↑s ℂ ) Σg ( 𝐸 ∘ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ) ) = ( ( ℂfld ↑s ℂ ) Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
241 157 215 240 3eqtr2d ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐸 ‘ 𝑎 ) = ( ( ℂfld ↑s ℂ ) Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
242 10 a1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ℂ ∈ V )
243 13 14 mp1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ℂfld ∈ CMnd )
244 181 adantlr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ∈ ℂ )
245 37 adantll ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
246 244 245 mulcld ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
247 246 anasss ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
248 165 mptex ⊢ ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∈ V
249 funmpt ⊢ Fun ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
250 248 249 43 3pm3.2i ⊢ ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( 0g ‘ ( ℂfld ↑s ℂ ) ) ∈ V )
251 250 a1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( 0g ‘ ( ℂfld ↑s ℂ ) ) ∈ V ) )
252 fzfid ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ∈ Fin )
253 eldifn ⊢ ( 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) → ¬ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) )
254 253 adantl ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ¬ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) )
255 152 ad2antrr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
256 eldifi ⊢ ( 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) → 𝑘 ∈ ℕ0 )
257 256 adantl ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → 𝑘 ∈ ℕ0 )
258 eqid ⊢ ( deg1 ‘ ℂfld ) = ( deg1 ‘ ℂfld )
259 258 57 93 21 154 deg1ge ⊢ ( ( 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ 𝑘 ∈ ℕ0 ∧ ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ≠ 0 ) → 𝑘 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) )
260 259 3expia ⊢ ( ( 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ) )
261 255 257 260 syl2anc ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ) )
262 0xr ⊢ 0 ∈ ℝ*
263 258 57 93 deg1xrcl ⊢ ( 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℝ* )
264 152 263 syl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℝ* )
265 264 ad2antrr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℝ* )
266 xrmax2 ⊢ ( ( 0 ∈ ℝ* ∧ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℝ* ) → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) )
267 262 265 266 sylancr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) )
268 257 nn0red ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → 𝑘 ∈ ℝ )
269 268 rexrd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → 𝑘 ∈ ℝ* )
270 ifcl ⊢ ( ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℝ* )
271 265 262 270 sylancl ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℝ* )
272 xrletr ⊢ ( ( 𝑘 ∈ ℝ* ∧ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℝ* ∧ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℝ* ) → ( ( 𝑘 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∧ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) → 𝑘 ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) )
273 269 265 271 272 syl3anc ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( 𝑘 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∧ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) → 𝑘 ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) )
274 267 273 mpan2d ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( 𝑘 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) → 𝑘 ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) )
275 261 274 syld ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) )
276 275 257 jctild ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ≠ 0 → ( 𝑘 ∈ ℕ0 ∧ 𝑘 ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) )
277 258 57 93 deg1cl ⊢ ( 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ( ℕ0 ∪ { -∞ } ) )
278 152 277 syl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ( ℕ0 ∪ { -∞ } ) )
279 elun ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ( ℕ0 ∪ { -∞ } ) ↔ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 ∨ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } ) )
280 278 279 sylib ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 ∨ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } ) )
281 nn0ge0 ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 → 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) )
282 281 iftrued ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) = ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) )
283 id ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 )
284 282 283 eqeltrd ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℕ0 )
285 mnflt0 ⊢ -∞ < 0
286 mnfxr ⊢ -∞ ∈ ℝ*
287 xrltnle ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( -∞ < 0 ↔ ¬ 0 ≤ -∞ ) )
288 286 262 287 mp2an ⊢ ( -∞ < 0 ↔ ¬ 0 ≤ -∞ )
289 285 288 mpbi ⊢ ¬ 0 ≤ -∞
290 elsni ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) = -∞ )
291 290 breq2d ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } → ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ↔ 0 ≤ -∞ ) )
292 289 291 mtbiri ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } → ¬ 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) )
293 292 iffalsed ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) = 0 )
294 0nn0 ⊢ 0 ∈ ℕ0
295 293 294 eqeltrdi ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℕ0 )
296 284 295 jaoi ⊢ ( ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 ∨ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } ) → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℕ0 )
297 280 296 syl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℕ0 )
298 297 ad2antrr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℕ0 )
299 fznn0 ⊢ ( if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℕ0 → ( 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ↔ ( 𝑘 ∈ ℕ0 ∧ 𝑘 ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) )
300 298 299 syl ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ↔ ( 𝑘 ∈ ℕ0 ∧ 𝑘 ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) )
301 276 300 sylibrd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) )
302 301 necon1bd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) → ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) = 0 ) )
303 254 302 mpd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) = 0 )
304 303 oveq1d ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 0 · ( 𝑧 ↑ 𝑘 ) ) )
305 256 245 sylan2 ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
306 305 mul02d ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( 0 · ( 𝑧 ↑ 𝑘 ) ) = 0 )
307 304 306 eqtrd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = 0 )
308 307 an32s ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) ∧ 𝑧 ∈ ℂ ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = 0 )
309 308 mpteq2dva ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ 0 ) )
310 fconstmpt ⊢ ( ℂ × { 0 } ) = ( 𝑧 ∈ ℂ ↦ 0 )
311 ringmnd ⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
312 13 311 ax-mp ⊢ ℂfld ∈ Mnd
313 7 21 pws0g ⊢ ( ( ℂfld ∈ Mnd ∧ ℂ ∈ V ) → ( ℂ × { 0 } ) = ( 0g ‘ ( ℂfld ↑s ℂ ) ) )
314 312 10 313 mp2an ⊢ ( ℂ × { 0 } ) = ( 0g ‘ ( ℂfld ↑s ℂ ) )
315 310 314 eqtr3i ⊢ ( 𝑧 ∈ ℂ ↦ 0 ) = ( 0g ‘ ( ℂfld ↑s ℂ ) )
316 309 315 eqtrdi ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 0g ‘ ( ℂfld ↑s ℂ ) ) )
317 316 166 suppss2 ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) supp ( 0g ‘ ( ℂfld ↑s ℂ ) ) ) ⊆ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) )
318 suppssfifsupp ⊢ ( ( ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( 0g ‘ ( ℂfld ↑s ℂ ) ) ∈ V ) ∧ ( ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ∈ Fin ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) supp ( 0g ‘ ( ℂfld ↑s ℂ ) ) ) ⊆ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) finSupp ( 0g ‘ ( ℂfld ↑s ℂ ) ) )
319 251 252 317 318 syl12anc ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) finSupp ( 0g ‘ ( ℂfld ↑s ℂ ) ) )
320 7 8 9 242 166 243 247 319 pwsgsum ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ℂfld ↑s ℂ ) Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) = ( 𝑧 ∈ ℂ ↦ ( ℂfld Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
321 fz0ssnn0 ⊢ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ⊆ ℕ0
322 resmpt ⊢ ( ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ⊆ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↾ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) = ( 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
323 321 322 ax-mp ⊢ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↾ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) = ( 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
324 323 oveq2i ⊢ ( ℂfld Σg ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↾ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) = ( ℂfld Σg ( 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
325 13 14 mp1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ℂfld ∈ CMnd )
326 165 a1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ℕ0 ∈ V )
327 246 fmpttd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) : ℕ0 ⟶ ℂ )
328 307 326 suppss2 ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) supp 0 ) ⊆ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) )
329 165 mptex ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ V
330 funmpt ⊢ Fun ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
331 329 330 210 3pm3.2i ⊢ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∧ 0 ∈ V )
332 331 a1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∧ 0 ∈ V ) )
333 fzfid ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ∈ Fin )
334 suppssfifsupp ⊢ ( ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∧ 0 ∈ V ) ∧ ( ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ∈ Fin ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) supp 0 ) ⊆ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) finSupp 0 )
335 332 333 328 334 syl12anc ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) finSupp 0 )
336 8 21 325 326 327 328 335 gsumres ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( ℂfld Σg ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↾ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) = ( ℂfld Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
337 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) → 𝑘 ∈ ℕ0 )
338 337 246 sylan2 ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
339 333 338 gsumfsum ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( ℂfld Σg ( 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
340 324 336 339 3eqtr3a ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( ℂfld Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
341 340 mpteq2dva ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑧 ∈ ℂ ↦ ( ℂfld Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
342 241 320 341 3eqtrd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐸 ‘ 𝑎 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
343 16 adantr ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → 𝑆 ⊆ ℂ )
344 elplyr ⊢ ( ( 𝑆 ⊆ ℂ ∧ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℕ0 ∧ ( coe1 ‘ 𝑎 ) : ℕ0 ⟶ 𝑆 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ 𝑆 ) )
345 343 297 179 344 syl3anc ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ 𝑆 ) )
346 342 345 eqeltrd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐸 ‘ 𝑎 ) ∈ ( Poly ‘ 𝑆 ) )
347 eleq1 ⊢ ( ( 𝐸 ‘ 𝑎 ) = 𝑓 → ( ( 𝐸 ‘ 𝑎 ) ∈ ( Poly ‘ 𝑆 ) ↔ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) )
348 346 347 syl5ibcom ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐸 ‘ 𝑎 ) = 𝑓 → 𝑓 ∈ ( Poly ‘ 𝑆 ) ) )
349 348 rexlimdva ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( ∃ 𝑎 ∈ 𝐴 ( 𝐸 ‘ 𝑎 ) = 𝑓 → 𝑓 ∈ ( Poly ‘ 𝑆 ) ) )
350 151 349 syl5 ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( 𝑓 ∈ ( 𝐸 “ 𝐴 ) → 𝑓 ∈ ( Poly ‘ 𝑆 ) ) )
351 147 350 impbid ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( 𝑓 ∈ ( Poly ‘ 𝑆 ) ↔ 𝑓 ∈ ( 𝐸 “ 𝐴 ) ) )
352 351 eqrdv ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( Poly ‘ 𝑆 ) = ( 𝐸 “ 𝐴 ) )