Theorem plypf1 26338

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 26321	. . . . 5 ⊢ (𝑓 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))
2	1	simprbi 502	. . . 4 ⊢ (𝑓 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
3		eqid 2769	. . . . . . . . 9 ⊢ (ℂfld ↑s ℂ) = (ℂfld ↑s ℂ)
4		cnfldbas 21495	. . . . . . . . 9 ⊢ ℂ = (Base‘ℂfld)
5		eqid 2769	. . . . . . . . 9 ⊢ (0g‘(ℂfld ↑s ℂ)) = (0g‘(ℂfld ↑s ℂ))
6		cnex 11181	. . . . . . . . . 10 ⊢ ℂ ∈ V
7	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ℂ ∈ V)
8		fzfid 14009	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (0...𝑛) ∈ Fin)
9		cnring 21513	. . . . . . . . . 10 ⊢ ℂfld ∈ Ring
10		ringcmn 20365	. . . . . . . . . 10 ⊢ (ℂfld ∈ Ring → ℂfld ∈ CMnd)
11	9, 10	mp1i 14	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ℂfld ∈ CMnd)
12	4	subrgss 20657	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ⊆ ℂ)
13	12	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ⊆ ℂ)
14		elmapi 8846	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
15	14	ad2antll 741	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
16		subrgsubg 20662	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ∈ (SubGrp‘ℂfld))
17		cnfld0 21515	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 = (0g‘ℂfld)
18	17	subg0cl 19200	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (SubGrp‘ℂfld) → 0 ∈ 𝑆)
19	16, 18	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 0 ∈ 𝑆)
20	19	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 0 ∈ 𝑆)
21	20	snssd 4757	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → {0} ⊆ 𝑆)
22		ssequn2 4150	. . . . . . . . . . . . . . . 16 ⊢ ({0} ⊆ 𝑆 ↔ (𝑆 ∪ {0}) = 𝑆)
23	21, 22	sylib 221	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑆 ∪ {0}) = 𝑆)
24	23	feq3d 6691	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑎:ℕ0⟶(𝑆 ∪ {0}) ↔ 𝑎:ℕ0⟶𝑆))
25	15, 24	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 𝑎:ℕ0⟶𝑆)
26		elfznn0 13648	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0)
27		ffvelcdm 7077	. . . . . . . . . . . . 13 ⊢ ((𝑎:ℕ0⟶𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑎‘𝑘) ∈ 𝑆)
28	25, 26, 27	syl2an 607	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ 𝑆)
29	13, 28	sseldd 3946	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) ∈ ℂ)
30	29	adantrl 728	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑎‘𝑘) ∈ ℂ)
31		simprl 782	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑧 ∈ ℂ)
32	26	ad2antll 741	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑘 ∈ ℕ0)
33		expcl 14115	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ)
34	31, 32, 33	syl2anc 595	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑧↑𝑘) ∈ ℂ)
35	30, 34	mulcld 11229	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → ((𝑎‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
36		eqid 2769	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))
37	6	mptex 7222	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V
38	37	a1i 11	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ V)
39		fvex 6895	. . . . . . . . . . 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 9336	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp (0g‘(ℂfld ↑s ℂ)))
42	3, 4, 5, 7, 8, 11, 35, 41	pwsgsum 20052	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))))
43		fzfid 14009	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑧 ∈ ℂ) → (0...𝑛) ∈ Fin)
44	35	anassrs 472	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑛)) → ((𝑎‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
45	43, 44	gsumfsum 21553	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
46	45	mpteq2dva 5208	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
47	42, 46	eqtrd 2804	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
48	3	pwsring 20405	. . . . . . . . . 10 ⊢ ((ℂfld ∈ Ring ∧ ℂ ∈ V) → (ℂfld ↑s ℂ) ∈ Ring)
49	9, 6, 48	mp2an 704	. . . . . . . . 9 ⊢ (ℂfld ↑s ℂ) ∈ Ring
50		ringcmn 20365	. . . . . . . . 9 ⊢ ((ℂfld ↑s ℂ) ∈ Ring → (ℂfld ↑s ℂ) ∈ CMnd)
51	49, 50	mp1i 14	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (ℂfld ↑s ℂ) ∈ CMnd)
52		cncrng 21512	. . . . . . . . . . 11 ⊢ ℂfld ∈ CRing
53		plypf1.e	. . . . . . . . . . . 12 ⊢ 𝐸 = (eval1‘ℂfld)
54		eqid 2769	. . . . . . . . . . . 12 ⊢ (Poly1‘ℂfld) = (Poly1‘ℂfld)
55	53, 54, 3, 4	evl1rhm 22461	. . . . . . . . . . 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 22361	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
61	60	adantr 485	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
62		rhmima 20689	. . . . . . . . . 10 ⊢ ((𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂfld ↑s ℂ)) ∧ 𝐴 ∈ (SubRing‘(Poly1‘ℂfld))) → (𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)))
63	56, 61, 62	sylancr 598	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)))
64		subrgsubg 20662	. . . . . . . . 9 ⊢ ((𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)) → (𝐸 “ 𝐴) ∈ (SubGrp‘(ℂfld ↑s ℂ)))
65		subgsubm 19215	. . . . . . . . 9 ⊢ ((𝐸 “ 𝐴) ∈ (SubGrp‘(ℂfld ↑s ℂ)) → (𝐸 “ 𝐴) ∈ (SubMnd‘(ℂfld ↑s ℂ)))
66	63, 64, 65	3syl 19	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝐸 “ 𝐴) ∈ (SubMnd‘(ℂfld ↑s ℂ)))
67		eqid 2769	. . . . . . . . . . . 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 6768	. . . . . . . . . . . . . 14 ⊢ ((𝑎‘𝑘) ∈ ℂ → (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)
71	29, 70	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)
72	3, 4, 67	pwselbasb 17541	. . . . . . . . . . . . . 14 ⊢ ((ℂfld ∈ Ring ∧ ℂ ∈ V) → ((ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ))
73	9, 6, 72	mp2an 704	. . . . . . . . . . . . 13 ⊢ ((ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (ℂ × {(𝑎‘𝑘)}):ℂ⟶ℂ)
74	71, 73	sylibr 237	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) ∈ (Base‘(ℂfld ↑s ℂ)))
75	34	anass1rs 667	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑧↑𝑘) ∈ ℂ)
76	75	fmpttd 7111	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ)
77	3, 4, 67	pwselbasb 17541	. . . . . . . . . . . . . 14 ⊢ ((ℂfld ∈ Ring ∧ ℂ ∈ V) → ((𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ))
78	9, 6, 77	mp2an 704	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld ↑s ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)):ℂ⟶ℂ)
79	76, 78	sylibr 237	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (Base‘(ℂfld ↑s ℂ)))
80		cnfldmul 21499	. . . . . . . . . . . 12 ⊢ · = (.r‘ℂfld)
81		eqid 2769	. . . . . . . . . . . 12 ⊢ (.r‘(ℂfld ↑s ℂ)) = (.r‘(ℂfld ↑s ℂ))
82	3, 67, 68, 69, 74, 79, 80, 81	pwsmulrval 17545	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = ((ℂ × {(𝑎‘𝑘)}) ∘f · (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))))
83	29	adantr 485	. . . . . . . . . . . 12 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑎‘𝑘) ∈ ℂ)
84		fconstmpt 5724	. . . . . . . . . . . . 13 ⊢ (ℂ × {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘))
85	84	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎‘𝑘)))
86		eqidd 2770	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))
87	69, 83, 75, 85, 86	offval2 7695	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)}) ∘f · (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))
88	82, 87	eqtrd 2804	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))
89	63	adantr 485	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)))
90		eqid 2769	. . . . . . . . . . . . . 14 ⊢ (algSc‘(Poly1‘ℂfld)) = (algSc‘(Poly1‘ℂfld))
91	53, 54, 4, 90	evl1sca 22463	. . . . . . . . . . . . 13 ⊢ ((ℂfld ∈ CRing ∧ (𝑎‘𝑘) ∈ ℂ) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) = (ℂ × {(𝑎‘𝑘)}))
92	52, 29, 91	sylancr 598	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) = (ℂ × {(𝑎‘𝑘)}))
93		eqid 2769	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Poly1‘ℂfld)) = (Base‘(Poly1‘ℂfld))
94	93, 67	rhmf 20566	. . . . . . . . . . . . . . 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 6706	. . . . . . . . . . . . . 14 ⊢ (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld ↑s ℂ)) → 𝐸 Fn (Base‘(Poly1‘ℂfld)))
97	95, 96	mp1i 14	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐸 Fn (Base‘(Poly1‘ℂfld)))
98	93	subrgss 20657	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (SubRing‘(Poly1‘ℂfld)) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
99	60, 98	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
100	99	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
101		simpll 778	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ∈ (SubRing‘ℂfld))
102	54, 90, 57, 58, 101, 59, 4, 29	subrg1asclcl 22390	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴 ↔ (𝑎‘𝑘) ∈ 𝑆))
103	28, 102	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴)
104		fnfvima 7232	. . . . . . . . . . . . 13 ⊢ ((𝐸 Fn (Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆ (Base‘(Poly1‘ℂfld)) ∧ ((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘)) ∈ 𝐴) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) ∈ (𝐸 “ 𝐴))
105	97, 100, 103, 104	syl3anc 1396	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎‘𝑘))) ∈ (𝐸 “ 𝐴))
106	92, 105	eqeltrrd 2870	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴))
107	67	subrgss 20657	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)) → (𝐸 “ 𝐴) ⊆ (Base‘(ℂfld ↑s ℂ)))
108	89, 107	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸 “ 𝐴) ⊆ (Base‘(ℂfld ↑s ℂ)))
109	60	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
110		eqid 2769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (mulGrp‘(Poly1‘ℂfld)) = (mulGrp‘(Poly1‘ℂfld))
111	110	subrgsubm 20670	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ (SubRing‘(Poly1‘ℂfld)) → 𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))))
112	109, 111	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))))
113	26	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑘 ∈ ℕ0)
114		eqid 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ (var1‘ℂfld) = (var1‘ℂfld)
115	114, 101, 57, 58, 59	subrgvr1cl 22392	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (var1‘ℂfld) ∈ 𝐴)
116		eqid 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ (.g‘(mulGrp‘(Poly1‘ℂfld))) = (.g‘(mulGrp‘(Poly1‘ℂfld)))
117	116	submmulgcl 19183	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))) ∧ 𝑘 ∈ ℕ0 ∧ (var1‘ℂfld) ∈ 𝐴) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
118	112, 113, 115, 117	syl3anc 1396	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
119		fnfvima 7232	. . . . . . . . . . . . . . . . 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 1396	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (𝐸 “ 𝐴))
121	108, 120	sseldd 3946	. . . . . . . . . . . . . . 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 17542	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))):ℂ⟶ℂ)
123	122	feqmptd 6950	. . . . . . . . . . . . 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 489	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
126	53, 114, 4, 54, 93, 124, 125	evl1vard 22466	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧))
127		eqid 2769	. . . . . . . . . . . . . . . . 17 ⊢ (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
128	113	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0)
129	53, 54, 4, 93, 124, 125, 126, 116, 127, 128	evl1expd 22474	. . . . . . . . . . . . . . . 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 500	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧))
131		cnfldexp 21524	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘))
132	125, 128, 131	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘))
133	130, 132	eqtrd 2804	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘))
134	133	mpteq2dva 5208	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧)) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))
135	123, 134	eqtrd 2804	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) = (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)))
136	135, 120	eqeltrrd 2870	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴))
137	81	subrgmcl 20669	. . . . . . . . . . 11 ⊢ (((𝐸 “ 𝐴) ∈ (SubRing‘(ℂfld ↑s ℂ)) ∧ (ℂ × {(𝑎‘𝑘)}) ∈ (𝐸 “ 𝐴) ∧ (𝑧 ∈ ℂ ↦ (𝑧↑𝑘)) ∈ (𝐸 “ 𝐴)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
138	89, 106, 136, 137	syl3anc 1396	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎‘𝑘)})(.r‘(ℂfld ↑s ℂ))(𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
139	88, 138	eqeltrrd 2870	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
140	139	fmpttd 7111	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))):(0...𝑛)⟶(𝐸 “ 𝐴))
141	36, 8, 139, 40	fsuppmptdm 9336	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘)))) finSupp (0g‘(ℂfld ↑s ℂ)))
142	5, 51, 8, 66, 140, 141	gsumsubmcl 19989	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎‘𝑘) · (𝑧↑𝑘))))) ∈ (𝐸 “ 𝐴))
143	47, 142	eqeltrrd 2870	. . . . . 6 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴))
144		eleq1 2857	. . . . . 6 ⊢ (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → (𝑓 ∈ (𝐸 “ 𝐴) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ∈ (𝐸 “ 𝐴)))
145	143, 144	syl5ibrcom 250	. . . . 5 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0))) → (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴)))
146	145	rexlimdvva 3228	. . . 4 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → 𝑓 ∈ (𝐸 “ 𝐴)))
147	2, 146	syl5 35	. . 3 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) → 𝑓 ∈ (𝐸 “ 𝐴)))
148		ffun 6709	. . . . . 6 ⊢ (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂfld ↑s ℂ)) → Fun 𝐸)
149	95, 148	ax-mp 5	. . . . 5 ⊢ Fun 𝐸
150		fvelima 6947	. . . . 5 ⊢ ((Fun 𝐸 ∧ 𝑓 ∈ (𝐸 “ 𝐴)) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓)
151	149, 150	mpan 702	. . . 4 ⊢ (𝑓 ∈ (𝐸 “ 𝐴) → ∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓)
152	99	sselda 3945	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ (Base‘(Poly1‘ℂfld)))
153		eqid 2769	. . . . . . . . . . . 12 ⊢ ( ·𝑠 ‘(Poly1‘ℂfld)) = ( ·𝑠 ‘(Poly1‘ℂfld))
154		eqid 2769	. . . . . . . . . . . 12 ⊢ (coe1‘𝑎) = (coe1‘𝑎)
155	54, 114, 93, 153, 110, 116, 154	ply1coe 22427	. . . . . . . . . . 11 ⊢ ((ℂfld ∈ Ring ∧ 𝑎 ∈ (Base‘(Poly1‘ℂfld))) → 𝑎 = ((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
156	9, 152, 155	sylancr 598	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑎 = ((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
157	156	fveq2d 6886	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝐸‘((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))))
158		eqid 2769	. . . . . . . . . 10 ⊢ (0g‘(Poly1‘ℂfld)) = (0g‘(Poly1‘ℂfld))
159	54	ply1ring 22376	. . . . . . . . . . . 12 ⊢ (ℂfld ∈ Ring → (Poly1‘ℂfld) ∈ Ring)
160	9, 159	ax-mp 5	. . . . . . . . . . 11 ⊢ (Poly1‘ℂfld) ∈ Ring
161		ringcmn 20365	. . . . . . . . . . 11 ⊢ ((Poly1‘ℂfld) ∈ Ring → (Poly1‘ℂfld) ∈ CMnd)
162	160, 161	mp1i 14	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (Poly1‘ℂfld) ∈ CMnd)
163		ringmnd 20325	. . . . . . . . . . 11 ⊢ ((ℂfld ↑s ℂ) ∈ Ring → (ℂfld ↑s ℂ) ∈ Mnd)
164	49, 163	mp1i 14	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (ℂfld ↑s ℂ) ∈ Mnd)
165		nn0ex 12510	. . . . . . . . . . 11 ⊢ ℕ0 ∈ V
166	165	a1i 11	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℕ0 ∈ V)
167		rhmghm 20565	. . . . . . . . . . . 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 19296	. . . . . . . . . . 11 ⊢ (𝐸 ∈ ((Poly1‘ℂfld) GrpHom (ℂfld ↑s ℂ)) → 𝐸 ∈ ((Poly1‘ℂfld) MndHom (ℂfld ↑s ℂ)))
170	168, 169	mp1i 14	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝐸 ∈ ((Poly1‘ℂfld) MndHom (ℂfld ↑s ℂ)))
171	54	ply1lmod 22380	. . . . . . . . . . . . 13 ⊢ (ℂfld ∈ Ring → (Poly1‘ℂfld) ∈ LMod)
172	9, 171	mp1i 14	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (Poly1‘ℂfld) ∈ LMod)
173	12	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑆 ⊆ ℂ)
174		eqid 2769	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝑅) = (Base‘𝑅)
175	154, 59, 58, 174	coe1f 22340	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ 𝐴 → (coe1‘𝑎):ℕ0⟶(Base‘𝑅))
176	57	subrgbas 20666	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 = (Base‘𝑅))
177	176	feq3d 6691	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → ((coe1‘𝑎):ℕ0⟶𝑆 ↔ (coe1‘𝑎):ℕ0⟶(Base‘𝑅)))
178	175, 177	imbitrrid 249	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (𝑎 ∈ 𝐴 → (coe1‘𝑎):ℕ0⟶𝑆))
179	178	imp 411	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎):ℕ0⟶𝑆)
180	179	ffvelcdmda 7080	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝑎)‘𝑘) ∈ 𝑆)
181	173, 180	sseldd 3946	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝑎)‘𝑘) ∈ ℂ)
182	110, 93	mgpbas 20221	. . . . . . . . . . . . 13 ⊢ (Base‘(Poly1‘ℂfld)) = (Base‘(mulGrp‘(Poly1‘ℂfld)))
183	110	ringmgp 20321	. . . . . . . . . . . . . 14 ⊢ ((Poly1‘ℂfld) ∈ Ring → (mulGrp‘(Poly1‘ℂfld)) ∈ Mnd)
184	160, 183	mp1i 14	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (mulGrp‘(Poly1‘ℂfld)) ∈ Mnd)
185		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
186	114, 54, 93	vr1cl 22346	. . . . . . . . . . . . . 14 ⊢ (ℂfld ∈ Ring → (var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)))
187	9, 186	mp1i 14	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)))
188	182, 116, 184, 185, 187	mulgnn0cld 19161	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)))
189	54	ply1sca 22381	. . . . . . . . . . . . . 14 ⊢ (ℂfld ∈ Ring → ℂfld = (Scalar‘(Poly1‘ℂfld)))
190	9, 189	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ℂfld = (Scalar‘(Poly1‘ℂfld))
191	93, 190, 153, 4	lmodvscl 20977	. . . . . . . . . . . 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 1396	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(Poly1‘ℂfld)))
193	192	fmpttd 7111	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℕ0⟶(Base‘(Poly1‘ℂfld)))
194	165	mptex 7222	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ V
195		funmpt 6575	. . . . . . . . . . . . 13 ⊢ Fun (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
196		fvex 6895	. . . . . . . . . . . . 13 ⊢ (0g‘(Poly1‘ℂfld)) ∈ V
197	194, 195, 196	3pm3.2i 1356	. . . . . . . . . . . 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 22342	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → (coe1‘𝑎) finSupp 0)
200	152, 199	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) finSupp 0)
201	200	fsuppimpd 9329	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) ∈ Fin)
202	179	feqmptd 6950	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (coe1‘𝑎) = (𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)))
203	202	oveq1d 7426	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((coe1‘𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)) supp 0))
204		eqimss2 4004	. . . . . . . . . . . . 13 ⊢ (((coe1‘𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)) supp 0) → ((𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)) supp 0) ⊆ ((coe1‘𝑎) supp 0))
205	203, 204	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ ((coe1‘𝑎)‘𝑘)) supp 0) ⊆ ((coe1‘𝑎) supp 0))
206	9, 171	mp1i 14	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (Poly1‘ℂfld) ∈ LMod)
207	93, 190, 153, 17, 158	lmod0vs 20994	. . . . . . . . . . . . 13 ⊢ (((Poly1‘ℂfld) ∈ LMod ∧ 𝑥 ∈ (Base‘(Poly1‘ℂfld))) → (0( ·𝑠 ‘(Poly1‘ℂfld))𝑥) = (0g‘(Poly1‘ℂfld)))
208	206, 207	sylan 591	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (Base‘(Poly1‘ℂfld))) → (0( ·𝑠 ‘(Poly1‘ℂfld))𝑥) = (0g‘(Poly1‘ℂfld)))
209		c0ex 11200	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
210	209	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 0 ∈ V)
211	205, 208, 180, 188, 210	suppssov1 8193	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) supp (0g‘(Poly1‘ℂfld))) ⊆ ((coe1‘𝑎) supp 0))
212		suppssfifsupp 9340	. . . . . . . . . . 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 849	. . . . . . . . . 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 20008	. . . . . . . . 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 7129	. . . . . . . . . . 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 7079	. . . . . . . . . . . . . . . 16 ⊢ ((((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(Poly1‘ℂfld)) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ (Base‘(ℂfld ↑s ℂ)))
220	192, 219	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ (Base‘(ℂfld ↑s ℂ)))
221	3, 4, 67, 217, 218, 220	pwselbas 17542	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℂ⟶ℂ)
222	221	feqmptd 6950	. . . . . . . . . . . . 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 489	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
225	53, 114, 4, 54, 93, 223, 224	evl1vard 22466	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧))
226	185	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0)
227	53, 54, 4, 93, 223, 224, 225, 116, 127, 226	evl1expd 22474	. . . . . . . . . . . . . . . . 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 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧↑𝑘))
229	228	eqeq2d 2780	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧) ↔ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘)))
230	229	anbi2d 641	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧)) ↔ ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘))))
231	227, 230	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧↑𝑘)))
232	181	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((coe1‘𝑎)‘𝑘) ∈ ℂ)
233	53, 54, 4, 93, 223, 224, 231, 232, 153, 80	evl1vsd 22473	. . . . . . . . . . . . . . 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 500	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧) = (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))
235	234	mpteq2dva 5208	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧)) = (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
236	222, 235	eqtrd 2804	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) = (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
237	236	mpteq2dva 5208	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))
238	216, 237	eqtrd 2804	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))
239	238	oveq2d 7427	. . . . . . . . 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 2810	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = ((ℂfld ↑s ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))))
241	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℂ ∈ V)
242	9, 10	mp1i 14	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ℂfld ∈ CMnd)
243	181	adantlr 727	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((coe1‘𝑎)‘𝑘) ∈ ℂ)
244	33	adantll 726	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ)
245	243, 244	mulcld 11229	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
246	245	anasss 471	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
247	165	mptex 7222	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) ∈ V
248		funmpt 6575	. . . . . . . . . . . 12 ⊢ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
249	247, 248, 39	3pm3.2i 1356	. . . . . . . . . . 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 14009	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ∈ Fin)
252		eldifn 4094	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))) → ¬ 𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
253	252	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → ¬ 𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
254	152	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑎 ∈ (Base‘(Poly1‘ℂfld)))
255		eldifi 4093	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))) → 𝑘 ∈ ℕ0)
256	255	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℕ0)
257		eqid 2769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (deg1‘ℂfld) = (deg1‘ℂfld)
258	257, 54, 93, 17, 154	deg1ge 26224	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ (Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0 ∧ ((coe1‘𝑎)‘𝑘) ≠ 0) → 𝑘 ≤ ((deg1‘ℂfld)‘𝑎))
259	258	3expia 1137	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ (Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0) → (((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ ((deg1‘ℂfld)‘𝑎)))
260	254, 256, 259	syl2anc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ ((deg1‘ℂfld)‘𝑎)))
261		0xr 11256	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ*
262	257, 54, 93	deg1xrcl 26208	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → ((deg1‘ℂfld)‘𝑎) ∈ ℝ*)
263	152, 262	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((deg1‘ℂfld)‘𝑎) ∈ ℝ*)
264	263	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → ((deg1‘ℂfld)‘𝑎) ∈ ℝ*)
265		xrmax2 13202	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0 ∈ ℝ* ∧ ((deg1‘ℂfld)‘𝑎) ∈ ℝ*) → ((deg1‘ℂfld)‘𝑎) ≤ if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))
266	261, 264, 265	sylancr 598	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → ((deg1‘ℂfld)‘𝑎) ≤ if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))
267	256	nn0red 12566	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ)
268	267	rexrd 11259	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ*)
269		ifcl 4538	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((deg1‘ℂfld)‘𝑎) ∈ ℝ* ∧ 0 ∈ ℝ*) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℝ*)
270	264, 261, 269	sylancl 597	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℝ*)
271		xrletr 13183	. . . . . . . . . . . . . . . . . . . . . . 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 1396	. . . . . . . . . . . . . . . . . . . . . 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 706	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑘 ≤ ((deg1‘ℂfld)‘𝑎) → 𝑘 ≤ if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
274	260, 273	syld 48	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
275	274, 256	jctild 534	. . . . . . . . . . . . . . . . . . 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 26209	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → ((deg1‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
277	152, 276	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((deg1‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
278		elun 4115	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}) ↔ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((deg1‘ℂfld)‘𝑎) ∈ {-∞}))
279	277, 278	sylib 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((deg1‘ℂfld)‘𝑎) ∈ {-∞}))
280		nn0ge0 12529	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → 0 ≤ ((deg1‘ℂfld)‘𝑎))
281	280	iftrued 4500	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) = ((deg1‘ℂfld)‘𝑎))
282		id 23	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → ((deg1‘ℂfld)‘𝑎) ∈ ℕ0)
283	281, 282	eqeltrd 2869	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
284		mnflt0 13150	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ -∞ < 0
285		mnfxr 11266	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ -∞ ∈ ℝ*
286		xrltnle 11276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*) → (-∞ < 0 ↔ ¬ 0 ≤ -∞))
287	285, 261, 286	mp2an 704	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (-∞ < 0 ↔ ¬ 0 ≤ -∞)
288	284, 287	mpbi 233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ¬ 0 ≤ -∞
289		elsni 4611	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → ((deg1‘ℂfld)‘𝑎) = -∞)
290	289	breq2d 5125	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → (0 ≤ ((deg1‘ℂfld)‘𝑎) ↔ 0 ≤ -∞))
291	288, 290	mtbiri 330	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → ¬ 0 ≤ ((deg1‘ℂfld)‘𝑎))
292	291	iffalsed 4503	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) = 0)
293		0nn0 12519	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ ℕ0
294	292, 293	eqeltrdi 2877	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((deg1‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
295	283, 294	jaoi 870	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((deg1‘ℂfld)‘𝑎) ∈ ℕ0 ∨ ((deg1‘ℂfld)‘𝑎) ∈ {-∞}) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
296	279, 295	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
297	296	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0)
298		fznn0 13647	. . . . . . . . . . . . . . . . . . . 20 ⊢ (if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0) ∈ ℕ0 → (𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ↔ (𝑘 ∈ ℕ0 ∧ 𝑘 ≤ if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))))
299	297, 298	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ↔ (𝑘 ∈ ℕ0 ∧ 𝑘 ≤ if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))))
300	275, 299	sylibrd 262	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) ≠ 0 → 𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))))
301	300	necon1bd 2982	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (¬ 𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) → ((coe1‘𝑎)‘𝑘) = 0))
302	253, 301	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → ((coe1‘𝑎)‘𝑘) = 0)
303	302	oveq1d 7426	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘)))
304	255, 244	sylan2 604	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑧↑𝑘) ∈ ℂ)
305	304	mul02d 11408	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (0 · (𝑧↑𝑘)) = 0)
306	303, 305	eqtrd 2804	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = 0)
307	306	an32s 664	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) ∧ 𝑧 ∈ ℂ) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) = 0)
308	307	mpteq2dva 5208	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ 0))
309		fconstmpt 5724	. . . . . . . . . . . . 13 ⊢ (ℂ × {0}) = (𝑧 ∈ ℂ ↦ 0)
310		ringmnd 20325	. . . . . . . . . . . . . . 15 ⊢ (ℂfld ∈ Ring → ℂfld ∈ Mnd)
311	9, 310	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ℂfld ∈ Mnd
312	3, 17	pws0g 18831	. . . . . . . . . . . . . 14 ⊢ ((ℂfld ∈ Mnd ∧ ℂ ∈ V) → (ℂ × {0}) = (0g‘(ℂfld ↑s ℂ)))
313	311, 6, 312	mp2an 704	. . . . . . . . . . . . 13 ⊢ (ℂ × {0}) = (0g‘(ℂfld ↑s ℂ))
314	309, 313	eqtr3i 2794	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℂ ↦ 0) = (0g‘(ℂfld ↑s ℂ))
315	308, 314	eqtrdi 2820	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) = (0g‘(ℂfld ↑s ℂ)))
316	315, 166	suppss2 8196	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) supp (0g‘(ℂfld ↑s ℂ))) ⊆ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
317		suppssfifsupp 9340	. . . . . . . . . 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 849	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) finSupp (0g‘(ℂfld ↑s ℂ)))
319	3, 4, 5, 241, 166, 242, 246, 318	pwsgsum 20052	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((ℂfld ↑s ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))))
320		fz0ssnn0 13650	. . . . . . . . . . . 12 ⊢ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ⊆ ℕ0
321		resmpt 6040	. . . . . . . . . . . 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 7422	. . . . . . . . . 10 ⊢ (ℂfld Σg ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) = (ℂfld Σg (𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
324	9, 10	mp1i 14	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ℂfld ∈ CMnd)
325	165	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ℕ0 ∈ V)
326	245	fmpttd 7111	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))):ℕ0⟶ℂ)
327	306, 325	suppss2 8196	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) supp 0) ⊆ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))
328	165	mptex 7222	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ V
329		funmpt 6575	. . . . . . . . . . . . . 14 ⊢ Fun (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))
330	328, 329, 209	3pm3.2i 1356	. . . . . . . . . . . . 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 14009	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) ∈ Fin)
333		suppssfifsupp 9340	. . . . . . . . . . . 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 849	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) finSupp 0)
335	4, 17, 324, 325, 326, 327, 334	gsumres 19983	. . . . . . . . . 10 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg ((𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ↾ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)))) = (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))))
336		elfznn0 13648	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0)) → 𝑘 ∈ ℕ0)
337	336, 245	sylan2 604	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))) → (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
338	332, 337	gsumfsum 21553	. . . . . . . . . 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 2828	. . . . . . . . 9 ⊢ (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘)))
340	339	mpteq2dva 5208	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
341	240, 319, 340	3eqtrd 2808	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))))
342	12	adantr 485	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → 𝑆 ⊆ ℂ)
343		elplyr 26327	. . . . . . . 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 1396	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ ((deg1‘ℂfld)‘𝑎), ((deg1‘ℂfld)‘𝑎), 0))(((coe1‘𝑎)‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆))
345	341, 344	eqeltrd 2869	. . . . . 6 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → (𝐸‘𝑎) ∈ (Poly‘𝑆))
346		eleq1 2857	. . . . . 6 ⊢ ((𝐸‘𝑎) = 𝑓 → ((𝐸‘𝑎) ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (Poly‘𝑆)))
347	345, 346	syl5ibcom 248	. . . . 5 ⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐴) → ((𝐸‘𝑎) = 𝑓 → 𝑓 ∈ (Poly‘𝑆)))
348	347	rexlimdva 3172	. . . 4 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (∃𝑎 ∈ 𝐴 (𝐸‘𝑎) = 𝑓 → 𝑓 ∈ (Poly‘𝑆)))
349	151, 348	syl5 35	. . 3 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (𝐸 “ 𝐴) → 𝑓 ∈ (Poly‘𝑆)))
350	147, 349	impbid 215	. 2 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (𝐸 “ 𝐴)))
351	350	eqrdv 2767	1 ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (Poly‘𝑆) = (𝐸 “ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∃wrex 3095  Vcvv 3463   ∖ cdif 3910   ∪ cun 3911   ⊆ wss 3913  ifcif 4492  {csn 4594   class class class wbr 5113   ↦ cmpt 5196   × cxp 5660   ↾ cres 5664   “ cima 5665   ∘ ccom 5666  Fun wfun 6531   Fn wfn 6532  ⟶wf 6533  ‘cfv 6537  (class class class)co 7411   ∘_f cof 7673   supp csupp 8156   ↑_m cmap 8824  Fincfn 8943   finSupp cfsupp 9321  ℂcc 11098  0cc0 11100   · cmul 11105  -∞cmnf 11241  ℝ^*cxr 11242   < clt 11243   ≤ cle 11244  ℕ₀cn0 12504  ...cfz 13535  ↑cexp 14097  Σcsu 15737  Basecbs 17269   ↾_s cress 17290  ._rcmulr 17311  Scalarcsca 17313   ·_𝑠 cvsca 17314  0_gc0g 17492   Σ_g cgsu 17493   ↑_s cpws 17499  Mndcmnd 18792   MndHom cmhm 18839  SubMndcsubmnd 18840  ._gcmg 19133  SubGrpcsubg 19186   GrpHom cghm 19283  CMndccmn 19850  mulGrpcmgp 20216  Ringcrg 20315  CRingccrg 20316   RingHom crh 20551  SubRingcsubrg 20654  LModclmod 20959  ℂ_fldccnfld 21491  algSccascl 21971  var₁cv1 22305  Poly₁cpl1 22306  coe₁cco1 22307  eval₁ce1 22443  deg₁cdg1 26180  Polycply 26310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-inf2 9610  ax-cnex 11156  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176  ax-pre-mulgt0 11177  ax-pre-sup 11178  ax-addf 11179  ax-mulf 11180

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-tp 4599  df-op 4601  df-uni 4877  df-int 4917  df-iun 4962  df-iin 4963  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-se 5616  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7675  df-ofr 7676  df-om 7863  df-1st 7986  df-2nd 7987  df-supp 8157  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-1o 8453  df-2o 8454  df-er 8694  df-map 8826  df-pm 8827  df-ixp 8896  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-fsupp 9322  df-sup 9402  df-oi 9472  df-card 9925  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-sub 11443  df-neg 11444  df-div 11872  df-nn 12234  df-2 12303  df-3 12304  df-4 12305  df-5 12306  df-6 12307  df-7 12308  df-8 12309  df-9 12310  df-n0 12505  df-z 12592  df-dec 12712  df-uz 12863  df-rp 13017  df-fz 13536  df-fzo 13683  df-seq 14038  df-exp 14098  df-hash 14367  df-cj 15150  df-re 15151  df-im 15152  df-sqrt 15286  df-abs 15287  df-clim 15539  df-sum 15738  df-struct 17207  df-sets 17224  df-slot 17242  df-ndx 17254  df-base 17270  df-ress 17291  df-plusg 17323  df-mulr 17324  df-starv 17325  df-sca 17326  df-vsca 17327  df-ip 17328  df-tset 17329  df-ple 17330  df-ds 17332  df-unif 17333  df-hom 17334  df-cco 17335  df-0g 17494  df-gsum 17495  df-prds 17500  df-pws 17502  df-mre 17638  df-mrc 17639  df-acs 17641  df-mgm 18698  df-sgrp 18777  df-mnd 18793  df-mhm 18841  df-submnd 18842  df-grp 19003  df-minusg 19004  df-sbg 19005  df-mulg 19134  df-subg 19189  df-ghm 19284  df-cntz 19387  df-cmn 19852  df-abl 19853  df-mgp 20217  df-rng 20231  df-ur 20264  df-srg 20269  df-ring 20317  df-cring 20318  df-rhm 20554  df-subrng 20631  df-subrg 20655  df-lmod 20961  df-lss 21031  df-lsp 21071  df-cnfld 21492  df-assa 21972  df-asp 21973  df-ascl 21974  df-psr 22028  df-mvr 22029  df-mpl 22030  df-opsr 22032  df-evls 22194  df-evl 22195  df-psr1 22309  df-vr1 22310  df-ply1 22311  df-coe1 22312  df-evl1 22445  df-mdeg 26181  df-deg1 26182  df-ply 26314

This theorem is referenced by: (None)