Theorem plypf1 26531

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 26513	. . . . 5 ⊢ (𝑓 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))
2	1	simprbi 503	. . . 4 ⊢ (𝑓 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
3		eqid 2761	. . . . . . . . 9 ⊢ (ℂfld ↑s ℂ) = (ℂfld ↑s ℂ)
4		cnfldbas 21682	. . . . . . . . 9 ⊢ ℂ = (Base‘ℂfld)
5		eqid 2761	. . . . . . . . 9 ⊢ (0g‘(ℂfld ↑s ℂ)) = (0g‘(ℂfld ↑s ℂ))
6		cnex 11281	. . . . . . . . . 10 ⊢ ℂ ∈ V
7	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ℂ ∈ V)
8		fzfid 14116	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (0...𝑛) ∈ Fin)
9		cnring 21700	. . . . . . . . . 10 ⊢ ℂfld ∈ Ring
10		ringcmn 20511	. . . . . . . . . 10 ⊢ (ℂfld ∈ Ring → ℂfld ∈ CMnd)
11	9, 10	mp1i 14	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ℂfld ∈ CMnd)
12	4	subrgss 20824	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ⊆ ℂ)
13	12	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ⊆ ℂ)
14		elmapi 8869	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
15	14	ad2antll 742	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
16		subrgsubg 20829	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ∈ (SubGrp‘ℂfld))
17		cnfld0 21702	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 = (0g‘ℂfld)
18	17	subg0cl 19344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (SubGrp‘ℂfld) → 0 ∈ 𝑆)
19	16, 18	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 0 ∈ 𝑆)
20	19	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 0 ∈ 𝑆)
21	20	snssd 4747	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → {0} ⊆ 𝑆)
22		ssequn2 4135	. . . . . . . . . . . . . . . 16 ⊢ ({0} ⊆ 𝑆 ↔ (𝑆 ∪ {0}) = 𝑆)
23	21, 22	sylib 221	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑆 ∪ {0}) = 𝑆)
24	23	feq3d 6694	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑎:ℕ0⟶(𝑆 ∪ {0}) ↔ 𝑎:ℕ0⟶𝑆))
25	15, 24	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 𝑎:ℕ0⟶𝑆)
26		elfznn0 13754	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0)
27		ffvelcdm 7081	. . . . . . . . . . . . 13 ⊢ ((𝑎:ℕ0⟶𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑎‘𝑘) ∈ 𝑆)
28	25, 26, 27	syl2an 608	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ 𝑆)
29	13, 28	sseldd 3932	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ ℂ)
30	29	adantrl 729	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑎‘𝑘) ∈ ℂ)
31		simprl 783	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑧 ∈ ℂ)
32	26	ad2antll 742	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑘 ∈ ℕ0)
33		expcl 14222	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ)
34	31, 32, 33	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑧↑𝑘) ∈ ℂ)
35	30, 34	mulcld 11329	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → ((𝑎‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
36		eqid 2761	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))
37	6	mptex 7229	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V
38	37	a1i 11	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V)
39		fvex 6898	. . . . . . . . . . 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 9368	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp (0g‘(ℂfld ↑s ℂ)))
42	3, 4, 5, 7, 8, 11, 35, 41	pwsgsum 20196	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))))
43		fzfid 14116	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑧 ∈ ℂ) → (0...𝑛) ∈ Fin)
44	35	anassrs 473	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑛)) → ((𝑎‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
45	43, 44	gsumfsum 21740	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
46	45	mpteq2dva 5198	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
47	42, 46	eqtrd 2796	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
48	3	pwsring 20553	. . . . . . . . . 10 ⊢ ((ℂfld ∈ Ring ∧ ℂ ∈ V) → (ℂfld ↑s ℂ) ∈ Ring)
49	9, 6, 48	mp2an 705	. . . . . . . . 9 ⊢ (ℂfld ↑s ℂ) ∈ Ring
50		ringcmn 20511	. . . . . . . . 9 ⊢ ((ℂfld ↑s ℂ) ∈ Ring → (ℂfld ↑s ℂ) ∈ CMnd)
51	49, 50	mp1i 14	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (ℂfld ↑s ℂ) ∈ CMnd)
52		cncrng 21699	. . . . . . . . . . 11 ⊢ ℂfld ∈ CRing
53		plypf1.e	. . . . . . . . . . . 12 ⊢ 𝐸 = (eval1‘ℂfld)
54		eqid 2761	. . . . . . . . . . . 12 ⊢ (Poly1‘ℂfld) = (Poly1‘ℂfld)
55	53, 54, 3, 4	evl1rhm 22650	. . . . . . . . . . 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 22550	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
61	60	adantr 486	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
62		rhmima 20856	. . . . . . . . . 10 ⊢ ((𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂfld ↑s ℂ)) ∧ 𝐴 ∈ (SubRing‘(Poly1‘ℂfld))) → (𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)))
63	56, 61, 62	sylancr 599	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)))
64		subrgsubg 20829	. . . . . . . . 9 ⊢ ((𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)) → (𝐸 “ 𝐴) ∈ (SubGrp‘(ℂfld ↑s ℂ)))
65		subgsubm 19359	. . . . . . . . 9 ⊢ ((𝐸 “ 𝐴) ∈ (SubGrp‘(ℂfld ↑s ℂ)) → (𝐸 “ 𝐴) ∈ (SubMnd‘(ℂfld ↑s ℂ)))
66	63, 64, 65	3syl 19	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝐸 “ 𝐴) ∈ (SubMnd‘(ℂfld ↑s ℂ)))
67		eqid 2761	. . . . . . . . . . . 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 6771	. . . . . . . . . . . . . 14 ⊢ ((𝑎‘𝑘) ∈ ℂ → (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)
71	29, 70	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)
72	3, 4, 67	pwselbasb 17659	. . . . . . . . . . . . . 14 ⊢ ((ℂfld ∈ Ring ∧ ℂ ∈ V) → ((ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ))
73	9, 6, 72	mp2an 705	. . . . . . . . . . . . 13 ⊢ ((ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)
74	71, 73	sylibr 237	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld ↑s ℂ)))
75	34	anass1rs 668	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑧↑𝑘) ∈ ℂ)
76	75	fmpttd 7115	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ)
77	3, 4, 67	pwselbasb 17659	. . . . . . . . . . . . . 14 ⊢ ((ℂfld ∈ Ring ∧ ℂ ∈ V) → ((𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ))
78	9, 6, 77	mp2an 705	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ)
79	76, 78	sylibr 237	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld ↑s ℂ)))
80		cnfldmul 21686	. . . . . . . . . . . 12 ⊢ · = (.r‘ℂfld)
81		eqid 2761	. . . . . . . . . . . 12 ⊢ (.r‘(ℂfld ↑s ℂ)) = (.r‘(ℂfld ↑s ℂ))
82	3, 67, 68, 69, 74, 79, 80, 81	pwsmulrval 17663	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = ((ℂ × {(𝑎‘𝑘)}) ∘f · (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))))
83	29	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑎‘𝑘) ∈ ℂ)
84		fconstmpt 5713	. . . . . . . . . . . . 13 ⊢ (ℂ × {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘))
85	84	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘)))
86		eqidd 2762	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))
87	69, 83, 75, 85, 86	offval2 7713	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)}) ∘f · (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))
88	82, 87	eqtrd 2796	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))
89	63	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)))
90		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (algSc‘(Poly1‘ℂfld)) = (algSc‘(Poly1‘ℂfld))
91	53, 54, 4, 90	evl1sca 22652	. . . . . . . . . . . . 13 ⊢ ((ℂfld ∈ CRing ∧ (𝑎‘𝑘) ∈ ℂ) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) = (ℂ × {(𝑎‘𝑘)}))
92	52, 29, 91	sylancr 599	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) = (ℂ × {(𝑎‘𝑘)}))
93		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Poly1‘ℂfld)) = (Base‘(Poly1‘ℂfld))
94	93, 67	rhmf 20715	. . . . . . . . . . . . . . 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 6709	. . . . . . . . . . . . . 14 ⊢ (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld ↑s ℂ)) → 𝐸 Fn (Base‘(Poly1‘ℂfld)))
97	95, 96	mp1i 14	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐸 Fn (Base‘(Poly1‘ℂfld)))
98	93	subrgss 20824	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (SubRing‘(Poly1‘ℂfld)) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
99	60, 98	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
100	99	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
101		simpll 779	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ∈ (SubRing‘ℂfld))
102	54, 90, 57, 58, 101, 59, 4, 29	subrg1asclcl 22579	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴 ↔ (𝑎‘𝑘) ∈ 𝑆))
103	28, 102	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴)
104		fnfvima 7239	. . . . . . . . . . . . 13 ⊢ ((𝐸 Fn (Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆ (Base‘(Poly1‘ℂfld)) ∧ ((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) ∈ (𝐸 “ 𝐴))
105	97, 100, 103, 104	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) ∈ (𝐸 “ 𝐴))
106	92, 105	eqeltrrd 2862	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴))
107	67	subrgss 20824	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)) → (𝐸 “ 𝐴) ⊆ (Base‘(ℂfld ↑s ℂ)))
108	89, 107	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸 “ 𝐴) ⊆ (Base‘(ℂfld ↑s ℂ)))
109	60	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
110		eqid 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (mulGrp‘(Poly1‘ℂfld)) = (mulGrp‘(Poly1‘ℂfld))
111	110	subrgsubm 20837	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ (SubRing‘(Poly1‘ℂfld)) → 𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))))
112	109, 111	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))))
113	26	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑘 ∈ ℕ0)
114		eqid 2761	. . . . . . . . . . . . . . . . . . 19 ⊢ (var1‘ℂfld) = (var1‘ℂfld)
115	114, 101, 57, 58, 59	subrgvr1cl 22581	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (var1‘ℂfld) ∈ 𝐴)
116		eqid 2761	. . . . . . . . . . . . . . . . . . 19 ⊢ (.g‘(mulGrp‘(Poly1‘ℂfld))) = (.g‘(mulGrp‘(Poly1‘ℂfld)))
117	116	submmulgcl 19327	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))) ∧ 𝑘 ∈ ℕ0 ∧ (var1‘ℂfld) ∈ 𝐴) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
118	112, 113, 115, 117	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
119		fnfvima 7239	. . . . . . . . . . . . . . . . 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 1398	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (𝐸 “ 𝐴))
121	108, 120	sseldd 3932	. . . . . . . . . . . . . . 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 17660	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))):ℂ⟶ℂ)
123	122	feqmptd 6953	. . . . . . . . . . . . 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 490	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
126	53, 114, 4, 54, 93, 124, 125	evl1vard 22655	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧))
127		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
128	113	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0)
129	53, 54, 4, 93, 124, 125, 126, 116, 127, 128	evl1expd 22663	. . . . . . . . . . . . . . . 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 501	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧))
131		cnfldexp 21711	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘))
132	125, 128, 131	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘))
133	130, 132	eqtrd 2796	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘))
134	133	mpteq2dva 5198	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))
135	123, 134	eqtrd 2796	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))
136	135, 120	eqeltrrd 2862	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴))
137	81	subrgmcl 20836	. . . . . . . . . . 11 ⊢ (((𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)) ∧ (ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴) ∧ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
138	89, 106, 136, 137	syl3anc 1398	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
139	88, 138	eqeltrrd 2862	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
140	139	fmpttd 7115	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))):(0...𝑛)⟶(𝐸 “ 𝐴))
141	36, 8, 139, 40	fsuppmptdm 9368	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp (0g‘(ℂfld ↑s ℂ)))
142	5, 51, 8, 66, 140, 141	gsumsubmcl 20133	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) ∈ (𝐸 “ 𝐴))
143	47, 142	eqeltrrd 2862	. . . . . 6 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
144		eleq1 2849	. . . . . 6 ⊢ (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → (𝑓 ∈ (𝐸 “ 𝐴) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)))
145	143, 144	syl5ibrcom 250	. . . . 5 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴)))
146	145	rexlimdvva 3220	. . . 4 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴)))
147	2, 146	syl5 35	. . 3 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) → 𝑓 ∈ (𝐸 “ 𝐴)))
148		ffun 6712	. . . . . 6 ⊢ (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld ↑s ℂ)) → Fun 𝐸)
149	95, 148	ax-mp 5	. . . . 5 ⊢ Fun 𝐸
150		fvelima 6950	. . . . 5 ⊢ ((Fun 𝐸 ∧ 𝑓 ∈ (𝐸 “ 𝐴)) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓)
151	149, 150	mpan 703	. . . 4 ⊢ (𝑓 ∈ (𝐸 “ 𝐴) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓)
152	99	sselda 3931	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ (Base‘(Poly1‘ℂfld)))
153		eqid 2761	. . . . . . . . . . . 12 ⊢ ( ·𝑠 ‘(Poly1‘ℂfld)) = ( ·𝑠 ‘(Poly1‘ℂfld))
154		eqid 2761	. . . . . . . . . . . 12 ⊢ (coe1‘𝑎) = (coe1‘𝑎)
155	54, 114, 93, 153, 110, 116, 154	ply1coe 22616	. . . . . . . . . . 11 ⊢ ((ℂfld ∈ Ring ∧ 𝑎 ∈ (Base‘(Poly1‘ℂfld))) → 𝑎 = ((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
156	9, 152, 155	sylancr 599	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑎 = ((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
157	156	fveq2d 6889	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝐸‘((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))))
158		eqid 2761	. . . . . . . . . 10 ⊢ (0g‘(Poly1‘ℂfld)) = (0g‘(Poly1‘ℂfld))
159	54	ply1ring 22565	. . . . . . . . . . . 12 ⊢ (ℂfld ∈ Ring → (Poly1‘ℂfld) ∈ Ring)
160	9, 159	ax-mp 5	. . . . . . . . . . 11 ⊢ (Poly1‘ℂfld) ∈ Ring
161		ringcmn 20511	. . . . . . . . . . 11 ⊢ ((Poly1‘ℂfld) ∈ Ring → (Poly1‘ℂfld) ∈ CMnd)
162	160, 161	mp1i 14	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (Poly1‘ℂfld) ∈ CMnd)
163		ringmnd 20470	. . . . . . . . . . 11 ⊢ ((ℂfld ↑s ℂ) ∈ Ring → (ℂfld ↑s ℂ) ∈ Mnd)
164	49, 163	mp1i 14	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (ℂfld ↑s ℂ) ∈ Mnd)
165		nn0ex 12612	. . . . . . . . . . 11 ⊢ ℕ0 ∈ V
166	165	a1i 11	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℕ0 ∈ V)
167		rhmghm 20714	. . . . . . . . . . . 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 19440	. . . . . . . . . . 11 ⊢ (𝐸 ∈ ((Poly1‘ℂfld) GrpHom (ℂfld ↑s ℂ)) → 𝐸 ∈ ((Poly1‘ℂfld) MndHom (ℂfld ↑s ℂ)))
170	168, 169	mp1i 14	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝐸 ∈ ((Poly1‘ℂfld) MndHom (ℂfld ↑s ℂ)))
171	54	ply1lmod 22569	. . . . . . . . . . . . 13 ⊢ (ℂfld ∈ Ring → (Poly1‘ℂfld) ∈ LMod)
172	9, 171	mp1i 14	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (Poly1‘ℂfld) ∈ LMod)
173	12	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑆 ⊆ ℂ)
174		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝑅) = (Base‘𝑅)
175	154, 59, 58, 174	coe1f 22529	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ 𝐴 → (coe1‘𝑎):ℕ0⟶(Base‘𝑅))
176	57	subrgbas 20833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 = (Base‘𝑅))
177	176	feq3d 6694	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → ((coe1‘𝑎):ℕ0⟶𝑆 ↔ (coe1‘𝑎):ℕ0⟶(Base‘𝑅)))
178	175, 177	imbitrrid 249	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (𝑎 ∈ 𝐴 → (coe1‘𝑎):ℕ0⟶𝑆))
179	178	imp 412	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎):ℕ0⟶𝑆)
180	179	ffvelcdmda 7084	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝑎)‘𝑘) ∈ 𝑆)
181	173, 180	sseldd 3932	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝑎)‘𝑘) ∈ ℂ)
182	110, 93	mgpbas 20365	. . . . . . . . . . . . 13 ⊢ (Base‘(Poly1‘ℂfld)) = (Base‘(mulGrp‘(Poly1‘ℂfld)))
183	110	ringmgp 20465	. . . . . . . . . . . . . 14 ⊢ ((Poly1‘ℂfld) ∈ Ring → (mulGrp‘(Poly1‘ℂfld)) ∈ Mnd)
184	160, 183	mp1i 14	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (mulGrp‘(Poly1‘ℂfld)) ∈ Mnd)
185		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
186	114, 54, 93	vr1cl 22535	. . . . . . . . . . . . . 14 ⊢ (ℂfld ∈ Ring → (var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)))
187	9, 186	mp1i 14	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)))
188	182, 116, 184, 185, 187	mulgnn0cld 19305	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)))
189	54	ply1sca 22570	. . . . . . . . . . . . . 14 ⊢ (ℂfld ∈ Ring → ℂfld = (Scalar‘(Poly1‘ℂfld)))
190	9, 189	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ℂfld = (Scalar‘(Poly1‘ℂfld))
191	93, 190, 153, 4	lmodvscl 21153	. . . . . . . . . . . 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 1398	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(Poly1‘ℂfld)))
193	192	fmpttd 7115	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℕ0⟶(Base‘(Poly1‘ℂfld)))
194	165	mptex 7229	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ V
195		funmpt 6578	. . . . . . . . . . . . 13 ⊢ Fun (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
196		fvex 6898	. . . . . . . . . . . . 13 ⊢ (0g‘(Poly1‘ℂfld)) ∈ V
197	194, 195, 196	3pm3.2i 1358	. . . . . . . . . . . 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 22531	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → (coe1‘𝑎) finSupp 0)
200	152, 199	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) finSupp 0)
201	200	fsuppimpd 9361	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) ∈ Fin)
202	179	feqmptd 6953	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) = (𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)))
203	202	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)) supp 0))
204		eqimss2 3990	. . . . . . . . . . . . 13 ⊢ (((coe1‘𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)) supp 0) → ((𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)) supp 0) ⊆ ((coe1‘𝑎) supp 0))
205	203, 204	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)) supp 0) ⊆ ((coe1‘𝑎) supp 0))
206	9, 171	mp1i 14	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (Poly1‘ℂfld) ∈ LMod)
207	93, 190, 153, 17, 158	lmod0vs 21170	. . . . . . . . . . . . 13 ⊢ (((Poly1‘ℂfld) ∈ LMod ∧ 𝑥 ∈ (Base‘(Poly1‘ℂfld))) → (0( ·𝑠 ‘(Poly1‘ℂfld))𝑥) = (0g‘(Poly1‘ℂfld)))
208	206, 207	sylan 592	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (Base‘(Poly1‘ℂfld))) → (0( ·𝑠 ‘(Poly1‘ℂfld))𝑥) = (0g‘(Poly1‘ℂfld)))
209		c0ex 11300	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
210	209	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 0 ∈ V)
211	205, 208, 180, 188, 210	suppssov1 8214	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) supp (0g‘(Poly1‘ℂfld))) ⊆ ((coe1‘𝑎) supp 0))
212		suppssfifsupp 9372	. . . . . . . . . . 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 850	. . . . . . . . . 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 20152	. . . . . . . . 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 7133	. . . . . . . . . . 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 7083	. . . . . . . . . . . . . . . 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 18	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ (Base‘(ℂfld ↑s ℂ)))
221	3, 4, 67, 217, 218, 220	pwselbas 17660	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℂ⟶ℂ)
222	221	feqmptd 6953	. . . . . . . . . . . . 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 490	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
225	53, 114, 4, 54, 93, 223, 224	evl1vard 22655	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧))
226	185	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0)
227	53, 54, 4, 93, 223, 224, 225, 116, 127, 226	evl1expd 22663	. . . . . . . . . . . . . . . . 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 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘))
229	228	eqeq2d 2772	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧) ↔ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘)))
230	229	anbi2d 642	. . . . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘)))
232	181	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((coe1‘𝑎)‘𝑘) ∈ ℂ)
233	53, 54, 4, 93, 223, 224, 231, 232, 153, 80	evl1vsd 22662	. . . . . . . . . . . . . . 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 501	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧) = (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))
235	234	mpteq2dva 5198	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧)) = (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
236	222, 235	eqtrd 2796	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) = (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
237	236	mpteq2dva 5198	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))
238	216, 237	eqtrd 2796	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))
239	238	oveq2d 7436	. . . . . . . . 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 2802	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = ((ℂfld ↑s ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))))
241	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℂ ∈ V)
242	9, 10	mp1i 14	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℂfld ∈ CMnd)
243	181	adantlr 728	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝑎)‘𝑘) ∈ ℂ)
244	33	adantll 727	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ)
245	243, 244	mulcld 11329	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
246	245	anasss 472	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
247	165	mptex 7229	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V
248		funmpt 6578	. . . . . . . . . . . 12 ⊢ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
249	247, 248, 39	3pm3.2i 1358	. . . . . . . . . . 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 14116	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ∈ Fin)
252		eldifn 4079	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))) → ¬ 𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
253	252	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → ¬ 𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
254	152	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑎 ∈ (Base‘(Poly1‘ℂfld)))
255		eldifi 4078	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))) → 𝑘 ∈ ℕ0)
256	255	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℕ0)
257		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (deg1‘ℂfld) = (deg1‘ℂfld)
258	257, 54, 93, 17, 154	deg1ge 26416	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ (Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0 ∧ ((coe1‘𝑎)‘𝑘) ≠ 0) → 𝑘 ≤ ((deg1‘ℂfld)‘𝑎))
259	258	3expia 1139	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ (Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0) → (((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ ((deg1‘ℂfld)‘𝑎)))
260	254, 256, 259	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ ((deg1‘ℂfld)‘𝑎)))
261		0xr 11356	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ*
262	257, 54, 93	deg1xrcl 26400	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → ((deg1‘ℂfld)‘𝑎) ∈ ℝ*)
263	152, 262	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((deg1‘ℂfld)‘𝑎) ∈ ℝ*)
264	263	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → ((deg1‘ℂfld)‘𝑎) ∈ ℝ*)
265		xrmax2 13306	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0 ∈ ℝ* ∧ ((deg1‘ℂfld)‘𝑎) ∈ ℝ*) → ((deg1‘ℂfld)‘𝑎) ≤ if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))
266	261, 264, 265	sylancr 599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → ((deg1‘ℂfld)‘𝑎) ≤ if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))
267	256	nn0red 12668	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ)
268	267	rexrd 11359	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ*)
269		ifcl 4528	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((deg1‘ℂfld)‘𝑎) ∈ ℝ* ∧ 0 ∈ ℝ*) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℝ*)
270	264, 261, 269	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℝ*)
271		xrletr 13287	. . . . . . . . . . . . . . . . . . . . . . 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 1398	. . . . . . . . . . . . . . . . . . . . . 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 707	. . . . . . . . . . . . . . . . . . . . 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 48	. . . . . . . . . . . . . . . . . . . 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 535	. . . . . . . . . . . . . . . . . . 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 26401	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → ((deg1‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
277	152, 276	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((deg1‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
278		elun 4100	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}) ↔ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((deg1‘ℂfld)‘𝑎) ∈ {-∞}))
279	277, 278	sylib 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((deg1‘ℂfld)‘𝑎) ∈ {-∞}))
280		nn0ge0 12631	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → 0 ≤ ((deg1‘ℂfld)‘𝑎))
281	280	iftrued 4490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) = ((deg1‘ℂfld)‘𝑎))
282		id 23	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → ((deg1‘ℂfld)‘𝑎) ∈ ℕ0)
283	281, 282	eqeltrd 2861	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
284		mnflt0 13254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ -∞ < 0
285		mnfxr 11366	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ -∞ ∈ ℝ*
286		xrltnle 11376	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*) → (-∞ < 0 ↔ ¬ 0 ≤ -∞))
287	285, 261, 286	mp2an 705	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (-∞ < 0 ↔ ¬ 0 ≤ -∞)
288	284, 287	mpbi 233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ¬ 0 ≤ -∞
289		elsni 4601	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → ((deg1‘ℂfld)‘𝑎) = -∞)
290	289	breq2d 5115	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → (0 ≤ ((deg1‘ℂfld)‘𝑎) ↔ 0 ≤ -∞))
291	288, 290	mtbiri 330	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → ¬ 0 ≤ ((deg1‘ℂfld)‘𝑎))
292	291	iffalsed 4493	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) = 0)
293		0nn0 12621	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ ℕ0
294	292, 293	eqeltrdi 2869	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
295	283, 294	jaoi 871	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((deg1‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((deg1‘ℂfld)‘𝑎) ∈ {-∞}) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
296	279, 295	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
297	296	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
298		fznn0 13753	. . . . . . . . . . . . . . . . . . . 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 18	. . . . . . . . . . . . . . . . . . 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 262	. . . . . . . . . . . . . . . . . 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 2974	. . . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → ((coe1‘𝑎)‘𝑘) = 0)
303	302	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘)))
304	255, 244	sylan2 605	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑧↑𝑘) ∈ ℂ)
305	304	mul02d 11508	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (0 · (𝑧↑𝑘)) = 0)
306	303, 305	eqtrd 2796	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = 0)
307	306	an32s 665	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) ∧ 𝑧 ∈ ℂ) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = 0)
308	307	mpteq2dva 5198	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ 0))
309		fconstmpt 5713	. . . . . . . . . . . . 13 ⊢ (ℂ × {0}) = (𝑧 ∈ ℂ ↦ 0)
310		ringmnd 20470	. . . . . . . . . . . . . . 15 ⊢ (ℂfld ∈ Ring → ℂfld ∈ Mnd)
311	9, 310	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ℂfld ∈ Mnd
312	3, 17	pws0g 18967	. . . . . . . . . . . . . 14 ⊢ ((ℂfld ∈ Mnd ∧ ℂ ∈ V) → (ℂ × {0}) = (0g‘(ℂfld ↑s ℂ)))
313	311, 6, 312	mp2an 705	. . . . . . . . . . . . 13 ⊢ (ℂ × {0}) = (0g‘(ℂfld ↑s ℂ))
314	309, 313	eqtr3i 2786	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℂ ↦ 0) = (0g‘(ℂfld ↑s ℂ))
315	308, 314	eqtrdi 2812	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) = (0g‘(ℂfld ↑s ℂ)))
316	315, 166	suppss2 8217	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) supp (0g‘(ℂfld ↑s ℂ))) ⊆ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
317		suppssfifsupp 9372	. . . . . . . . . 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 850	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) finSupp (0g‘(ℂfld ↑s ℂ)))
319	3, 4, 5, 241, 166, 242, 246, 318	pwsgsum 20196	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))))
320		fz0ssnn0 13756	. . . . . . . . . . . 12 ⊢ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ⊆ ℕ0
321		resmpt 6029	. . . . . . . . . . . 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 7431	. . . . . . . . . 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 14	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ℂfld ∈ CMnd)
325	165	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ℕ0 ∈ V)
326	245	fmpttd 7115	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))):ℕ0⟶ℂ)
327	306, 325	suppss2 8217	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) supp 0) ⊆ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
328	165	mptex 7229	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V
329		funmpt 6578	. . . . . . . . . . . . . 14 ⊢ Fun (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))
330	328, 329, 209	3pm3.2i 1358	. . . . . . . . . . . . 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 14116	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ∈ Fin)
333		suppssfifsupp 9372	. . . . . . . . . . . 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 850	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) finSupp 0)
335	4, 17, 324, 325, 326, 327, 334	gsumres 20127	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) = (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))
336		elfznn0 13754	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) → 𝑘 ∈ ℕ0)
337	336, 245	sylan2 605	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
338	332, 337	gsumfsum 21740	. . . . . . . . . 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 2820	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))
340	339	mpteq2dva 5198	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
341	240, 319, 340	3eqtrd 2800	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
342	12	adantr 486	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑆 ⊆ ℂ)
343		elplyr 26519	. . . . . . . 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 1398	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆))
345	341, 344	eqeltrd 2861	. . . . . 6 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) ∈ (Poly‘𝑆))
346		eleq1 2849	. . . . . 6 ⊢ ((𝐸‘𝑎) = 𝑓 → ((𝐸‘𝑎) ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (Poly‘𝑆)))
347	345, 346	syl5ibcom 248	. . . . 5 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝐸‘𝑎) = 𝑓 → 𝑓 ∈ (Poly‘𝑆)))
348	347	rexlimdva 3164	. . . 4 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓 → 𝑓 ∈ (Poly‘𝑆)))
349	151, 348	syl5 35	. . 3 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (𝐸 “ 𝐴) → 𝑓 ∈ (Poly‘𝑆)))
350	147, 349	impbid 215	. 2 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (𝐸 “ 𝐴)))
351	350	eqrdv 2759	1 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (Poly‘𝑆) = (𝐸 “ 𝐴))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∃wrex 3087  Vcvv 3451   ∖ cdif 3896   ∪ cun 3897   ⊆ wss 3899  ifcif 4482  {csn 4584   class class class wbr 5103   ↦ cmpt 5186   × cxp 5649   ↾ cres 5653   “ cima 5654   ∘ ccom 5655  Fun wfun 6532   Fn wfn 6533  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420   ∘_f cof 7691   supp csupp 8177   ↑_m cmap 8847  Fincfn 8973   finSupp cfsupp 9353  ℂcc 11198  0cc0 11200   · cmul 11205  -∞cmnf 11341  ℝ^*cxr 11342   < clt 11343   ≤ cle 11344  ℕ₀cn0 12606  ...cfz 13639  ↑cexp 14204  Σcsu 15853  Basecbs 17387   ↾_s cress 17408  ._rcmulr 17429  Scalarcsca 17431   ·_𝑠 cvsca 17432  0_gc0g 17610   Σ_g cgsu 17611   ↑_s cpws 17617  Mndcmnd 18923   MndHom cmhm 18976  SubMndcsubmnd 18977  ._gcmg 19277  SubGrpcsubg 19330   GrpHom cghm 19427  CMndccmn 19994  mulGrpcmgp 20360  Ringcrg 20459  CRingccrg 20460   RingHom crh 20699  SubRingcsubrg 20821  LModclmod 21135  ℂ_fldccnfld 21678  algSccascl 22160  var₁cv1 22494  Poly₁cpl1 22495  coe₁cco1 22496  eval₁ce1 22632  deg₁cdg1 26372  Polycply 26502

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-inf2 9642  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277  ax-pre-sup 11278  ax-addf 11279  ax-mulf 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7693  df-ofr 7694  df-om 7878  df-1st 8001  df-2nd 8002  df-supp 8178  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-1o 8476  df-2o 8477  df-er 8717  df-map 8849  df-pm 8850  df-ixp 8926  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-fsupp 9354  df-sup 9434  df-oi 9504  df-card 10020  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-div 11974  df-nn 12336  df-2 12405  df-3 12406  df-4 12407  df-5 12408  df-6 12409  df-7 12410  df-8 12411  df-9 12412  df-n0 12607  df-z 12694  df-dec 12815  df-uz 12966  df-rp 13121  df-fz 13640  df-fzo 13789  df-seq 14145  df-exp 14205  df-hash 14475  df-cj 15266  df-re 15267  df-im 15268  df-sqrt 15402  df-abs 15403  df-clim 15655  df-sum 15854  df-struct 17325  df-sets 17342  df-slot 17360  df-ndx 17372  df-base 17388  df-ress 17409  df-plusg 17441  df-mulr 17442  df-starv 17443  df-sca 17444  df-vsca 17445  df-ip 17446  df-tset 17447  df-ple 17448  df-ds 17450  df-unif 17451  df-hom 17452  df-cco 17453  df-0g 17612  df-gsum 17613  df-prds 17618  df-pws 17620  df-mre 17756  df-mrc 17757  df-acs 17759  df-mgm 18816  df-sgrp 18908  df-mnd 18924  df-mhm 18978  df-submnd 18979  df-grp 19147  df-minusg 19148  df-sbg 19149  df-mulg 19278  df-subg 19333  df-ghm 19428  df-cntz 19531  df-cmn 19996  df-abl 19997  df-mgp 20361  df-rng 20375  df-ur 20408  df-srg 20413  df-ring 20461  df-cring 20462  df-rhm 20702  df-subrng 20798  df-subrg 20822  df-lmod 21137  df-lss 21207  df-lsp 21247  df-cnfld 21679  df-assa 22161  df-asp 22162  df-ascl 22163  df-psr 22217  df-mvr 22218  df-mpl 22219  df-opsr 22221  df-evls 22383  df-evl 22384  df-psr1 22498  df-vr1 22499  df-ply1 22500  df-coe1 22501  df-evl1 22634  df-mdeg 26373  df-deg1 26374  df-ply 26506

This theorem is used by: (None)