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 ffvelcdm ⊢ ( ( 𝑎 : ℕ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 imbitrrid ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( 𝑎 ∈ 𝐴 → ( coe1 ‘ 𝑎 ) : ℕ0 ⟶ 𝑆 ) )
179 178 imp ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( coe1 ‘ 𝑎 ) : ℕ0 ⟶ 𝑆 )
180 179 ffvelcdmda ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ∈ 𝑆 )
181 173 180 sseldd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ∈ ℂ )
182 110 93 mgpbas ⊢ ( Base ‘ ( Poly1 ‘ ℂfld ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) )
183 110 ringmgp ⊢ ( ( Poly1 ‘ ℂfld ) ∈ Ring → ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ∈ Mnd )
184 160 183 mp1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ∈ Mnd )
185 simpr ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
186 114 57 93 vr1cl ⊢ ( ℂfld ∈ Ring → ( var1 ‘ ℂfld ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
187 13 186 mp1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( var1 ‘ ℂfld ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
188 182 116 184 185 187 mulgnn0cld ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
189 57 ply1sca ⊢ ( ℂfld ∈ Ring → ℂfld = ( Scalar ‘ ( Poly1 ‘ ℂfld ) ) )
190 13 189 ax-mp ⊢ ℂfld = ( Scalar ‘ ( Poly1 ‘ ℂfld ) )
191 93 190 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 ) ) )
192 172 181 188 191 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
193 192 fmpttd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) : ℕ0 ⟶ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
194 165 mptex ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ∈ V
195 funmpt ⊢ Fun ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) )
196 fvex ⊢ ( 0g ‘ ( Poly1 ‘ ℂfld ) ) ∈ V
197 194 195 196 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 )
198 197 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 ) )
199 154 93 57 21 coe1sfi ⊢ ( 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) → ( coe1 ‘ 𝑎 ) finSupp 0 )
200 152 199 syl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( coe1 ‘ 𝑎 ) finSupp 0 )
201 200 fsuppimpd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( coe1 ‘ 𝑎 ) supp 0 ) ∈ Fin )
202 179 feqmptd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( coe1 ‘ 𝑎 ) = ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ) )
203 202 oveq1d ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( coe1 ‘ 𝑎 ) supp 0 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ) supp 0 ) )
204 eqimss2 ⊢ ( ( ( coe1 ‘ 𝑎 ) supp 0 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ) supp 0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ) supp 0 ) ⊆ ( ( coe1 ‘ 𝑎 ) supp 0 ) )
205 203 204 syl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ) supp 0 ) ⊆ ( ( coe1 ‘ 𝑎 ) supp 0 ) )
206 13 171 mp1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( Poly1 ‘ ℂfld ) ∈ LMod )
207 93 190 153 21 158 lmod0vs ⊢ ( ( ( Poly1 ‘ ℂfld ) ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ) → ( 0 ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) 𝑥 ) = ( 0g ‘ ( Poly1 ‘ ℂfld ) ) )
208 206 207 sylan ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ) → ( 0 ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) 𝑥 ) = ( 0g ‘ ( Poly1 ‘ ℂfld ) ) )
209 c0ex ⊢ 0 ∈ V
210 209 a1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → 0 ∈ V )
211 205 208 180 188 210 suppssov1 ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) supp ( 0g ‘ ( Poly1 ‘ ℂfld ) ) ) ⊆ ( ( coe1 ‘ 𝑎 ) supp 0 ) )
212 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 ) ) )
213 198 201 211 212 syl12anc ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) finSupp ( 0g ‘ ( Poly1 ‘ ℂfld ) ) )
214 93 158 162 164 166 170 193 213 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 ) ) ) ) ) ) )
215 95 a1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → 𝐸 : ( Base ‘ ( Poly1 ‘ ℂfld ) ) ⟶ ( Base ‘ ( ℂfld ↑s ℂ ) ) )
216 215 192 cofmpt ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐸 ∘ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ) )
217 13 a1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ℂfld ∈ Ring )
218 10 a1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ℂ ∈ V )
219 95 ffvelcdmi ⊢ ( ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) → ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ∈ ( Base ‘ ( ℂfld ↑s ℂ ) ) )
220 192 219 syl ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ∈ ( Base ‘ ( ℂfld ↑s ℂ ) ) )
221 7 8 67 217 218 220 pwselbas ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) : ℂ ⟶ ℂ )
222 221 feqmptd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) = ( 𝑧 ∈ ℂ ↦ ( ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ‘ 𝑧 ) ) )
223 56 a1i ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ℂfld ∈ CRing )
224 simpr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
225 4 114 8 57 93 223 224 evl1vard ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( ( var1 ‘ ℂfld ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ ( ( 𝐸 ‘ ( var1 ‘ ℂfld ) ) ‘ 𝑧 ) = 𝑧 ) )
226 185 adantr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → 𝑘 ∈ ℕ0 )
227 4 57 8 93 223 224 225 116 127 226 evl1expd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ ( ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ‘ 𝑧 ) = ( 𝑘 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑧 ) ) )
228 224 226 131 syl2anc ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑧 ) = ( 𝑧 ↑ 𝑘 ) )
229 228 eqeq2d ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( ( ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ‘ 𝑧 ) = ( 𝑘 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑧 ) ↔ ( ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ‘ 𝑧 ) = ( 𝑧 ↑ 𝑘 ) ) )
230 229 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 ) ) ) ‘ 𝑧 ) = ( 𝑧 ↑ 𝑘 ) ) ) )
231 227 230 mpbid ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ ( ( 𝐸 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ‘ 𝑧 ) = ( 𝑧 ↑ 𝑘 ) ) )
232 181 adantr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ∈ ℂ )
233 4 57 8 93 223 224 231 232 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 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
234 233 simprd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ‘ 𝑧 ) = ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
235 234 mpteq2dva ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ ( ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ‘ 𝑧 ) ) = ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
236 222 235 eqtrd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) = ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
237 236 mpteq2dva ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝐸 ‘ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
238 216 237 eqtrd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐸 ∘ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
239 238 oveq2d ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ℂfld ↑s ℂ ) Σg ( 𝐸 ∘ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ℂfld ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) ) ( var1 ‘ ℂfld ) ) ) ) ) ) = ( ( ℂfld ↑s ℂ ) Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
240 157 214 239 3eqtr2d ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐸 ‘ 𝑎 ) = ( ( ℂfld ↑s ℂ ) Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
241 10 a1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ℂ ∈ V )
242 13 14 mp1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ℂfld ∈ CMnd )
243 181 adantlr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ∈ ℂ )
244 37 adantll ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
245 243 244 mulcld ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
246 245 anasss ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
247 165 mptex ⊢ ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∈ V
248 funmpt ⊢ Fun ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
249 247 248 43 3pm3.2i ⊢ ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( 0g ‘ ( ℂfld ↑s ℂ ) ) ∈ V )
250 249 a1i ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( 0g ‘ ( ℂfld ↑s ℂ ) ) ∈ V ) )
251 fzfid ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ∈ Fin )
252 eldifn ⊢ ( 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) → ¬ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) )
253 252 adantl ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ¬ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) )
254 152 ad2antrr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) )
255 eldifi ⊢ ( 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) → 𝑘 ∈ ℕ0 )
256 255 adantl ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → 𝑘 ∈ ℕ0 )
257 eqid ⊢ ( deg1 ‘ ℂfld ) = ( deg1 ‘ ℂfld )
258 257 57 93 21 154 deg1ge ⊢ ( ( 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ 𝑘 ∈ ℕ0 ∧ ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ≠ 0 ) → 𝑘 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) )
259 258 3expia ⊢ ( ( 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ) )
260 254 256 259 syl2anc ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ) )
261 0xr ⊢ 0 ∈ ℝ*
262 257 57 93 deg1xrcl ⊢ ( 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℝ* )
263 152 262 syl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℝ* )
264 263 ad2antrr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℝ* )
265 xrmax2 ⊢ ( ( 0 ∈ ℝ* ∧ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℝ* ) → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) )
266 261 264 265 sylancr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) )
267 256 nn0red ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → 𝑘 ∈ ℝ )
268 267 rexrd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → 𝑘 ∈ ℝ* )
269 ifcl ⊢ ( ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℝ* )
270 264 261 269 sylancl ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℝ* )
271 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 ) ) )
272 268 264 270 271 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 ) ) )
273 266 272 mpan2d ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( 𝑘 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) → 𝑘 ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) )
274 260 273 syld ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) )
275 274 256 jctild ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ≠ 0 → ( 𝑘 ∈ ℕ0 ∧ 𝑘 ≤ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) )
276 257 57 93 deg1cl ⊢ ( 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ℂfld ) ) → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ( ℕ0 ∪ { -∞ } ) )
277 152 276 syl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ( ℕ0 ∪ { -∞ } ) )
278 elun ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ( ℕ0 ∪ { -∞ } ) ↔ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 ∨ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } ) )
279 277 278 sylib ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 ∨ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } ) )
280 nn0ge0 ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 → 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) )
281 280 iftrued ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) = ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) )
282 id ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 )
283 281 282 eqeltrd ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℕ0 )
284 mnflt0 ⊢ -∞ < 0
285 mnfxr ⊢ -∞ ∈ ℝ*
286 xrltnle ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( -∞ < 0 ↔ ¬ 0 ≤ -∞ ) )
287 285 261 286 mp2an ⊢ ( -∞ < 0 ↔ ¬ 0 ≤ -∞ )
288 284 287 mpbi ⊢ ¬ 0 ≤ -∞
289 elsni ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } → ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) = -∞ )
290 289 breq2d ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } → ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ↔ 0 ≤ -∞ ) )
291 288 290 mtbiri ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } → ¬ 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) )
292 291 iffalsed ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) = 0 )
293 0nn0 ⊢ 0 ∈ ℕ0
294 292 293 eqeltrdi ⊢ ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℕ0 )
295 283 294 jaoi ⊢ ( ( ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ ℕ0 ∨ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) ∈ { -∞ } ) → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℕ0 )
296 279 295 syl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℕ0 )
297 296 ad2antrr ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℕ0 )
298 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 ) ) ) )
299 297 298 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 ) ) ) )
300 275 299 sylibrd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) )
301 300 necon1bd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) → ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) = 0 ) )
302 253 301 mpd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) = 0 )
303 302 oveq1d ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 0 · ( 𝑧 ↑ 𝑘 ) ) )
304 255 244 sylan2 ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
305 304 mul02d ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( 0 · ( 𝑧 ↑ 𝑘 ) ) = 0 )
306 303 305 eqtrd ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = 0 )
307 306 an32s ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) ∧ 𝑧 ∈ ℂ ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = 0 )
308 307 mpteq2dva ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ 0 ) )
309 fconstmpt ⊢ ( ℂ × { 0 } ) = ( 𝑧 ∈ ℂ ↦ 0 )
310 ringmnd ⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
311 13 310 ax-mp ⊢ ℂfld ∈ Mnd
312 7 21 pws0g ⊢ ( ( ℂfld ∈ Mnd ∧ ℂ ∈ V ) → ( ℂ × { 0 } ) = ( 0g ‘ ( ℂfld ↑s ℂ ) ) )
313 311 10 312 mp2an ⊢ ( ℂ × { 0 } ) = ( 0g ‘ ( ℂfld ↑s ℂ ) )
314 309 313 eqtr3i ⊢ ( 𝑧 ∈ ℂ ↦ 0 ) = ( 0g ‘ ( ℂfld ↑s ℂ ) )
315 308 314 eqtrdi ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) → ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 0g ‘ ( ℂfld ↑s ℂ ) ) )
316 315 166 suppss2 ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) supp ( 0g ‘ ( ℂfld ↑s ℂ ) ) ) ⊆ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) )
317 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 ℂ ) ) )
318 250 251 316 317 syl12anc ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) finSupp ( 0g ‘ ( ℂfld ↑s ℂ ) ) )
319 7 8 9 241 166 242 246 318 pwsgsum ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ℂfld ↑s ℂ ) Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝑧 ∈ ℂ ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) = ( 𝑧 ∈ ℂ ↦ ( ℂfld Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
320 fz0ssnn0 ⊢ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ⊆ ℕ0
321 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 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
322 320 321 ax-mp ⊢ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↾ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) = ( 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
323 322 oveq2i ⊢ ( ℂfld Σg ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↾ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) = ( ℂfld Σg ( 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
324 13 14 mp1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ℂfld ∈ CMnd )
325 165 a1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ℕ0 ∈ V )
326 245 fmpttd ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) : ℕ0 ⟶ ℂ )
327 306 325 suppss2 ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) supp 0 ) ⊆ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) )
328 165 mptex ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ V
329 funmpt ⊢ Fun ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
330 328 329 209 3pm3.2i ⊢ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∧ 0 ∈ V )
331 330 a1i ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∧ 0 ∈ V ) )
332 fzfid ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ∈ Fin )
333 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 )
334 331 332 327 333 syl12anc ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) finSupp 0 )
335 8 21 324 325 326 327 334 gsumres ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( ℂfld Σg ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↾ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) ) = ( ℂfld Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
336 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) → 𝑘 ∈ ℕ0 )
337 336 245 sylan2 ⊢ ( ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ) → ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
338 332 337 gsumfsum ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( ℂfld Σg ( 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
339 323 335 338 3eqtr3a ⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑧 ∈ ℂ ) → ( ℂfld Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
340 339 mpteq2dva ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑧 ∈ ℂ ↦ ( ℂfld Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
341 240 319 340 3eqtrd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐸 ‘ 𝑎 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
342 16 adantr ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → 𝑆 ⊆ ℂ )
343 elplyr ⊢ ( ( 𝑆 ⊆ ℂ ∧ if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ∈ ℕ0 ∧ ( coe1 ‘ 𝑎 ) : ℕ0 ⟶ 𝑆 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ 𝑆 ) )
344 342 296 179 343 syl3anc ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 0 ≤ ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , ( ( deg1 ‘ ℂfld ) ‘ 𝑎 ) , 0 ) ) ( ( ( coe1 ‘ 𝑎 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ 𝑆 ) )
345 341 344 eqeltrd ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐸 ‘ 𝑎 ) ∈ ( Poly ‘ 𝑆 ) )
346 eleq1 ⊢ ( ( 𝐸 ‘ 𝑎 ) = 𝑓 → ( ( 𝐸 ‘ 𝑎 ) ∈ ( Poly ‘ 𝑆 ) ↔ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) )
347 345 346 syl5ibcom ⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐸 ‘ 𝑎 ) = 𝑓 → 𝑓 ∈ ( Poly ‘ 𝑆 ) ) )
348 347 rexlimdva ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( ∃ 𝑎 ∈ 𝐴 ( 𝐸 ‘ 𝑎 ) = 𝑓 → 𝑓 ∈ ( Poly ‘ 𝑆 ) ) )
349 151 348 syl5 ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( 𝑓 ∈ ( 𝐸 “ 𝐴 ) → 𝑓 ∈ ( Poly ‘ 𝑆 ) ) )
350 147 349 impbid ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( 𝑓 ∈ ( Poly ‘ 𝑆 ) ↔ 𝑓 ∈ ( 𝐸 “ 𝐴 ) ) )
351 350 eqrdv ⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( Poly ‘ 𝑆 ) = ( 𝐸 “ 𝐴 ) )