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 ‘ 𝑆 ) = ( 𝐸 “ 𝐴 ) )