Theorem plypf1 26150

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 26133	. . . . 5 ⊢ (𝑓 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))
2	1	simprbi 496	. . . 4 ⊢ (𝑓 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
3		eqid 2729	. . . . . . . . 9 ⊢ (ℂfld ↑s ℂ) = (ℂfld ↑s ℂ)
4		cnfldbas 21300	. . . . . . . . 9 ⊢ ℂ = (Base‘ℂfld)
5		eqid 2729	. . . . . . . . 9 ⊢ (0g‘(ℂfld ↑s ℂ)) = (0g‘(ℂfld ↑s ℂ))
6		cnex 11125	. . . . . . . . . 10 ⊢ ℂ ∈ V
7	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ℂ ∈ V)
8		fzfid 13914	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (0...𝑛) ∈ Fin)
9		cnring 21332	. . . . . . . . . 10 ⊢ ℂfld ∈ Ring
10		ringcmn 20202	. . . . . . . . . 10 ⊢ (ℂfld ∈ Ring → ℂfld ∈ CMnd)
11	9, 10	mp1i 13	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ℂfld ∈ CMnd)
12	4	subrgss 20492	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ⊆ ℂ)
13	12	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ⊆ ℂ)
14		elmapi 8799	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
15	14	ad2antll 729	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
16		subrgsubg 20497	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ∈ (SubGrp‘ℂfld))
17		cnfld0 21334	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 = (0g‘ℂfld)
18	17	subg0cl 19048	. . . . . . . . . . . . . . . . . . 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 4769	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → {0} ⊆ 𝑆)
22		ssequn2 4148	. . . . . . . . . . . . . . . 16 ⊢ ({0} ⊆ 𝑆 ↔ (𝑆 ∪ {0}) = 𝑆)
23	21, 22	sylib 218	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑆 ∪ {0}) = 𝑆)
24	23	feq3d 6655	. . . . . . . . . . . . . 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 13557	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0)
27		ffvelcdm 7035	. . . . . . . . . . . . 13 ⊢ ((𝑎:ℕ0⟶𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑎‘𝑘) ∈ 𝑆)
28	25, 26, 27	syl2an 596	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ 𝑆)
29	13, 28	sseldd 3944	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ ℂ)
30	29	adantrl 716	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑎‘𝑘) ∈ ℂ)
31		simprl 770	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑧 ∈ ℂ)
32	26	ad2antll 729	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑘 ∈ ℕ0)
33		expcl 14020	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ)
34	31, 32, 33	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑧↑𝑘) ∈ ℂ)
35	30, 34	mulcld 11170	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → ((𝑎‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
36		eqid 2729	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))
37	6	mptex 7179	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V
38	37	a1i 11	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V)
39		fvex 6853	. . . . . . . . . . 11 ⊢ (0g‘(ℂfld ↑s ℂ)) ∈ V
40	39	a1i 11	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (0g‘(ℂfld ↑s ℂ)) ∈ V)
41	36, 8, 38, 40	fsuppmptdm 9303	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp (0g‘(ℂfld ↑s ℂ)))
42	3, 4, 5, 7, 8, 11, 35, 41	pwsgsum 19896	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))))
43		fzfid 13914	. . . . . . . . . 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 21376	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
46	45	mpteq2dva 5195	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
47	42, 46	eqtrd 2764	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
48	3	pwsring 20244	. . . . . . . . . 10 ⊢ ((ℂfld ∈ Ring ∧ ℂ ∈ V) → (ℂfld ↑s ℂ) ∈ Ring)
49	9, 6, 48	mp2an 692	. . . . . . . . 9 ⊢ (ℂfld ↑s ℂ) ∈ Ring
50		ringcmn 20202	. . . . . . . . 9 ⊢ ((ℂfld ↑s ℂ) ∈ Ring → (ℂfld ↑s ℂ) ∈ CMnd)
51	49, 50	mp1i 13	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (ℂfld ↑s ℂ) ∈ CMnd)
52		cncrng 21330	. . . . . . . . . . 11 ⊢ ℂfld ∈ CRing
53		plypf1.e	. . . . . . . . . . . 12 ⊢ 𝐸 = (eval1‘ℂfld)
54		eqid 2729	. . . . . . . . . . . 12 ⊢ (Poly1‘ℂfld) = (Poly1‘ℂfld)
55	53, 54, 3, 4	evl1rhm 22252	. . . . . . . . . . 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 22150	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
61	60	adantr 480	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
62		rhmima 20524	. . . . . . . . . 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 20497	. . . . . . . . 9 ⊢ ((𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)) → (𝐸 “ 𝐴) ∈ (SubGrp‘(ℂfld ↑s ℂ)))
65		subgsubm 19062	. . . . . . . . 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 2729	. . . . . . . . . . . 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 6731	. . . . . . . . . . . . . 14 ⊢ ((𝑎‘𝑘) ∈ ℂ → (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)
71	29, 70	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)
72	3, 4, 67	pwselbasb 17427	. . . . . . . . . . . . . 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 7069	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ)
77	3, 4, 67	pwselbasb 17427	. . . . . . . . . . . . . 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 21304	. . . . . . . . . . . 12 ⊢ · = (.r‘ℂfld)
81		eqid 2729	. . . . . . . . . . . 12 ⊢ (.r‘(ℂfld ↑s ℂ)) = (.r‘(ℂfld ↑s ℂ))
82	3, 67, 68, 69, 74, 79, 80, 81	pwsmulrval 17430	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = ((ℂ × {(𝑎‘𝑘)}) ∘f · (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))))
83	29	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑎‘𝑘) ∈ ℂ)
84		fconstmpt 5693	. . . . . . . . . . . . 13 ⊢ (ℂ × {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘))
85	84	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘)))
86		eqidd 2730	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))
87	69, 83, 75, 85, 86	offval2 7653	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)}) ∘f · (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))
88	82, 87	eqtrd 2764	. . . . . . . . . 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 2729	. . . . . . . . . . . . . 14 ⊢ (algSc‘(Poly1‘ℂfld)) = (algSc‘(Poly1‘ℂfld))
91	53, 54, 4, 90	evl1sca 22254	. . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Poly1‘ℂfld)) = (Base‘(Poly1‘ℂfld))
94	93, 67	rhmf 20405	. . . . . . . . . . . . . . 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 6670	. . . . . . . . . . . . . 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 20492	. . . . . . . . . . . . . . 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 766	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ∈ (SubRing‘ℂfld))
102	54, 90, 57, 58, 101, 59, 4, 29	subrg1asclcl 22179	. . . . . . . . . . . . . 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 7189	. . . . . . . . . . . . 13 ⊢ ((𝐸 Fn (Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆ (Base‘(Poly1‘ℂfld)) ∧ ((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) ∈ (𝐸 “ 𝐴))
105	97, 100, 103, 104	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) ∈ (𝐸 “ 𝐴))
106	92, 105	eqeltrrd 2829	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴))
107	67	subrgss 20492	. . . . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (mulGrp‘(Poly1‘ℂfld)) = (mulGrp‘(Poly1‘ℂfld))
111	110	subrgsubm 20505	. . . . . . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ (var1‘ℂfld) = (var1‘ℂfld)
115	114, 101, 57, 58, 59	subrgvr1cl 22181	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (var1‘ℂfld) ∈ 𝐴)
116		eqid 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ (.g‘(mulGrp‘(Poly1‘ℂfld))) = (.g‘(mulGrp‘(Poly1‘ℂfld)))
117	116	submmulgcl 19031	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))) ∧ 𝑘 ∈ ℕ0 ∧ (var1‘ℂfld) ∈ 𝐴) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
118	112, 113, 115, 117	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
119		fnfvima 7189	. . . . . . . . . . . . . . . . 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 1373	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (𝐸 “ 𝐴))
121	108, 120	sseldd 3944	. . . . . . . . . . . . . . 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 17428	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))):ℂ⟶ℂ)
123	122	feqmptd 6911	. . . . . . . . . . . . 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 22257	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧))
127		eqid 2729	. . . . . . . . . . . . . . . . 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 22265	. . . . . . . . . . . . . . . 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 21346	. . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘))
134	133	mpteq2dva 5195	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))
135	123, 134	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))
136	135, 120	eqeltrrd 2829	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴))
137	81	subrgmcl 20504	. . . . . . . . . . 11 ⊢ (((𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)) ∧ (ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴) ∧ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
138	89, 106, 136, 137	syl3anc 1373	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
139	88, 138	eqeltrrd 2829	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
140	139	fmpttd 7069	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))):(0...𝑛)⟶(𝐸 “ 𝐴))
141	36, 8, 139, 40	fsuppmptdm 9303	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp (0g‘(ℂfld ↑s ℂ)))
142	5, 51, 8, 66, 140, 141	gsumsubmcl 19833	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) ∈ (𝐸 “ 𝐴))
143	47, 142	eqeltrrd 2829	. . . . . 6 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
144		eleq1 2816	. . . . . 6 ⊢ (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → (𝑓 ∈ (𝐸 “ 𝐴) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)))
145	143, 144	syl5ibrcom 247	. . . . 5 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴)))
146	145	rexlimdvva 3192	. . . 4 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴)))
147	2, 146	syl5 34	. . 3 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) → 𝑓 ∈ (𝐸 “ 𝐴)))
148		ffun 6673	. . . . . 6 ⊢ (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld ↑s ℂ)) → Fun 𝐸)
149	95, 148	ax-mp 5	. . . . 5 ⊢ Fun 𝐸
150		fvelima 6908	. . . . 5 ⊢ ((Fun 𝐸 ∧ 𝑓 ∈ (𝐸 “ 𝐴)) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓)
151	149, 150	mpan 690	. . . 4 ⊢ (𝑓 ∈ (𝐸 “ 𝐴) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓)
152	99	sselda 3943	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ (Base‘(Poly1‘ℂfld)))
153		eqid 2729	. . . . . . . . . . . 12 ⊢ ( ·𝑠 ‘(Poly1‘ℂfld)) = ( ·𝑠 ‘(Poly1‘ℂfld))
154		eqid 2729	. . . . . . . . . . . 12 ⊢ (coe1‘𝑎) = (coe1‘𝑎)
155	54, 114, 93, 153, 110, 116, 154	ply1coe 22218	. . . . . . . . . . 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 6844	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝐸‘((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))))
158		eqid 2729	. . . . . . . . . 10 ⊢ (0g‘(Poly1‘ℂfld)) = (0g‘(Poly1‘ℂfld))
159	54	ply1ring 22165	. . . . . . . . . . . 12 ⊢ (ℂfld ∈ Ring → (Poly1‘ℂfld) ∈ Ring)
160	9, 159	ax-mp 5	. . . . . . . . . . 11 ⊢ (Poly1‘ℂfld) ∈ Ring
161		ringcmn 20202	. . . . . . . . . . 11 ⊢ ((Poly1‘ℂfld) ∈ Ring → (Poly1‘ℂfld) ∈ CMnd)
162	160, 161	mp1i 13	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (Poly1‘ℂfld) ∈ CMnd)
163		ringmnd 20163	. . . . . . . . . . 11 ⊢ ((ℂfld ↑s ℂ) ∈ Ring → (ℂfld ↑s ℂ) ∈ Mnd)
164	49, 163	mp1i 13	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (ℂfld ↑s ℂ) ∈ Mnd)
165		nn0ex 12424	. . . . . . . . . . 11 ⊢ ℕ0 ∈ V
166	165	a1i 11	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℕ0 ∈ V)
167		rhmghm 20404	. . . . . . . . . . . 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 19140	. . . . . . . . . . 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 22169	. . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝑅) = (Base‘𝑅)
175	154, 59, 58, 174	coe1f 22129	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ 𝐴 → (coe1‘𝑎):ℕ0⟶(Base‘𝑅))
176	57	subrgbas 20501	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 = (Base‘𝑅))
177	176	feq3d 6655	. . . . . . . . . . . . . . . 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 7038	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝑎)‘𝑘) ∈ 𝑆)
181	173, 180	sseldd 3944	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝑎)‘𝑘) ∈ ℂ)
182	110, 93	mgpbas 20065	. . . . . . . . . . . . 13 ⊢ (Base‘(Poly1‘ℂfld)) = (Base‘(mulGrp‘(Poly1‘ℂfld)))
183	110	ringmgp 20159	. . . . . . . . . . . . . 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 22135	. . . . . . . . . . . . . 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 19009	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)))
189	54	ply1sca 22170	. . . . . . . . . . . . . 14 ⊢ (ℂfld ∈ Ring → ℂfld = (Scalar‘(Poly1‘ℂfld)))
190	9, 189	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ℂfld = (Scalar‘(Poly1‘ℂfld))
191	93, 190, 153, 4	lmodvscl 20816	. . . . . . . . . . . 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 1373	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(Poly1‘ℂfld)))
193	192	fmpttd 7069	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℕ0⟶(Base‘(Poly1‘ℂfld)))
194	165	mptex 7179	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ V
195		funmpt 6538	. . . . . . . . . . . . 13 ⊢ Fun (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
196		fvex 6853	. . . . . . . . . . . . 13 ⊢ (0g‘(Poly1‘ℂfld)) ∈ V
197	194, 195, 196	3pm3.2i 1340	. . . . . . . . . . . 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 22131	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → (coe1‘𝑎) finSupp 0)
200	152, 199	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) finSupp 0)
201	200	fsuppimpd 9296	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) ∈ Fin)
202	179	feqmptd 6911	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) = (𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)))
203	202	oveq1d 7384	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)) supp 0))
204		eqimss2 4003	. . . . . . . . . . . . 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 20833	. . . . . . . . . . . . 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 11144	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
210	209	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 0 ∈ V)
211	205, 208, 180, 188, 210	suppssov1 8153	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) supp (0g‘(Poly1‘ℂfld))) ⊆ ((coe1‘𝑎) supp 0))
212		suppssfifsupp 9307	. . . . . . . . . . 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 836	. . . . . . . . . 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 19852	. . . . . . . . 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 7086	. . . . . . . . . . 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 7037	. . . . . . . . . . . . . . . 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 17428	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℂ⟶ℂ)
222	221	feqmptd 6911	. . . . . . . . . . . . 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 22257	. . . . . . . . . . . . . . . . . 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 22265	. . . . . . . . . . . . . . . . 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 2740	. . . . . . . . . . . . . . . . . 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 22264	. . . . . . . . . . . . . . 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 5195	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧)) = (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
236	222, 235	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) = (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
237	236	mpteq2dva 5195	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))
238	216, 237	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))
239	238	oveq2d 7385	. . . . . . . . 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 2770	. . . . . . . 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 11170	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
246	245	anasss 466	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
247	165	mptex 7179	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V
248		funmpt 6538	. . . . . . . . . . . 12 ⊢ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
249	247, 248, 39	3pm3.2i 1340	. . . . . . . . . . 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 13914	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ∈ Fin)
252		eldifn 4091	. . . . . . . . . . . . . . . . . 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 4090	. . . . . . . . . . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (deg1‘ℂfld) = (deg1‘ℂfld)
258	257, 54, 93, 17, 154	deg1ge 26036	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ (Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0 ∧ ((coe1‘𝑎)‘𝑘) ≠ 0) → 𝑘 ≤ ((deg1‘ℂfld)‘𝑎))
259	258	3expia 1121	. . . . . . . . . . . . . . . . . . . . . 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 11197	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ*
262	257, 54, 93	deg1xrcl 26020	. . . . . . . . . . . . . . . . . . . . . . . . 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 13112	. . . . . . . . . . . . . . . . . . . . . . 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 12480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ)
268	267	rexrd 11200	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ*)
269		ifcl 4530	. . . . . . . . . . . . . . . . . . . . . . . 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 13094	. . . . . . . . . . . . . . . . . . . . . . 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 1373	. . . . . . . . . . . . . . . . . . . . . 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 26021	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → ((deg1‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
277	152, 276	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((deg1‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
278		elun 4112	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}) ↔ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((deg1‘ℂfld)‘𝑎) ∈ {-∞}))
279	277, 278	sylib 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((deg1‘ℂfld)‘𝑎) ∈ {-∞}))
280		nn0ge0 12443	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → 0 ≤ ((deg1‘ℂfld)‘𝑎))
281	280	iftrued 4492	. . . . . . . . . . . . . . . . . . . . . . . 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 2828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
284		mnflt0 13061	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ -∞ < 0
285		mnfxr 11207	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ -∞ ∈ ℝ*
286		xrltnle 11217	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*) → (-∞ < 0 ↔ ¬ 0 ≤ -∞))
287	285, 261, 286	mp2an 692	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (-∞ < 0 ↔ ¬ 0 ≤ -∞)
288	284, 287	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ¬ 0 ≤ -∞
289		elsni 4602	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → ((deg1‘ℂfld)‘𝑎) = -∞)
290	289	breq2d 5114	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → (0 ≤ ((deg1‘ℂfld)‘𝑎) ↔ 0 ≤ -∞))
291	288, 290	mtbiri 327	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → ¬ 0 ≤ ((deg1‘ℂfld)‘𝑎))
292	291	iffalsed 4495	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) = 0)
293		0nn0 12433	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ ℕ0
294	292, 293	eqeltrdi 2836	. . . . . . . . . . . . . . . . . . . . . . 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 13556	. . . . . . . . . . . . . . . . . . . 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 2943	. . . . . . . . . . . . . . . . 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 7384	. . . . . . . . . . . . . . 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 11348	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (0 · (𝑧↑𝑘)) = 0)
306	303, 305	eqtrd 2764	. . . . . . . . . . . . . 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 5195	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ 0))
309		fconstmpt 5693	. . . . . . . . . . . . 13 ⊢ (ℂ × {0}) = (𝑧 ∈ ℂ ↦ 0)
310		ringmnd 20163	. . . . . . . . . . . . . . 15 ⊢ (ℂfld ∈ Ring → ℂfld ∈ Mnd)
311	9, 310	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ℂfld ∈ Mnd
312	3, 17	pws0g 18682	. . . . . . . . . . . . . 14 ⊢ ((ℂfld ∈ Mnd ∧ ℂ ∈ V) → (ℂ × {0}) = (0g‘(ℂfld ↑s ℂ)))
313	311, 6, 312	mp2an 692	. . . . . . . . . . . . 13 ⊢ (ℂ × {0}) = (0g‘(ℂfld ↑s ℂ))
314	309, 313	eqtr3i 2754	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℂ ↦ 0) = (0g‘(ℂfld ↑s ℂ))
315	308, 314	eqtrdi 2780	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) = (0g‘(ℂfld ↑s ℂ)))
316	315, 166	suppss2 8156	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) supp (0g‘(ℂfld ↑s ℂ))) ⊆ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
317		suppssfifsupp 9307	. . . . . . . . . 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 836	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) finSupp (0g‘(ℂfld ↑s ℂ)))
319	3, 4, 5, 241, 166, 242, 246, 318	pwsgsum 19896	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))))
320		fz0ssnn0 13559	. . . . . . . . . . . 12 ⊢ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ⊆ ℕ0
321		resmpt 5997	. . . . . . . . . . . 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 7380	. . . . . . . . . 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 7069	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))):ℕ0⟶ℂ)
327	306, 325	suppss2 8156	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) supp 0) ⊆ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
328	165	mptex 7179	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V
329		funmpt 6538	. . . . . . . . . . . . . 14 ⊢ Fun (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))
330	328, 329, 209	3pm3.2i 1340	. . . . . . . . . . . . 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 13914	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ∈ Fin)
333		suppssfifsupp 9307	. . . . . . . . . . . 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 836	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) finSupp 0)
335	4, 17, 324, 325, 326, 327, 334	gsumres 19827	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) = (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))
336		elfznn0 13557	. . . . . . . . . . . 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 21376	. . . . . . . . . 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 2788	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))
340	339	mpteq2dva 5195	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
341	240, 319, 340	3eqtrd 2768	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
342	12	adantr 480	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑆 ⊆ ℂ)
343		elplyr 26139	. . . . . . . 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 1373	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆))
345	341, 344	eqeltrd 2828	. . . . . 6 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) ∈ (Poly‘𝑆))
346		eleq1 2816	. . . . . 6 ⊢ ((𝐸‘𝑎) = 𝑓 → ((𝐸‘𝑎) ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (Poly‘𝑆)))
347	345, 346	syl5ibcom 245	. . . . 5 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝐸‘𝑎) = 𝑓 → 𝑓 ∈ (Poly‘𝑆)))
348	347	rexlimdva 3134	. . . 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 2727	1 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (Poly‘𝑆) = (𝐸 “ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∃wrex 3053  Vcvv 3444   ∖ cdif 3908   ∪ cun 3909   ⊆ wss 3911  ifcif 4484  {csn 4585   class class class wbr 5102   ↦ cmpt 5183   × cxp 5629   ↾ cres 5633   “ cima 5634   ∘ ccom 5635  Fun wfun 6493   Fn wfn 6494  ⟶wf 6495  ‘cfv 6499  (class class class)co 7369   ∘_f cof 7631   supp csupp 8116   ↑_m cmap 8776  Fincfn 8895   finSupp cfsupp 9288  ℂcc 11042  0cc0 11044   · cmul 11049  -∞cmnf 11182  ℝ^*cxr 11183   < clt 11184   ≤ cle 11185  ℕ₀cn0 12418  ...cfz 13444  ↑cexp 14002  Σcsu 15628  Basecbs 17155   ↾_s cress 17176  ._rcmulr 17197  Scalarcsca 17199   ·_𝑠 cvsca 17200  0_gc0g 17378   Σ_g cgsu 17379   ↑_s cpws 17385  Mndcmnd 18643   MndHom cmhm 18690  SubMndcsubmnd 18691  ._gcmg 18981  SubGrpcsubg 19034   GrpHom cghm 19126  CMndccmn 19694  mulGrpcmgp 20060  Ringcrg 20153  CRingccrg 20154   RingHom crh 20389  SubRingcsubrg 20489  LModclmod 20798  ℂ_fldccnfld 21296  algSccascl 21794  var₁cv1 22093  Poly₁cpl1 22094  coe₁cco1 22095  eval₁ce1 22234  deg₁cdg1 25992  Polycply 26122

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-inf2 9570  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121  ax-pre-sup 11122  ax-addf 11123  ax-mulf 11124

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-iin 4954  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-of 7633  df-ofr 7634  df-om 7823  df-1st 7947  df-2nd 7948  df-supp 8117  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-2o 8412  df-er 8648  df-map 8778  df-pm 8779  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9289  df-sup 9369  df-oi 9439  df-card 9868  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-div 11812  df-nn 12163  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231  df-9 12232  df-n0 12419  df-z 12506  df-dec 12626  df-uz 12770  df-rp 12928  df-fz 13445  df-fzo 13592  df-seq 13943  df-exp 14003  df-hash 14272  df-cj 15041  df-re 15042  df-im 15043  df-sqrt 15177  df-abs 15178  df-clim 15430  df-sum 15629  df-struct 17093  df-sets 17110  df-slot 17128  df-ndx 17140  df-base 17156  df-ress 17177  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-0g 17380  df-gsum 17381  df-prds 17386  df-pws 17388  df-mre 17523  df-mrc 17524  df-acs 17526  df-mgm 18549  df-sgrp 18628  df-mnd 18644  df-mhm 18692  df-submnd 18693  df-grp 18850  df-minusg 18851  df-sbg 18852  df-mulg 18982  df-subg 19037  df-ghm 19127  df-cntz 19231  df-cmn 19696  df-abl 19697  df-mgp 20061  df-rng 20073  df-ur 20102  df-srg 20107  df-ring 20155  df-cring 20156  df-rhm 20392  df-subrng 20466  df-subrg 20490  df-lmod 20800  df-lss 20870  df-lsp 20910  df-cnfld 21297  df-assa 21795  df-asp 21796  df-ascl 21797  df-psr 21851  df-mvr 21852  df-mpl 21853  df-opsr 21855  df-evls 22014  df-evl 22015  df-psr1 22097  df-vr1 22098  df-ply1 22099  df-coe1 22100  df-evl1 22236  df-mdeg 25993  df-deg1 25994  df-ply 26126

This theorem is referenced by: (None)