Theorem plypf1 26265

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 26248	. . . . 5 ⊢ (𝑓 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))
2	1	simprbi 496	. . . 4 ⊢ (𝑓 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
3		eqid 2734	. . . . . . . . 9 ⊢ (ℂfld ↑s ℂ) = (ℂfld ↑s ℂ)
4		cnfldbas 21385	. . . . . . . . 9 ⊢ ℂ = (Base‘ℂfld)
5		eqid 2734	. . . . . . . . 9 ⊢ (0g‘(ℂfld ↑s ℂ)) = (0g‘(ℂfld ↑s ℂ))
6		cnex 11233	. . . . . . . . . 10 ⊢ ℂ ∈ V
7	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ℂ ∈ V)
8		fzfid 14010	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (0...𝑛) ∈ Fin)
9		cnring 21420	. . . . . . . . . 10 ⊢ ℂfld ∈ Ring
10		ringcmn 20295	. . . . . . . . . 10 ⊢ (ℂfld ∈ Ring → ℂfld ∈ CMnd)
11	9, 10	mp1i 13	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ℂfld ∈ CMnd)
12	4	subrgss 20588	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ⊆ ℂ)
13	12	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ⊆ ℂ)
14		elmapi 8887	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
15	14	ad2antll 729	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
16		subrgsubg 20593	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ∈ (SubGrp‘ℂfld))
17		cnfld0 21422	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 = (0g‘ℂfld)
18	17	subg0cl 19164	. . . . . . . . . . . . . . . . . . 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 4813	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → {0} ⊆ 𝑆)
22		ssequn2 4198	. . . . . . . . . . . . . . . 16 ⊢ ({0} ⊆ 𝑆 ↔ (𝑆 ∪ {0}) = 𝑆)
23	21, 22	sylib 218	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑆 ∪ {0}) = 𝑆)
24	23	feq3d 6723	. . . . . . . . . . . . . 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 13656	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0)
27		ffvelcdm 7100	. . . . . . . . . . . . 13 ⊢ ((𝑎:ℕ0⟶𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑎‘𝑘) ∈ 𝑆)
28	25, 26, 27	syl2an 596	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ 𝑆)
29	13, 28	sseldd 3995	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ ℂ)
30	29	adantrl 716	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑎‘𝑘) ∈ ℂ)
31		simprl 771	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑧 ∈ ℂ)
32	26	ad2antll 729	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑘 ∈ ℕ0)
33		expcl 14116	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ)
34	31, 32, 33	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑧↑𝑘) ∈ ℂ)
35	30, 34	mulcld 11278	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → ((𝑎‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
36		eqid 2734	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))
37	6	mptex 7242	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V
38	37	a1i 11	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V)
39		fvex 6919	. . . . . . . . . . 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 9413	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp (0g‘(ℂfld ↑s ℂ)))
42	3, 4, 5, 7, 8, 11, 35, 41	pwsgsum 20014	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))))
43		fzfid 14010	. . . . . . . . . 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 21469	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
46	45	mpteq2dva 5247	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
47	42, 46	eqtrd 2774	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
48	3	pwsring 20337	. . . . . . . . . 10 ⊢ ((ℂfld ∈ Ring ∧ ℂ ∈ V) → (ℂfld ↑s ℂ) ∈ Ring)
49	9, 6, 48	mp2an 692	. . . . . . . . 9 ⊢ (ℂfld ↑s ℂ) ∈ Ring
50		ringcmn 20295	. . . . . . . . 9 ⊢ ((ℂfld ↑s ℂ) ∈ Ring → (ℂfld ↑s ℂ) ∈ CMnd)
51	49, 50	mp1i 13	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (ℂfld ↑s ℂ) ∈ CMnd)
52		cncrng 21418	. . . . . . . . . . 11 ⊢ ℂfld ∈ CRing
53		plypf1.e	. . . . . . . . . . . 12 ⊢ 𝐸 = (eval1‘ℂfld)
54		eqid 2734	. . . . . . . . . . . 12 ⊢ (Poly1‘ℂfld) = (Poly1‘ℂfld)
55	53, 54, 3, 4	evl1rhm 22351	. . . . . . . . . . 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 22249	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
61	60	adantr 480	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
62		rhmima 20620	. . . . . . . . . 10 ⊢ ((𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂfld ↑s ℂ)) ∧ 𝐴 ∈ (SubRing‘(Poly1‘ℂfld))) → (𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)))
63	56, 61, 62	sylancr 587	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)))
64		subrgsubg 20593	. . . . . . . . 9 ⊢ ((𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)) → (𝐸 “ 𝐴) ∈ (SubGrp‘(ℂfld ↑s ℂ)))
65		subgsubm 19178	. . . . . . . . 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 2734	. . . . . . . . . . . 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 6797	. . . . . . . . . . . . . 14 ⊢ ((𝑎‘𝑘) ∈ ℂ → (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)
71	29, 70	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)
72	3, 4, 67	pwselbasb 17534	. . . . . . . . . . . . . 14 ⊢ ((ℂfld ∈ Ring ∧ ℂ ∈ V) → ((ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ))
73	9, 6, 72	mp2an 692	. . . . . . . . . . . . 13 ⊢ ((ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)
74	71, 73	sylibr 234	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld ↑s ℂ)))
75	34	anass1rs 655	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑧↑𝑘) ∈ ℂ)
76	75	fmpttd 7134	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ)
77	3, 4, 67	pwselbasb 17534	. . . . . . . . . . . . . 14 ⊢ ((ℂfld ∈ Ring ∧ ℂ ∈ V) → ((𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ))
78	9, 6, 77	mp2an 692	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ)
79	76, 78	sylibr 234	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld ↑s ℂ)))
80		cnfldmul 21389	. . . . . . . . . . . 12 ⊢ · = (.r‘ℂfld)
81		eqid 2734	. . . . . . . . . . . 12 ⊢ (.r‘(ℂfld ↑s ℂ)) = (.r‘(ℂfld ↑s ℂ))
82	3, 67, 68, 69, 74, 79, 80, 81	pwsmulrval 17537	. . . . . . . . . . 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 5750	. . . . . . . . . . . . 13 ⊢ (ℂ × {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘))
85	84	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘)))
86		eqidd 2735	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))
87	69, 83, 75, 85, 86	offval2 7716	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)}) ∘f · (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))
88	82, 87	eqtrd 2774	. . . . . . . . . 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 2734	. . . . . . . . . . . . . 14 ⊢ (algSc‘(Poly1‘ℂfld)) = (algSc‘(Poly1‘ℂfld))
91	53, 54, 4, 90	evl1sca 22353	. . . . . . . . . . . . 13 ⊢ ((ℂfld ∈ CRing ∧ (𝑎‘𝑘) ∈ ℂ) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) = (ℂ × {(𝑎‘𝑘)}))
92	52, 29, 91	sylancr 587	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) = (ℂ × {(𝑎‘𝑘)}))
93		eqid 2734	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Poly1‘ℂfld)) = (Base‘(Poly1‘ℂfld))
94	93, 67	rhmf 20501	. . . . . . . . . . . . . . 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 6736	. . . . . . . . . . . . . 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 20588	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (SubRing‘(Poly1‘ℂfld)) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
99	60, 98	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
100	99	ad2antrr 726	. . . . . . . . . . . . 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 22278	. . . . . . . . . . . . . 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 7252	. . . . . . . . . . . . 13 ⊢ ((𝐸 Fn (Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆ (Base‘(Poly1‘ℂfld)) ∧ ((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) ∈ (𝐸 “ 𝐴))
105	97, 100, 103, 104	syl3anc 1370	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) ∈ (𝐸 “ 𝐴))
106	92, 105	eqeltrrd 2839	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴))
107	67	subrgss 20588	. . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
110		eqid 2734	. . . . . . . . . . . . . . . . . . . 20 ⊢ (mulGrp‘(Poly1‘ℂfld)) = (mulGrp‘(Poly1‘ℂfld))
111	110	subrgsubm 20601	. . . . . . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . . . . . 19 ⊢ (var1‘ℂfld) = (var1‘ℂfld)
115	114, 101, 57, 58, 59	subrgvr1cl 22280	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (var1‘ℂfld) ∈ 𝐴)
116		eqid 2734	. . . . . . . . . . . . . . . . . . 19 ⊢ (.g‘(mulGrp‘(Poly1‘ℂfld))) = (.g‘(mulGrp‘(Poly1‘ℂfld)))
117	116	submmulgcl 19147	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))) ∧ 𝑘 ∈ ℕ0 ∧ (var1‘ℂfld) ∈ 𝐴) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
118	112, 113, 115, 117	syl3anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
119		fnfvima 7252	. . . . . . . . . . . . . . . . 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 1370	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (𝐸 “ 𝐴))
121	108, 120	sseldd 3995	. . . . . . . . . . . . . . 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 17535	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))):ℂ⟶ℂ)
123	122	feqmptd 6976	. . . . . . . . . . . . 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 22356	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧))
127		eqid 2734	. . . . . . . . . . . . . . . . 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 22364	. . . . . . . . . . . . . . . 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 21434	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘))
132	125, 128, 131	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘))
133	130, 132	eqtrd 2774	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘))
134	133	mpteq2dva 5247	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))
135	123, 134	eqtrd 2774	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))
136	135, 120	eqeltrrd 2839	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴))
137	81	subrgmcl 20600	. . . . . . . . . . 11 ⊢ (((𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)) ∧ (ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴) ∧ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
138	89, 106, 136, 137	syl3anc 1370	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
139	88, 138	eqeltrrd 2839	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
140	139	fmpttd 7134	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))):(0...𝑛)⟶(𝐸 “ 𝐴))
141	36, 8, 139, 40	fsuppmptdm 9413	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp (0g‘(ℂfld ↑s ℂ)))
142	5, 51, 8, 66, 140, 141	gsumsubmcl 19951	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) ∈ (𝐸 “ 𝐴))
143	47, 142	eqeltrrd 2839	. . . . . 6 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
144		eleq1 2826	. . . . . 6 ⊢ (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → (𝑓 ∈ (𝐸 “ 𝐴) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)))
145	143, 144	syl5ibrcom 247	. . . . 5 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴)))
146	145	rexlimdvva 3210	. . . 4 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴)))
147	2, 146	syl5 34	. . 3 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) → 𝑓 ∈ (𝐸 “ 𝐴)))
148		ffun 6739	. . . . . 6 ⊢ (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld ↑s ℂ)) → Fun 𝐸)
149	95, 148	ax-mp 5	. . . . 5 ⊢ Fun 𝐸
150		fvelima 6973	. . . . 5 ⊢ ((Fun 𝐸 ∧ 𝑓 ∈ (𝐸 “ 𝐴)) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓)
151	149, 150	mpan 690	. . . 4 ⊢ (𝑓 ∈ (𝐸 “ 𝐴) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓)
152	99	sselda 3994	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ (Base‘(Poly1‘ℂfld)))
153		eqid 2734	. . . . . . . . . . . 12 ⊢ ( ·𝑠 ‘(Poly1‘ℂfld)) = ( ·𝑠 ‘(Poly1‘ℂfld))
154		eqid 2734	. . . . . . . . . . . 12 ⊢ (coe1‘𝑎) = (coe1‘𝑎)
155	54, 114, 93, 153, 110, 116, 154	ply1coe 22317	. . . . . . . . . . 11 ⊢ ((ℂfld ∈ Ring ∧ 𝑎 ∈ (Base‘(Poly1‘ℂfld))) → 𝑎 = ((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
156	9, 152, 155	sylancr 587	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑎 = ((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
157	156	fveq2d 6910	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝐸‘((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))))
158		eqid 2734	. . . . . . . . . 10 ⊢ (0g‘(Poly1‘ℂfld)) = (0g‘(Poly1‘ℂfld))
159	54	ply1ring 22264	. . . . . . . . . . . 12 ⊢ (ℂfld ∈ Ring → (Poly1‘ℂfld) ∈ Ring)
160	9, 159	ax-mp 5	. . . . . . . . . . 11 ⊢ (Poly1‘ℂfld) ∈ Ring
161		ringcmn 20295	. . . . . . . . . . 11 ⊢ ((Poly1‘ℂfld) ∈ Ring → (Poly1‘ℂfld) ∈ CMnd)
162	160, 161	mp1i 13	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (Poly1‘ℂfld) ∈ CMnd)
163		ringmnd 20260	. . . . . . . . . . 11 ⊢ ((ℂfld ↑s ℂ) ∈ Ring → (ℂfld ↑s ℂ) ∈ Mnd)
164	49, 163	mp1i 13	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (ℂfld ↑s ℂ) ∈ Mnd)
165		nn0ex 12529	. . . . . . . . . . 11 ⊢ ℕ0 ∈ V
166	165	a1i 11	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℕ0 ∈ V)
167		rhmghm 20500	. . . . . . . . . . . 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 19256	. . . . . . . . . . 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 22268	. . . . . . . . . . . . 13 ⊢ (ℂfld ∈ Ring → (Poly1‘ℂfld) ∈ LMod)
172	9, 171	mp1i 13	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (Poly1‘ℂfld) ∈ LMod)
173	12	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑆 ⊆ ℂ)
174		eqid 2734	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝑅) = (Base‘𝑅)
175	154, 59, 58, 174	coe1f 22228	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ 𝐴 → (coe1‘𝑎):ℕ0⟶(Base‘𝑅))
176	57	subrgbas 20597	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 = (Base‘𝑅))
177	176	feq3d 6723	. . . . . . . . . . . . . . . 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 7103	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝑎)‘𝑘) ∈ 𝑆)
181	173, 180	sseldd 3995	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝑎)‘𝑘) ∈ ℂ)
182	110, 93	mgpbas 20157	. . . . . . . . . . . . 13 ⊢ (Base‘(Poly1‘ℂfld)) = (Base‘(mulGrp‘(Poly1‘ℂfld)))
183	110	ringmgp 20256	. . . . . . . . . . . . . 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 22234	. . . . . . . . . . . . . 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 19125	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)))
189	54	ply1sca 22269	. . . . . . . . . . . . . 14 ⊢ (ℂfld ∈ Ring → ℂfld = (Scalar‘(Poly1‘ℂfld)))
190	9, 189	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ℂfld = (Scalar‘(Poly1‘ℂfld))
191	93, 190, 153, 4	lmodvscl 20892	. . . . . . . . . . . 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 1370	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(Poly1‘ℂfld)))
193	192	fmpttd 7134	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℕ0⟶(Base‘(Poly1‘ℂfld)))
194	165	mptex 7242	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ V
195		funmpt 6605	. . . . . . . . . . . . 13 ⊢ Fun (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
196		fvex 6919	. . . . . . . . . . . . 13 ⊢ (0g‘(Poly1‘ℂfld)) ∈ V
197	194, 195, 196	3pm3.2i 1338	. . . . . . . . . . . 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 22230	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → (coe1‘𝑎) finSupp 0)
200	152, 199	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) finSupp 0)
201	200	fsuppimpd 9406	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) ∈ Fin)
202	179	feqmptd 6976	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) = (𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)))
203	202	oveq1d 7445	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)) supp 0))
204		eqimss2 4054	. . . . . . . . . . . . 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 20909	. . . . . . . . . . . . 13 ⊢ (((Poly1‘ℂfld) ∈ LMod ∧ 𝑥 ∈ (Base‘(Poly1‘ℂfld))) → (0( ·𝑠 ‘(Poly1‘ℂfld))𝑥) = (0g‘(Poly1‘ℂfld)))
208	206, 207	sylan 580	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (Base‘(Poly1‘ℂfld))) → (0( ·𝑠 ‘(Poly1‘ℂfld))𝑥) = (0g‘(Poly1‘ℂfld)))
209		c0ex 11252	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
210	209	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 0 ∈ V)
211	205, 208, 180, 188, 210	suppssov1 8220	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) supp (0g‘(Poly1‘ℂfld))) ⊆ ((coe1‘𝑎) supp 0))
212		suppssfifsupp 9417	. . . . . . . . . . 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 19970	. . . . . . . . 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 7151	. . . . . . . . . . 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 7102	. . . . . . . . . . . . . . . 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 17535	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℂ⟶ℂ)
222	221	feqmptd 6976	. . . . . . . . . . . . 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 22356	. . . . . . . . . . . . . . . . . 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 22364	. . . . . . . . . . . . . . . . 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 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘))
229	228	eqeq2d 2745	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧) ↔ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘)))
230	229	anbi2d 630	. . . . . . . . . . . . . . . . 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 22363	. . . . . . . . . . . . . . 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 5247	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧)) = (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
236	222, 235	eqtrd 2774	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) = (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
237	236	mpteq2dva 5247	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))
238	216, 237	eqtrd 2774	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))
239	238	oveq2d 7446	. . . . . . . . 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 2780	. . . . . . . 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 715	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝑎)‘𝑘) ∈ ℂ)
244	33	adantll 714	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ)
245	243, 244	mulcld 11278	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
246	245	anasss 466	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
247	165	mptex 7242	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V
248		funmpt 6605	. . . . . . . . . . . 12 ⊢ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
249	247, 248, 39	3pm3.2i 1338	. . . . . . . . . . 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 14010	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ∈ Fin)
252		eldifn 4141	. . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑎 ∈ (Base‘(Poly1‘ℂfld)))
255		eldifi 4140	. . . . . . . . . . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (deg1‘ℂfld) = (deg1‘ℂfld)
258	257, 54, 93, 17, 154	deg1ge 26151	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ (Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0 ∧ ((coe1‘𝑎)‘𝑘) ≠ 0) → 𝑘 ≤ ((deg1‘ℂfld)‘𝑎))
259	258	3expia 1120	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ (Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0) → (((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ ((deg1‘ℂfld)‘𝑎)))
260	254, 256, 259	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ ((deg1‘ℂfld)‘𝑎)))
261		0xr 11305	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ*
262	257, 54, 93	deg1xrcl 26135	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → ((deg1‘ℂfld)‘𝑎) ∈ ℝ*)
263	152, 262	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((deg1‘ℂfld)‘𝑎) ∈ ℝ*)
264	263	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → ((deg1‘ℂfld)‘𝑎) ∈ ℝ*)
265		xrmax2 13214	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0 ∈ ℝ* ∧ ((deg1‘ℂfld)‘𝑎) ∈ ℝ*) → ((deg1‘ℂfld)‘𝑎) ≤ if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))
266	261, 264, 265	sylancr 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → ((deg1‘ℂfld)‘𝑎) ≤ if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))
267	256	nn0red 12585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ)
268	267	rexrd 11308	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ*)
269		ifcl 4575	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((deg1‘ℂfld)‘𝑎) ∈ ℝ* ∧ 0 ∈ ℝ*) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℝ*)
270	264, 261, 269	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℝ*)
271		xrletr 13196	. . . . . . . . . . . . . . . . . . . . . . 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 1370	. . . . . . . . . . . . . . . . . . . . . 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 694	. . . . . . . . . . . . . . . . . . . . 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 26136	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → ((deg1‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
277	152, 276	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((deg1‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
278		elun 4162	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}) ↔ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((deg1‘ℂfld)‘𝑎) ∈ {-∞}))
279	277, 278	sylib 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((deg1‘ℂfld)‘𝑎) ∈ {-∞}))
280		nn0ge0 12548	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → 0 ≤ ((deg1‘ℂfld)‘𝑎))
281	280	iftrued 4538	. . . . . . . . . . . . . . . . . . . . . . . 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 2838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
284		mnflt0 13164	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ -∞ < 0
285		mnfxr 11315	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ -∞ ∈ ℝ*
286		xrltnle 11325	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*) → (-∞ < 0 ↔ ¬ 0 ≤ -∞))
287	285, 261, 286	mp2an 692	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (-∞ < 0 ↔ ¬ 0 ≤ -∞)
288	284, 287	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ¬ 0 ≤ -∞
289		elsni 4647	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → ((deg1‘ℂfld)‘𝑎) = -∞)
290	289	breq2d 5159	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → (0 ≤ ((deg1‘ℂfld)‘𝑎) ↔ 0 ≤ -∞))
291	288, 290	mtbiri 327	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → ¬ 0 ≤ ((deg1‘ℂfld)‘𝑎))
292	291	iffalsed 4541	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) = 0)
293		0nn0 12538	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ ℕ0
294	292, 293	eqeltrdi 2846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
295	283, 294	jaoi 857	. . . . . . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
298		fznn0 13655	. . . . . . . . . . . . . . . . . . . 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 2955	. . . . . . . . . . . . . . . . 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 7445	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘)))
304	255, 244	sylan2 593	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑧↑𝑘) ∈ ℂ)
305	304	mul02d 11456	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (0 · (𝑧↑𝑘)) = 0)
306	303, 305	eqtrd 2774	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = 0)
307	306	an32s 652	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) ∧ 𝑧 ∈ ℂ) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = 0)
308	307	mpteq2dva 5247	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ 0))
309		fconstmpt 5750	. . . . . . . . . . . . 13 ⊢ (ℂ × {0}) = (𝑧 ∈ ℂ ↦ 0)
310		ringmnd 20260	. . . . . . . . . . . . . . 15 ⊢ (ℂfld ∈ Ring → ℂfld ∈ Mnd)
311	9, 310	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ℂfld ∈ Mnd
312	3, 17	pws0g 18798	. . . . . . . . . . . . . 14 ⊢ ((ℂfld ∈ Mnd ∧ ℂ ∈ V) → (ℂ × {0}) = (0g‘(ℂfld ↑s ℂ)))
313	311, 6, 312	mp2an 692	. . . . . . . . . . . . 13 ⊢ (ℂ × {0}) = (0g‘(ℂfld ↑s ℂ))
314	309, 313	eqtr3i 2764	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℂ ↦ 0) = (0g‘(ℂfld ↑s ℂ))
315	308, 314	eqtrdi 2790	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) = (0g‘(ℂfld ↑s ℂ)))
316	315, 166	suppss2 8223	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) supp (0g‘(ℂfld ↑s ℂ))) ⊆ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
317		suppssfifsupp 9417	. . . . . . . . . 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 20014	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))))
320		fz0ssnn0 13658	. . . . . . . . . . . 12 ⊢ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ⊆ ℕ0
321		resmpt 6056	. . . . . . . . . . . 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 7441	. . . . . . . . . 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 7134	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))):ℕ0⟶ℂ)
327	306, 325	suppss2 8223	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) supp 0) ⊆ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
328	165	mptex 7242	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V
329		funmpt 6605	. . . . . . . . . . . . . 14 ⊢ Fun (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))
330	328, 329, 209	3pm3.2i 1338	. . . . . . . . . . . . 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 14010	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ∈ Fin)
333		suppssfifsupp 9417	. . . . . . . . . . . 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 19945	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) = (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))
336		elfznn0 13656	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) → 𝑘 ∈ ℕ0)
337	336, 245	sylan2 593	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
338	332, 337	gsumfsum 21469	. . . . . . . . . 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 2798	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))
340	339	mpteq2dva 5247	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
341	240, 319, 340	3eqtrd 2778	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
342	12	adantr 480	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑆 ⊆ ℂ)
343		elplyr 26254	. . . . . . . 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 1370	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆))
345	341, 344	eqeltrd 2838	. . . . . 6 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) ∈ (Poly‘𝑆))
346		eleq1 2826	. . . . . 6 ⊢ ((𝐸‘𝑎) = 𝑓 → ((𝐸‘𝑎) ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (Poly‘𝑆)))
347	345, 346	syl5ibcom 245	. . . . 5 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝐸‘𝑎) = 𝑓 → 𝑓 ∈ (Poly‘𝑆)))
348	347	rexlimdva 3152	. . . 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 2732	1 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (Poly‘𝑆) = (𝐸 “ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105   ≠ wne 2937  ∃wrex 3067  Vcvv 3477   ∖ cdif 3959   ∪ cun 3960   ⊆ wss 3962  ifcif 4530  {csn 4630   class class class wbr 5147   ↦ cmpt 5230   × cxp 5686   ↾ cres 5690   “ cima 5691   ∘ ccom 5692  Fun wfun 6556   Fn wfn 6557  ⟶wf 6558  ‘cfv 6562  (class class class)co 7430   ∘_f cof 7694   supp csupp 8183   ↑_m cmap 8864  Fincfn 8983   finSupp cfsupp 9398  ℂcc 11150  0cc0 11152   · cmul 11157  -∞cmnf 11290  ℝ^*cxr 11291   < clt 11292   ≤ cle 11293  ℕ₀cn0 12523  ...cfz 13543  ↑cexp 14098  Σcsu 15718  Basecbs 17244   ↾_s cress 17273  ._rcmulr 17298  Scalarcsca 17300   ·_𝑠 cvsca 17301  0_gc0g 17485   Σ_g cgsu 17486   ↑_s cpws 17492  Mndcmnd 18759   MndHom cmhm 18806  SubMndcsubmnd 18807  ._gcmg 19097  SubGrpcsubg 19150   GrpHom cghm 19242  CMndccmn 19812  mulGrpcmgp 20151  Ringcrg 20250  CRingccrg 20251   RingHom crh 20485  SubRingcsubrg 20585  LModclmod 20874  ℂ_fldccnfld 21381  algSccascl 21889  var₁cv1 22192  Poly₁cpl1 22193  coe₁cco1 22194  eval₁ce1 22333  deg₁cdg1 26107  Polycply 26237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230  ax-addf 11231  ax-mulf 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-ofr 7697  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-pm 8867  df-ixp 8936  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-sup 9479  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-rp 13032  df-fz 13544  df-fzo 13691  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-0g 17487  df-gsum 17488  df-prds 17493  df-pws 17495  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-mhm 18808  df-submnd 18809  df-grp 18966  df-minusg 18967  df-sbg 18968  df-mulg 19098  df-subg 19153  df-ghm 19243  df-cntz 19347  df-cmn 19814  df-abl 19815  df-mgp 20152  df-rng 20170  df-ur 20199  df-srg 20204  df-ring 20252  df-cring 20253  df-rhm 20488  df-subrng 20562  df-subrg 20586  df-lmod 20876  df-lss 20947  df-lsp 20987  df-cnfld 21382  df-assa 21890  df-asp 21891  df-ascl 21892  df-psr 21946  df-mvr 21947  df-mpl 21948  df-opsr 21950  df-evls 22115  df-evl 22116  df-psr1 22196  df-vr1 22197  df-ply1 22198  df-coe1 22199  df-evl1 22335  df-mdeg 26108  df-deg1 26109  df-ply 26241

This theorem is referenced by: (None)