Theorem plypf1 26177

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.)

Hypotheses

Ref	Expression
plypf1.r	⊢ 𝑅 = (ℂfld ↾s 𝑆)
plypf1.p	⊢ 𝑃 = (Poly1‘𝑅)
plypf1.a	⊢ 𝐴 = (Base‘𝑃)
plypf1.e	⊢ 𝐸 = (eval1‘ℂfld)

Assertion

Ref	Expression
plypf1	⊢ (𝑆 ∈ (SubRing‘ℂfld) → (Poly‘𝑆) = (𝐸 “ 𝐴))

Proof of Theorem plypf1

Dummy variables 𝑓 𝑎 𝑘 𝑛 𝑥 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elply 26160	. . . . 5 ⊢ (𝑓 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))
2	1	simprbi 497	. . . 4 ⊢ (𝑓 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
3		eqid 2736	. . . . . . . . 9 ⊢ (ℂfld ↑s ℂ) = (ℂfld ↑s ℂ)
4		cnfldbas 21356	. . . . . . . . 9 ⊢ ℂ = (Base‘ℂfld)
5		eqid 2736	. . . . . . . . 9 ⊢ (0g‘(ℂfld ↑s ℂ)) = (0g‘(ℂfld ↑s ℂ))
6		cnex 11119	. . . . . . . . . 10 ⊢ ℂ ∈ V
7	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ℂ ∈ V)
8		fzfid 13935	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (0...𝑛) ∈ Fin)
9		cnring 21374	. . . . . . . . . 10 ⊢ ℂfld ∈ Ring
10		ringcmn 20263	. . . . . . . . . 10 ⊢ (ℂfld ∈ Ring → ℂfld ∈ CMnd)
11	9, 10	mp1i 13	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ℂfld ∈ CMnd)
12	4	subrgss 20549	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ⊆ ℂ)
13	12	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ⊆ ℂ)
14		elmapi 8796	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
15	14	ad2antll 730	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
16		subrgsubg 20554	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ∈ (SubGrp‘ℂfld))
17		cnfld0 21376	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 = (0g‘ℂfld)
18	17	subg0cl 19110	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (SubGrp‘ℂfld) → 0 ∈ 𝑆)
19	16, 18	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 0 ∈ 𝑆)
20	19	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 0 ∈ 𝑆)
21	20	snssd 4730	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → {0} ⊆ 𝑆)
22		ssequn2 4129	. . . . . . . . . . . . . . . 16 ⊢ ({0} ⊆ 𝑆 ↔ (𝑆 ∪ {0}) = 𝑆)
23	21, 22	sylib 218	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑆 ∪ {0}) = 𝑆)
24	23	feq3d 6653	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑎:ℕ0⟶(𝑆 ∪ {0}) ↔ 𝑎:ℕ0⟶𝑆))
25	15, 24	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 𝑎:ℕ0⟶𝑆)
26		elfznn0 13574	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0)
27		ffvelcdm 7033	. . . . . . . . . . . . 13 ⊢ ((𝑎:ℕ0⟶𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑎‘𝑘) ∈ 𝑆)
28	25, 26, 27	syl2an 597	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ 𝑆)
29	13, 28	sseldd 3922	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ ℂ)
30	29	adantrl 717	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑎‘𝑘) ∈ ℂ)
31		simprl 771	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑧 ∈ ℂ)
32	26	ad2antll 730	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑘 ∈ ℕ0)
33		expcl 14041	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ)
34	31, 32, 33	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑧↑𝑘) ∈ ℂ)
35	30, 34	mulcld 11165	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → ((𝑎‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
36		eqid 2736	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))
37	6	mptex 7178	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V
38	37	a1i 11	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V)
39		fvex 6853	. . . . . . . . . . 11 ⊢ (0g‘(ℂfld ↑s ℂ)) ∈ V
40	39	a1i 11	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (0g‘(ℂfld ↑s ℂ)) ∈ V)
41	36, 8, 38, 40	fsuppmptdm 9289	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp (0g‘(ℂfld ↑s ℂ)))
42	3, 4, 5, 7, 8, 11, 35, 41	pwsgsum 19957	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))))
43		fzfid 13935	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑧 ∈ ℂ) → (0...𝑛) ∈ Fin)
44	35	anassrs 467	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑛)) → ((𝑎‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
45	43, 44	gsumfsum 21414	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
46	45	mpteq2dva 5178	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
47	42, 46	eqtrd 2771	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
48	3	pwsring 20303	. . . . . . . . . 10 ⊢ ((ℂfld ∈ Ring ∧ ℂ ∈ V) → (ℂfld ↑s ℂ) ∈ Ring)
49	9, 6, 48	mp2an 693	. . . . . . . . 9 ⊢ (ℂfld ↑s ℂ) ∈ Ring
50		ringcmn 20263	. . . . . . . . 9 ⊢ ((ℂfld ↑s ℂ) ∈ Ring → (ℂfld ↑s ℂ) ∈ CMnd)
51	49, 50	mp1i 13	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (ℂfld ↑s ℂ) ∈ CMnd)
52		cncrng 21373	. . . . . . . . . . 11 ⊢ ℂfld ∈ CRing
53		plypf1.e	. . . . . . . . . . . 12 ⊢ 𝐸 = (eval1‘ℂfld)
54		eqid 2736	. . . . . . . . . . . 12 ⊢ (Poly1‘ℂfld) = (Poly1‘ℂfld)
55	53, 54, 3, 4	evl1rhm 22297	. . . . . . . . . . 11 ⊢ (ℂfld ∈ CRing → 𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂfld ↑s ℂ)))
56	52, 55	ax-mp 5	. . . . . . . . . 10 ⊢ 𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂfld ↑s ℂ))
57		plypf1.r	. . . . . . . . . . . 12 ⊢ 𝑅 = (ℂfld ↾s 𝑆)
58		plypf1.p	. . . . . . . . . . . 12 ⊢ 𝑃 = (Poly1‘𝑅)
59		plypf1.a	. . . . . . . . . . . 12 ⊢ 𝐴 = (Base‘𝑃)
60	54, 57, 58, 59	subrgply1 22196	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
61	60	adantr 480	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
62		rhmima 20581	. . . . . . . . . 10 ⊢ ((𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂfld ↑s ℂ)) ∧ 𝐴 ∈ (SubRing‘(Poly1‘ℂfld))) → (𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)))
63	56, 61, 62	sylancr 588	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)))
64		subrgsubg 20554	. . . . . . . . 9 ⊢ ((𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)) → (𝐸 “ 𝐴) ∈ (SubGrp‘(ℂfld ↑s ℂ)))
65		subgsubm 19124	. . . . . . . . 9 ⊢ ((𝐸 “ 𝐴) ∈ (SubGrp‘(ℂfld ↑s ℂ)) → (𝐸 “ 𝐴) ∈ (SubMnd‘(ℂfld ↑s ℂ)))
66	63, 64, 65	3syl 18	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝐸 “ 𝐴) ∈ (SubMnd‘(ℂfld ↑s ℂ)))
67		eqid 2736	. . . . . . . . . . . 12 ⊢ (Base‘(ℂfld ↑s ℂ)) = (Base‘(ℂfld ↑s ℂ))
68	9	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ℂfld ∈ Ring)
69	6	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ℂ ∈ V)
70		fconst6g 6729	. . . . . . . . . . . . . 14 ⊢ ((𝑎‘𝑘) ∈ ℂ → (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)
71	29, 70	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)
72	3, 4, 67	pwselbasb 17451	. . . . . . . . . . . . . 14 ⊢ ((ℂfld ∈ Ring ∧ ℂ ∈ V) → ((ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ))
73	9, 6, 72	mp2an 693	. . . . . . . . . . . . 13 ⊢ ((ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)
74	71, 73	sylibr 234	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld ↑s ℂ)))
75	34	anass1rs 656	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑧↑𝑘) ∈ ℂ)
76	75	fmpttd 7067	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ)
77	3, 4, 67	pwselbasb 17451	. . . . . . . . . . . . . 14 ⊢ ((ℂfld ∈ Ring ∧ ℂ ∈ V) → ((𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ))
78	9, 6, 77	mp2an 693	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ)
79	76, 78	sylibr 234	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld ↑s ℂ)))
80		cnfldmul 21360	. . . . . . . . . . . 12 ⊢ · = (.r‘ℂfld)
81		eqid 2736	. . . . . . . . . . . 12 ⊢ (.r‘(ℂfld ↑s ℂ)) = (.r‘(ℂfld ↑s ℂ))
82	3, 67, 68, 69, 74, 79, 80, 81	pwsmulrval 17455	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = ((ℂ × {(𝑎‘𝑘)}) ∘f · (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))))
83	29	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑎‘𝑘) ∈ ℂ)
84		fconstmpt 5693	. . . . . . . . . . . . 13 ⊢ (ℂ × {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘))
85	84	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘)))
86		eqidd 2737	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))
87	69, 83, 75, 85, 86	offval2 7651	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)}) ∘f · (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))
88	82, 87	eqtrd 2771	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))
89	63	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)))
90		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (algSc‘(Poly1‘ℂfld)) = (algSc‘(Poly1‘ℂfld))
91	53, 54, 4, 90	evl1sca 22299	. . . . . . . . . . . . 13 ⊢ ((ℂfld ∈ CRing ∧ (𝑎‘𝑘) ∈ ℂ) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) = (ℂ × {(𝑎‘𝑘)}))
92	52, 29, 91	sylancr 588	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) = (ℂ × {(𝑎‘𝑘)}))
93		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Poly1‘ℂfld)) = (Base‘(Poly1‘ℂfld))
94	93, 67	rhmf 20464	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂfld ↑s ℂ)) → 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld ↑s ℂ)))
95	56, 94	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld ↑s ℂ))
96		ffn 6668	. . . . . . . . . . . . . 14 ⊢ (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld ↑s ℂ)) → 𝐸 Fn (Base‘(Poly1‘ℂfld)))
97	95, 96	mp1i 13	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐸 Fn (Base‘(Poly1‘ℂfld)))
98	93	subrgss 20549	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (SubRing‘(Poly1‘ℂfld)) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
99	60, 98	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
100	99	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
101		simpll 767	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ∈ (SubRing‘ℂfld))
102	54, 90, 57, 58, 101, 59, 4, 29	subrg1asclcl 22225	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴 ↔ (𝑎‘𝑘) ∈ 𝑆))
103	28, 102	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴)
104		fnfvima 7188	. . . . . . . . . . . . 13 ⊢ ((𝐸 Fn (Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆ (Base‘(Poly1‘ℂfld)) ∧ ((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) ∈ (𝐸 “ 𝐴))
105	97, 100, 103, 104	syl3anc 1374	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) ∈ (𝐸 “ 𝐴))
106	92, 105	eqeltrrd 2837	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴))
107	67	subrgss 20549	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)) → (𝐸 “ 𝐴) ⊆ (Base‘(ℂfld ↑s ℂ)))
108	89, 107	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸 “ 𝐴) ⊆ (Base‘(ℂfld ↑s ℂ)))
109	60	ad2antrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
110		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (mulGrp‘(Poly1‘ℂfld)) = (mulGrp‘(Poly1‘ℂfld))
111	110	subrgsubm 20562	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ (SubRing‘(Poly1‘ℂfld)) → 𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))))
112	109, 111	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))))
113	26	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑘 ∈ ℕ0)
114		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (var1‘ℂfld) = (var1‘ℂfld)
115	114, 101, 57, 58, 59	subrgvr1cl 22227	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (var1‘ℂfld) ∈ 𝐴)
116		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (.g‘(mulGrp‘(Poly1‘ℂfld))) = (.g‘(mulGrp‘(Poly1‘ℂfld)))
117	116	submmulgcl 19093	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))) ∧ 𝑘 ∈ ℕ0 ∧ (var1‘ℂfld) ∈ 𝐴) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
118	112, 113, 115, 117	syl3anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
119		fnfvima 7188	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 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 1374	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (𝐸 “ 𝐴))
121	108, 120	sseldd 3922	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(ℂfld ↑s ℂ)))
122	3, 4, 67, 68, 69, 121	pwselbas 17452	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))):ℂ⟶ℂ)
123	122	feqmptd 6908	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) = (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧)))
124	52	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ℂfld ∈ CRing)
125		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
126	53, 114, 4, 54, 93, 124, 125	evl1vard 22302	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧))
127		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
128	113	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0)
129	53, 54, 4, 93, 124, 125, 126, 116, 127, 128	evl1expd 22310	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (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 495	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧))
131		cnfldexp 21385	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘))
132	125, 128, 131	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘))
133	130, 132	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘))
134	133	mpteq2dva 5178	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))
135	123, 134	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))
136	135, 120	eqeltrrd 2837	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴))
137	81	subrgmcl 20561	. . . . . . . . . . 11 ⊢ (((𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)) ∧ (ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴) ∧ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
138	89, 106, 136, 137	syl3anc 1374	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
139	88, 138	eqeltrrd 2837	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
140	139	fmpttd 7067	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))):(0...𝑛)⟶(𝐸 “ 𝐴))
141	36, 8, 139, 40	fsuppmptdm 9289	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp (0g‘(ℂfld ↑s ℂ)))
142	5, 51, 8, 66, 140, 141	gsumsubmcl 19894	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) ∈ (𝐸 “ 𝐴))
143	47, 142	eqeltrrd 2837	. . . . . 6 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
144		eleq1 2824	. . . . . 6 ⊢ (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → (𝑓 ∈ (𝐸 “ 𝐴) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)))
145	143, 144	syl5ibrcom 247	. . . . 5 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴)))
146	145	rexlimdvva 3194	. . . 4 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴)))
147	2, 146	syl5 34	. . 3 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) → 𝑓 ∈ (𝐸 “ 𝐴)))
148		ffun 6671	. . . . . 6 ⊢ (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld ↑s ℂ)) → Fun 𝐸)
149	95, 148	ax-mp 5	. . . . 5 ⊢ Fun 𝐸
150		fvelima 6905	. . . . 5 ⊢ ((Fun 𝐸 ∧ 𝑓 ∈ (𝐸 “ 𝐴)) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓)
151	149, 150	mpan 691	. . . 4 ⊢ (𝑓 ∈ (𝐸 “ 𝐴) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓)
152	99	sselda 3921	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ (Base‘(Poly1‘ℂfld)))
153		eqid 2736	. . . . . . . . . . . 12 ⊢ ( ·𝑠 ‘(Poly1‘ℂfld)) = ( ·𝑠 ‘(Poly1‘ℂfld))
154		eqid 2736	. . . . . . . . . . . 12 ⊢ (coe1‘𝑎) = (coe1‘𝑎)
155	54, 114, 93, 153, 110, 116, 154	ply1coe 22263	. . . . . . . . . . 11 ⊢ ((ℂfld ∈ Ring ∧ 𝑎 ∈ (Base‘(Poly1‘ℂfld))) → 𝑎 = ((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
156	9, 152, 155	sylancr 588	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑎 = ((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
157	156	fveq2d 6844	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝐸‘((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))))
158		eqid 2736	. . . . . . . . . 10 ⊢ (0g‘(Poly1‘ℂfld)) = (0g‘(Poly1‘ℂfld))
159	54	ply1ring 22211	. . . . . . . . . . . 12 ⊢ (ℂfld ∈ Ring → (Poly1‘ℂfld) ∈ Ring)
160	9, 159	ax-mp 5	. . . . . . . . . . 11 ⊢ (Poly1‘ℂfld) ∈ Ring
161		ringcmn 20263	. . . . . . . . . . 11 ⊢ ((Poly1‘ℂfld) ∈ Ring → (Poly1‘ℂfld) ∈ CMnd)
162	160, 161	mp1i 13	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (Poly1‘ℂfld) ∈ CMnd)
163		ringmnd 20224	. . . . . . . . . . 11 ⊢ ((ℂfld ↑s ℂ) ∈ Ring → (ℂfld ↑s ℂ) ∈ Mnd)
164	49, 163	mp1i 13	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (ℂfld ↑s ℂ) ∈ Mnd)
165		nn0ex 12443	. . . . . . . . . . 11 ⊢ ℕ0 ∈ V
166	165	a1i 11	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℕ0 ∈ V)
167		rhmghm 20463	. . . . . . . . . . . 12 ⊢ (𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂfld ↑s ℂ)) → 𝐸 ∈ ((Poly1‘ℂfld) GrpHom (ℂfld ↑s ℂ)))
168	56, 167	ax-mp 5	. . . . . . . . . . 11 ⊢ 𝐸 ∈ ((Poly1‘ℂfld) GrpHom (ℂfld ↑s ℂ))
169		ghmmhm 19201	. . . . . . . . . . 11 ⊢ (𝐸 ∈ ((Poly1‘ℂfld) GrpHom (ℂfld ↑s ℂ)) → 𝐸 ∈ ((Poly1‘ℂfld) MndHom (ℂfld ↑s ℂ)))
170	168, 169	mp1i 13	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝐸 ∈ ((Poly1‘ℂfld) MndHom (ℂfld ↑s ℂ)))
171	54	ply1lmod 22215	. . . . . . . . . . . . 13 ⊢ (ℂfld ∈ Ring → (Poly1‘ℂfld) ∈ LMod)
172	9, 171	mp1i 13	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (Poly1‘ℂfld) ∈ LMod)
173	12	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑆 ⊆ ℂ)
174		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝑅) = (Base‘𝑅)
175	154, 59, 58, 174	coe1f 22175	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ 𝐴 → (coe1‘𝑎):ℕ0⟶(Base‘𝑅))
176	57	subrgbas 20558	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 = (Base‘𝑅))
177	176	feq3d 6653	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → ((coe1‘𝑎):ℕ0⟶𝑆 ↔ (coe1‘𝑎):ℕ0⟶(Base‘𝑅)))
178	175, 177	imbitrrid 246	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (𝑎 ∈ 𝐴 → (coe1‘𝑎):ℕ0⟶𝑆))
179	178	imp 406	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎):ℕ0⟶𝑆)
180	179	ffvelcdmda 7036	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝑎)‘𝑘) ∈ 𝑆)
181	173, 180	sseldd 3922	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝑎)‘𝑘) ∈ ℂ)
182	110, 93	mgpbas 20126	. . . . . . . . . . . . 13 ⊢ (Base‘(Poly1‘ℂfld)) = (Base‘(mulGrp‘(Poly1‘ℂfld)))
183	110	ringmgp 20220	. . . . . . . . . . . . . 14 ⊢ ((Poly1‘ℂfld) ∈ Ring → (mulGrp‘(Poly1‘ℂfld)) ∈ Mnd)
184	160, 183	mp1i 13	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (mulGrp‘(Poly1‘ℂfld)) ∈ Mnd)
185		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
186	114, 54, 93	vr1cl 22181	. . . . . . . . . . . . . 14 ⊢ (ℂfld ∈ Ring → (var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)))
187	9, 186	mp1i 13	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)))
188	182, 116, 184, 185, 187	mulgnn0cld 19071	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)))
189	54	ply1sca 22216	. . . . . . . . . . . . . 14 ⊢ (ℂfld ∈ Ring → ℂfld = (Scalar‘(Poly1‘ℂfld)))
190	9, 189	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ℂfld = (Scalar‘(Poly1‘ℂfld))
191	93, 190, 153, 4	lmodvscl 20873	. . . . . . . . . . . 12 ⊢ (((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 1374	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(Poly1‘ℂfld)))
193	192	fmpttd 7067	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℕ0⟶(Base‘(Poly1‘ℂfld)))
194	165	mptex 7178	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ V
195		funmpt 6536	. . . . . . . . . . . . 13 ⊢ Fun (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
196		fvex 6853	. . . . . . . . . . . . 13 ⊢ (0g‘(Poly1‘ℂfld)) ∈ V
197	194, 195, 196	3pm3.2i 1341	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ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 11	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (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, 54, 17	coe1sfi 22177	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → (coe1‘𝑎) finSupp 0)
200	152, 199	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) finSupp 0)
201	200	fsuppimpd 9282	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) ∈ Fin)
202	179	feqmptd 6908	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) = (𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)))
203	202	oveq1d 7382	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)) supp 0))
204		eqimss2 3981	. . . . . . . . . . . . 13 ⊢ (((coe1‘𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)) supp 0) → ((𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)) supp 0) ⊆ ((coe1‘𝑎) supp 0))
205	203, 204	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)) supp 0) ⊆ ((coe1‘𝑎) supp 0))
206	9, 171	mp1i 13	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (Poly1‘ℂfld) ∈ LMod)
207	93, 190, 153, 17, 158	lmod0vs 20890	. . . . . . . . . . . . 13 ⊢ (((Poly1‘ℂfld) ∈ LMod ∧ 𝑥 ∈ (Base‘(Poly1‘ℂfld))) → (0( ·𝑠 ‘(Poly1‘ℂfld))𝑥) = (0g‘(Poly1‘ℂfld)))
208	206, 207	sylan 581	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (Base‘(Poly1‘ℂfld))) → (0( ·𝑠 ‘(Poly1‘ℂfld))𝑥) = (0g‘(Poly1‘ℂfld)))
209		c0ex 11138	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
210	209	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 0 ∈ V)
211	205, 208, 180, 188, 210	suppssov1 8147	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) supp (0g‘(Poly1‘ℂfld))) ⊆ ((coe1‘𝑎) supp 0))
212		suppssfifsupp 9293	. . . . . . . . . . 11 ⊢ ((((𝑘 ∈ ℕ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 837	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (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 19913	. . . . . . . . 9 ⊢ ((𝑆 ∈ (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 11	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld ↑s ℂ)))
216	215, 192	cofmpt 7085	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
217	9	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → ℂfld ∈ Ring)
218	6	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → ℂ ∈ V)
219	95	ffvelcdmi 7035	. . . . . . . . . . . . . . . 16 ⊢ ((((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 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ (Base‘(ℂfld ↑s ℂ)))
221	3, 4, 67, 217, 218, 220	pwselbas 17452	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℂ⟶ℂ)
222	221	feqmptd 6908	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) = (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧)))
223	52	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ℂfld ∈ CRing)
224		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
225	53, 114, 4, 54, 93, 223, 224	evl1vard 22302	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧))
226	185	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0)
227	53, 54, 4, 93, 223, 224, 225, 116, 127, 226	evl1expd 22310	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (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 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘))
229	228	eqeq2d 2747	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧) ↔ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘)))
230	229	anbi2d 631	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (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 232	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘)))
232	181	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((coe1‘𝑎)‘𝑘) ∈ ℂ)
233	53, 54, 4, 93, 223, 224, 231, 232, 153, 80	evl1vsd 22309	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (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 495	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧) = (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))
235	234	mpteq2dva 5178	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧)) = (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
236	222, 235	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) = (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
237	236	mpteq2dva 5178	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))
238	216, 237	eqtrd 2771	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))
239	238	oveq2d 7383	. . . . . . . . 9 ⊢ ((𝑆 ∈ (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 2777	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = ((ℂfld ↑s ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))))
241	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℂ ∈ V)
242	9, 10	mp1i 13	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℂfld ∈ CMnd)
243	181	adantlr 716	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝑎)‘𝑘) ∈ ℂ)
244	33	adantll 715	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ)
245	243, 244	mulcld 11165	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
246	245	anasss 466	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
247	165	mptex 7178	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V
248		funmpt 6536	. . . . . . . . . . . 12 ⊢ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
249	247, 248, 39	3pm3.2i 1341	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∧ (0g‘(ℂfld ↑s ℂ)) ∈ V)
250	249	a1i 11	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∧ (0g‘(ℂfld ↑s ℂ)) ∈ V))
251		fzfid 13935	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ∈ Fin)
252		eldifn 4072	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))) → ¬ 𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
253	252	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → ¬ 𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
254	152	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑎 ∈ (Base‘(Poly1‘ℂfld)))
255		eldifi 4071	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))) → 𝑘 ∈ ℕ0)
256	255	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℕ0)
257		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (deg1‘ℂfld) = (deg1‘ℂfld)
258	257, 54, 93, 17, 154	deg1ge 26063	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ (Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0 ∧ ((coe1‘𝑎)‘𝑘) ≠ 0) → 𝑘 ≤ ((deg1‘ℂfld)‘𝑎))
259	258	3expia 1122	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ (Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0) → (((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ ((deg1‘ℂfld)‘𝑎)))
260	254, 256, 259	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ ((deg1‘ℂfld)‘𝑎)))
261		0xr 11192	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ*
262	257, 54, 93	deg1xrcl 26047	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → ((deg1‘ℂfld)‘𝑎) ∈ ℝ*)
263	152, 262	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((deg1‘ℂfld)‘𝑎) ∈ ℝ*)
264	263	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → ((deg1‘ℂfld)‘𝑎) ∈ ℝ*)
265		xrmax2 13128	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0 ∈ ℝ* ∧ ((deg1‘ℂfld)‘𝑎) ∈ ℝ*) → ((deg1‘ℂfld)‘𝑎) ≤ if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))
266	261, 264, 265	sylancr 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → ((deg1‘ℂfld)‘𝑎) ≤ if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))
267	256	nn0red 12499	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ)
268	267	rexrd 11195	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ*)
269		ifcl 4512	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((deg1‘ℂfld)‘𝑎) ∈ ℝ* ∧ 0 ∈ ℝ*) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℝ*)
270	264, 261, 269	sylancl 587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℝ*)
271		xrletr 13109	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℝ* ∧ ((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 1374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑆 ∈ (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 695	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑘 ≤ ((deg1‘ℂfld)‘𝑎) → 𝑘 ≤ if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
274	260, 273	syld 47	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
275	274, 256	jctild 525	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) ≠ 0 → (𝑘 ∈ ℕ0 ∧ 𝑘 ≤ if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))))
276	257, 54, 93	deg1cl 26048	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → ((deg1‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
277	152, 276	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((deg1‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
278		elun 4093	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}) ↔ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((deg1‘ℂfld)‘𝑎) ∈ {-∞}))
279	277, 278	sylib 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((deg1‘ℂfld)‘𝑎) ∈ {-∞}))
280		nn0ge0 12462	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → 0 ≤ ((deg1‘ℂfld)‘𝑎))
281	280	iftrued 4474	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) = ((deg1‘ℂfld)‘𝑎))
282		id 22	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → ((deg1‘ℂfld)‘𝑎) ∈ ℕ0)
283	281, 282	eqeltrd 2836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
284		mnflt0 13076	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ -∞ < 0
285		mnfxr 11202	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ -∞ ∈ ℝ*
286		xrltnle 11212	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*) → (-∞ < 0 ↔ ¬ 0 ≤ -∞))
287	285, 261, 286	mp2an 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (-∞ < 0 ↔ ¬ 0 ≤ -∞)
288	284, 287	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ¬ 0 ≤ -∞
289		elsni 4584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → ((deg1‘ℂfld)‘𝑎) = -∞)
290	289	breq2d 5097	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → (0 ≤ ((deg1‘ℂfld)‘𝑎) ↔ 0 ≤ -∞))
291	288, 290	mtbiri 327	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → ¬ 0 ≤ ((deg1‘ℂfld)‘𝑎))
292	291	iffalsed 4477	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) = 0)
293		0nn0 12452	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ ℕ0
294	292, 293	eqeltrdi 2844	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
295	283, 294	jaoi 858	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((deg1‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((deg1‘ℂfld)‘𝑎) ∈ {-∞}) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
296	279, 295	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
297	296	ad2antrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
298		fznn0 13573	. . . . . . . . . . . . . . . . . . . 20 ⊢ (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 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑆 ∈ (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 259	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))))
301	300	necon1bd 2950	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (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 15	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → ((coe1‘𝑎)‘𝑘) = 0)
303	302	oveq1d 7382	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘)))
304	255, 244	sylan2 594	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑧↑𝑘) ∈ ℂ)
305	304	mul02d 11344	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (0 · (𝑧↑𝑘)) = 0)
306	303, 305	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = 0)
307	306	an32s 653	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) ∧ 𝑧 ∈ ℂ) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = 0)
308	307	mpteq2dva 5178	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ 0))
309		fconstmpt 5693	. . . . . . . . . . . . 13 ⊢ (ℂ × {0}) = (𝑧 ∈ ℂ ↦ 0)
310		ringmnd 20224	. . . . . . . . . . . . . . 15 ⊢ (ℂfld ∈ Ring → ℂfld ∈ Mnd)
311	9, 310	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ℂfld ∈ Mnd
312	3, 17	pws0g 18741	. . . . . . . . . . . . . 14 ⊢ ((ℂfld ∈ Mnd ∧ ℂ ∈ V) → (ℂ × {0}) = (0g‘(ℂfld ↑s ℂ)))
313	311, 6, 312	mp2an 693	. . . . . . . . . . . . 13 ⊢ (ℂ × {0}) = (0g‘(ℂfld ↑s ℂ))
314	309, 313	eqtr3i 2761	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℂ ↦ 0) = (0g‘(ℂfld ↑s ℂ))
315	308, 314	eqtrdi 2787	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) = (0g‘(ℂfld ↑s ℂ)))
316	315, 166	suppss2 8150	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) supp (0g‘(ℂfld ↑s ℂ))) ⊆ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
317		suppssfifsupp 9293	. . . . . . . . . 10 ⊢ ((((𝑘 ∈ ℕ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 837	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) finSupp (0g‘(ℂfld ↑s ℂ)))
319	3, 4, 5, 241, 166, 242, 246, 318	pwsgsum 19957	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))))
320		fz0ssnn0 13576	. . . . . . . . . . . 12 ⊢ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ⊆ ℕ0
321		resmpt 6002	. . . . . . . . . . . 12 ⊢ ((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 5	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))) = (𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))
323	322	oveq2i 7378	. . . . . . . . . 10 ⊢ (ℂfld Σg ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) = (ℂfld Σg (𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
324	9, 10	mp1i 13	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ℂfld ∈ CMnd)
325	165	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ℕ0 ∈ V)
326	245	fmpttd 7067	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))):ℕ0⟶ℂ)
327	306, 325	suppss2 8150	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) supp 0) ⊆ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
328	165	mptex 7178	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V
329		funmpt 6536	. . . . . . . . . . . . . 14 ⊢ Fun (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))
330	328, 329, 209	3pm3.2i 1341	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∧ 0 ∈ V)
331	330	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∧ 0 ∈ V))
332		fzfid 13935	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ∈ Fin)
333		suppssfifsupp 9293	. . . . . . . . . . . 12 ⊢ ((((𝑘 ∈ ℕ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 837	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) finSupp 0)
335	4, 17, 324, 325, 326, 327, 334	gsumres 19888	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) = (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))
336		elfznn0 13574	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) → 𝑘 ∈ ℕ0)
337	336, 245	sylan2 594	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
338	332, 337	gsumfsum 21414	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (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 2795	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))
340	339	mpteq2dva 5178	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
341	240, 319, 340	3eqtrd 2775	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
342	12	adantr 480	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑆 ⊆ ℂ)
343		elplyr 26166	. . . . . . . 8 ⊢ ((𝑆 ⊆ ℂ ∧ 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 1374	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆))
345	341, 344	eqeltrd 2836	. . . . . 6 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) ∈ (Poly‘𝑆))
346		eleq1 2824	. . . . . 6 ⊢ ((𝐸‘𝑎) = 𝑓 → ((𝐸‘𝑎) ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (Poly‘𝑆)))
347	345, 346	syl5ibcom 245	. . . . 5 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝐸‘𝑎) = 𝑓 → 𝑓 ∈ (Poly‘𝑆)))
348	347	rexlimdva 3138	. . . 4 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓 → 𝑓 ∈ (Poly‘𝑆)))
349	151, 348	syl5 34	. . 3 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (𝐸 “ 𝐴) → 𝑓 ∈ (Poly‘𝑆)))
350	147, 349	impbid 212	. 2 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (𝐸 “ 𝐴)))
351	350	eqrdv 2734	1 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (Poly‘𝑆) = (𝐸 “ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2932  ∃wrex 3061  Vcvv 3429   ∖ cdif 3886   ∪ cun 3887   ⊆ wss 3889  ifcif 4466  {csn 4567   class class class wbr 5085   ↦ cmpt 5166   × cxp 5629   ↾ cres 5633   “ cima 5634   ∘ ccom 5635  Fun wfun 6492   Fn wfn 6493  ⟶wf 6494  ‘cfv 6498  (class class class)co 7367   ∘_f cof 7629   supp csupp 8110   ↑_m cmap 8773  Fincfn 8893   finSupp cfsupp 9274  ℂcc 11036  0cc0 11038   · cmul 11043  -∞cmnf 11177  ℝ^*cxr 11178   < clt 11179   ≤ cle 11180  ℕ₀cn0 12437  ...cfz 13461  ↑cexp 14023  Σcsu 15648  Basecbs 17179   ↾_s cress 17200  ._rcmulr 17221  Scalarcsca 17223   ·_𝑠 cvsca 17224  0_gc0g 17402   Σ_g cgsu 17403   ↑_s cpws 17409  Mndcmnd 18702   MndHom cmhm 18749  SubMndcsubmnd 18750  ._gcmg 19043  SubGrpcsubg 19096   GrpHom cghm 19187  CMndccmn 19755  mulGrpcmgp 20121  Ringcrg 20214  CRingccrg 20215   RingHom crh 20449  SubRingcsubrg 20546  LModclmod 20855  ℂ_fldccnfld 21352  algSccascl 21832  var₁cv1 22139  Poly₁cpl1 22140  coe₁cco1 22141  eval₁ce1 22279  deg₁cdg1 26019  Polycply 26149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-inf2 9562  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116  ax-addf 11117  ax-mulf 11118

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-iin 4936  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-isom 6507  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-of 7631  df-ofr 7632  df-om 7818  df-1st 7942  df-2nd 7943  df-supp 8111  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-2o 8406  df-er 8643  df-map 8775  df-pm 8776  df-ixp 8846  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-fsupp 9275  df-sup 9355  df-oi 9425  df-card 9863  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808  df-nn 12175  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250  df-9 12251  df-n0 12438  df-z 12525  df-dec 12645  df-uz 12789  df-rp 12943  df-fz 13462  df-fzo 13609  df-seq 13964  df-exp 14024  df-hash 14293  df-cj 15061  df-re 15062  df-im 15063  df-sqrt 15197  df-abs 15198  df-clim 15450  df-sum 15649  df-struct 17117  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201  df-plusg 17233  df-mulr 17234  df-starv 17235  df-sca 17236  df-vsca 17237  df-ip 17238  df-tset 17239  df-ple 17240  df-ds 17242  df-unif 17243  df-hom 17244  df-cco 17245  df-0g 17404  df-gsum 17405  df-prds 17410  df-pws 17412  df-mre 17548  df-mrc 17549  df-acs 17551  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-mhm 18751  df-submnd 18752  df-grp 18912  df-minusg 18913  df-sbg 18914  df-mulg 19044  df-subg 19099  df-ghm 19188  df-cntz 19292  df-cmn 19757  df-abl 19758  df-mgp 20122  df-rng 20134  df-ur 20163  df-srg 20168  df-ring 20216  df-cring 20217  df-rhm 20452  df-subrng 20523  df-subrg 20547  df-lmod 20857  df-lss 20927  df-lsp 20967  df-cnfld 21353  df-assa 21833  df-asp 21834  df-ascl 21835  df-psr 21889  df-mvr 21890  df-mpl 21891  df-opsr 21893  df-evls 22052  df-evl 22053  df-psr1 22143  df-vr1 22144  df-ply1 22145  df-coe1 22146  df-evl1 22281  df-mdeg 26020  df-deg1 26021  df-ply 26153

This theorem is referenced by: (None)