MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  plypf1 Structured version   Visualization version   GIF version

Theorem plypf1 23717
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 𝑅 = (ℂflds 𝑆)
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.
StepHypRef Expression
1 elply 23700 . . . . 5 (𝑓 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))))
21simprbi 478 . . . 4 (𝑓 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))
3 eqid 2609 . . . . . . . . 9 (ℂflds ℂ) = (ℂflds ℂ)
4 cnfldbas 19520 . . . . . . . . 9 ℂ = (Base‘ℂfld)
5 eqid 2609 . . . . . . . . 9 (0g‘(ℂflds ℂ)) = (0g‘(ℂflds ℂ))
6 cnex 9874 . . . . . . . . . 10 ℂ ∈ V
76a1i 11 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → ℂ ∈ V)
8 fzfid 12592 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → (0...𝑛) ∈ Fin)
9 cnring 19536 . . . . . . . . . 10 fld ∈ Ring
10 ringcmn 18353 . . . . . . . . . 10 (ℂfld ∈ Ring → ℂfld ∈ CMnd)
119, 10mp1i 13 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → ℂfld ∈ CMnd)
124subrgss 18553 . . . . . . . . . . . . 13 (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ⊆ ℂ)
1312ad2antrr 757 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ⊆ ℂ)
14 elmapi 7743 . . . . . . . . . . . . . . 15 (𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
1514ad2antll 760 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
16 subrgsubg 18558 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ∈ (SubGrp‘ℂfld))
17 cnfld0 19538 . . . . . . . . . . . . . . . . . . . 20 0 = (0g‘ℂfld)
1817subg0cl 17374 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ (SubGrp‘ℂfld) → 0 ∈ 𝑆)
1916, 18syl 17 . . . . . . . . . . . . . . . . . 18 (𝑆 ∈ (SubRing‘ℂfld) → 0 ∈ 𝑆)
2019adantr 479 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → 0 ∈ 𝑆)
2120snssd 4280 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → {0} ⊆ 𝑆)
22 ssequn2 3747 . . . . . . . . . . . . . . . 16 ({0} ⊆ 𝑆 ↔ (𝑆 ∪ {0}) = 𝑆)
2321, 22sylib 206 . . . . . . . . . . . . . . 15 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → (𝑆 ∪ {0}) = 𝑆)
2423feq3d 5931 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → (𝑎:ℕ0⟶(𝑆 ∪ {0}) ↔ 𝑎:ℕ0𝑆))
2515, 24mpbid 220 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → 𝑎:ℕ0𝑆)
26 elfznn0 12260 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0)
27 ffvelrn 6250 . . . . . . . . . . . . 13 ((𝑎:ℕ0𝑆𝑘 ∈ ℕ0) → (𝑎𝑘) ∈ 𝑆)
2825, 26, 27syl2an 492 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎𝑘) ∈ 𝑆)
2913, 28sseldd 3568 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎𝑘) ∈ ℂ)
3029adantrl 747 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑎𝑘) ∈ ℂ)
31 simprl 789 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑧 ∈ ℂ)
3226ad2antll 760 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑘 ∈ ℕ0)
33 expcl 12698 . . . . . . . . . . 11 ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑧𝑘) ∈ ℂ)
3431, 32, 33syl2anc 690 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑧𝑘) ∈ ℂ)
3530, 34mulcld 9917 . . . . . . . . 9 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → ((𝑎𝑘) · (𝑧𝑘)) ∈ ℂ)
36 eqid 2609 . . . . . . . . . 10 (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘)))) = (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))
376mptex 6368 . . . . . . . . . . 11 (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))) ∈ V
3837a1i 11 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))) ∈ V)
39 fvex 6098 . . . . . . . . . . 11 (0g‘(ℂflds ℂ)) ∈ V
4039a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → (0g‘(ℂflds ℂ)) ∈ V)
4136, 8, 38, 40fsuppmptdm 8147 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘)))) finSupp (0g‘(ℂflds ℂ)))
423, 4, 5, 7, 8, 11, 35, 41pwsgsum 18150 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → ((ℂflds ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎𝑘) · (𝑧𝑘))))))
43 fzfid 12592 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑧 ∈ ℂ) → (0...𝑛) ∈ Fin)
4435anassrs 677 . . . . . . . . . 10 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑛)) → ((𝑎𝑘) · (𝑧𝑘)) ∈ ℂ)
4543, 44gsumfsum 19581 . . . . . . . . 9 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎𝑘) · (𝑧𝑘)))) = Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))
4645mpteq2dva 4666 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎𝑘) · (𝑧𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))
4742, 46eqtrd 2643 . . . . . . 7 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → ((ℂflds ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))
483pwsring 18387 . . . . . . . . . 10 ((ℂfld ∈ Ring ∧ ℂ ∈ V) → (ℂflds ℂ) ∈ Ring)
499, 6, 48mp2an 703 . . . . . . . . 9 (ℂflds ℂ) ∈ Ring
50 ringcmn 18353 . . . . . . . . 9 ((ℂflds ℂ) ∈ Ring → (ℂflds ℂ) ∈ CMnd)
5149, 50mp1i 13 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → (ℂflds ℂ) ∈ CMnd)
52 cncrng 19535 . . . . . . . . . . 11 fld ∈ CRing
53 plypf1.e . . . . . . . . . . . 12 𝐸 = (eval1‘ℂfld)
54 eqid 2609 . . . . . . . . . . . 12 (Poly1‘ℂfld) = (Poly1‘ℂfld)
5553, 54, 3, 4evl1rhm 19466 . . . . . . . . . . 11 (ℂfld ∈ CRing → 𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂflds ℂ)))
5652, 55ax-mp 5 . . . . . . . . . 10 𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂflds ℂ))
57 plypf1.r . . . . . . . . . . . 12 𝑅 = (ℂflds 𝑆)
58 plypf1.p . . . . . . . . . . . 12 𝑃 = (Poly1𝑅)
59 plypf1.a . . . . . . . . . . . 12 𝐴 = (Base‘𝑃)
6054, 57, 58, 59subrgply1 19373 . . . . . . . . . . 11 (𝑆 ∈ (SubRing‘ℂfld) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
6160adantr 479 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
62 rhmima 18583 . . . . . . . . . 10 ((𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂflds ℂ)) ∧ 𝐴 ∈ (SubRing‘(Poly1‘ℂfld))) → (𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)))
6356, 61, 62sylancr 693 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → (𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)))
64 subrgsubg 18558 . . . . . . . . 9 ((𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)) → (𝐸𝐴) ∈ (SubGrp‘(ℂflds ℂ)))
65 subgsubm 17388 . . . . . . . . 9 ((𝐸𝐴) ∈ (SubGrp‘(ℂflds ℂ)) → (𝐸𝐴) ∈ (SubMnd‘(ℂflds ℂ)))
6663, 64, 653syl 18 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → (𝐸𝐴) ∈ (SubMnd‘(ℂflds ℂ)))
67 eqid 2609 . . . . . . . . . . . 12 (Base‘(ℂflds ℂ)) = (Base‘(ℂflds ℂ))
689a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → ℂfld ∈ Ring)
696a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → ℂ ∈ V)
70 fconst6g 5992 . . . . . . . . . . . . . 14 ((𝑎𝑘) ∈ ℂ → (ℂ × {(𝑎𝑘)}):ℂ⟶ℂ)
7129, 70syl 17 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎𝑘)}):ℂ⟶ℂ)
723, 4, 67pwselbasb 15920 . . . . . . . . . . . . . 14 ((ℂfld ∈ Ring ∧ ℂ ∈ V) → ((ℂ × {(𝑎𝑘)}) ∈ (Base‘(ℂflds ℂ)) ↔ (ℂ × {(𝑎𝑘)}):ℂ⟶ℂ))
739, 6, 72mp2an 703 . . . . . . . . . . . . 13 ((ℂ × {(𝑎𝑘)}) ∈ (Base‘(ℂflds ℂ)) ↔ (ℂ × {(𝑎𝑘)}):ℂ⟶ℂ)
7471, 73sylibr 222 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎𝑘)}) ∈ (Base‘(ℂflds ℂ)))
7534anass1rs 844 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑧𝑘) ∈ ℂ)
76 eqid 2609 . . . . . . . . . . . . . 14 (𝑧 ∈ ℂ ↦ (𝑧𝑘)) = (𝑧 ∈ ℂ ↦ (𝑧𝑘))
7775, 76fmptd 6277 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧𝑘)):ℂ⟶ℂ)
783, 4, 67pwselbasb 15920 . . . . . . . . . . . . . 14 ((ℂfld ∈ Ring ∧ ℂ ∈ V) → ((𝑧 ∈ ℂ ↦ (𝑧𝑘)) ∈ (Base‘(ℂflds ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧𝑘)):ℂ⟶ℂ))
799, 6, 78mp2an 703 . . . . . . . . . . . . 13 ((𝑧 ∈ ℂ ↦ (𝑧𝑘)) ∈ (Base‘(ℂflds ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧𝑘)):ℂ⟶ℂ)
8077, 79sylibr 222 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧𝑘)) ∈ (Base‘(ℂflds ℂ)))
81 cnfldmul 19522 . . . . . . . . . . . 12 · = (.r‘ℂfld)
82 eqid 2609 . . . . . . . . . . . 12 (.r‘(ℂflds ℂ)) = (.r‘(ℂflds ℂ))
833, 67, 68, 69, 74, 80, 81, 82pwsmulrval 15923 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎𝑘)})(.r‘(ℂflds ℂ))(𝑧 ∈ ℂ ↦ (𝑧𝑘))) = ((ℂ × {(𝑎𝑘)}) ∘𝑓 · (𝑧 ∈ ℂ ↦ (𝑧𝑘))))
8429adantr 479 . . . . . . . . . . . 12 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑎𝑘) ∈ ℂ)
85 fconstmpt 5075 . . . . . . . . . . . . 13 (ℂ × {(𝑎𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎𝑘))
8685a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎𝑘)))
87 eqidd 2610 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧𝑘)) = (𝑧 ∈ ℂ ↦ (𝑧𝑘)))
8869, 84, 75, 86, 87offval2 6790 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎𝑘)}) ∘𝑓 · (𝑧 ∈ ℂ ↦ (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))
8983, 88eqtrd 2643 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎𝑘)})(.r‘(ℂflds ℂ))(𝑧 ∈ ℂ ↦ (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))
9063adantr 479 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)))
91 eqid 2609 . . . . . . . . . . . . . 14 (algSc‘(Poly1‘ℂfld)) = (algSc‘(Poly1‘ℂfld))
9253, 54, 4, 91evl1sca 19468 . . . . . . . . . . . . 13 ((ℂfld ∈ CRing ∧ (𝑎𝑘) ∈ ℂ) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘))) = (ℂ × {(𝑎𝑘)}))
9352, 29, 92sylancr 693 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘))) = (ℂ × {(𝑎𝑘)}))
94 eqid 2609 . . . . . . . . . . . . . . . 16 (Base‘(Poly1‘ℂfld)) = (Base‘(Poly1‘ℂfld))
9594, 67rhmf 18498 . . . . . . . . . . . . . . 15 (𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂflds ℂ)) → 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂflds ℂ)))
9656, 95ax-mp 5 . . . . . . . . . . . . . 14 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂflds ℂ))
97 ffn 5944 . . . . . . . . . . . . . 14 (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂflds ℂ)) → 𝐸 Fn (Base‘(Poly1‘ℂfld)))
9896, 97mp1i 13 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐸 Fn (Base‘(Poly1‘ℂfld)))
9994subrgss 18553 . . . . . . . . . . . . . . 15 (𝐴 ∈ (SubRing‘(Poly1‘ℂfld)) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
10060, 99syl 17 . . . . . . . . . . . . . 14 (𝑆 ∈ (SubRing‘ℂfld) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
101100ad2antrr 757 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
102 simpll 785 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ∈ (SubRing‘ℂfld))
10354, 91, 57, 58, 102, 59, 4, 29subrg1asclcl 19400 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘)) ∈ 𝐴 ↔ (𝑎𝑘) ∈ 𝑆))
10428, 103mpbird 245 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → ((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘)) ∈ 𝐴)
105 fnfvima 6378 . . . . . . . . . . . . 13 ((𝐸 Fn (Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆ (Base‘(Poly1‘ℂfld)) ∧ ((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘)) ∈ 𝐴) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘))) ∈ (𝐸𝐴))
10698, 101, 104, 105syl3anc 1317 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘))) ∈ (𝐸𝐴))
10793, 106eqeltrrd 2688 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎𝑘)}) ∈ (𝐸𝐴))
10867subrgss 18553 . . . . . . . . . . . . . . . . 17 ((𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)) → (𝐸𝐴) ⊆ (Base‘(ℂflds ℂ)))
10990, 108syl 17 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸𝐴) ⊆ (Base‘(ℂflds ℂ)))
11060ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
111 eqid 2609 . . . . . . . . . . . . . . . . . . . 20 (mulGrp‘(Poly1‘ℂfld)) = (mulGrp‘(Poly1‘ℂfld))
112111subrgsubm 18565 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ (SubRing‘(Poly1‘ℂfld)) → 𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))))
113110, 112syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))))
11426adantl 480 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑘 ∈ ℕ0)
115 eqid 2609 . . . . . . . . . . . . . . . . . . 19 (var1‘ℂfld) = (var1‘ℂfld)
116115, 102, 57, 58, 59subrgvr1cl 19402 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (var1‘ℂfld) ∈ 𝐴)
117 eqid 2609 . . . . . . . . . . . . . . . . . . 19 (.g‘(mulGrp‘(Poly1‘ℂfld))) = (.g‘(mulGrp‘(Poly1‘ℂfld)))
118117submmulgcl 17357 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))) ∧ 𝑘 ∈ ℕ0 ∧ (var1‘ℂfld) ∈ 𝐴) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
119113, 114, 116, 118syl3anc 1317 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
120 fnfvima 6378 . . . . . . . . . . . . . . . . 17 ((𝐸 Fn (Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆ (Base‘(Poly1‘ℂfld)) ∧ (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (𝐸𝐴))
12198, 101, 119, 120syl3anc 1317 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (𝐸𝐴))
122109, 121sseldd 3568 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(ℂflds ℂ)))
1233, 4, 67, 68, 69, 122pwselbas 15921 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))):ℂ⟶ℂ)
124123feqmptd 6144 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) = (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧)))
12552a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ℂfld ∈ CRing)
126 simpr 475 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
12753, 115, 4, 54, 94, 125, 126evl1vard 19471 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧))
128 eqid 2609 . . . . . . . . . . . . . . . . 17 (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
129114adantr 479 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0)
13053, 54, 4, 94, 125, 126, 127, 117, 128, 129evl1expd 19479 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧)))
131130simprd 477 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧))
132 cnfldexp 19547 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧𝑘))
133126, 129, 132syl2anc 690 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧𝑘))
134131, 133eqtrd 2643 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧𝑘))
135134mpteq2dva 4666 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧)) = (𝑧 ∈ ℂ ↦ (𝑧𝑘)))
136124, 135eqtrd 2643 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) = (𝑧 ∈ ℂ ↦ (𝑧𝑘)))
137136, 121eqeltrrd 2688 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧𝑘)) ∈ (𝐸𝐴))
13882subrgmcl 18564 . . . . . . . . . . 11 (((𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)) ∧ (ℂ × {(𝑎𝑘)}) ∈ (𝐸𝐴) ∧ (𝑧 ∈ ℂ ↦ (𝑧𝑘)) ∈ (𝐸𝐴)) → ((ℂ × {(𝑎𝑘)})(.r‘(ℂflds ℂ))(𝑧 ∈ ℂ ↦ (𝑧𝑘))) ∈ (𝐸𝐴))
13990, 107, 137, 138syl3anc 1317 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎𝑘)})(.r‘(ℂflds ℂ))(𝑧 ∈ ℂ ↦ (𝑧𝑘))) ∈ (𝐸𝐴))
14089, 139eqeltrrd 2688 . . . . . . . . 9 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))) ∈ (𝐸𝐴))
141140, 36fmptd 6277 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘)))):(0...𝑛)⟶(𝐸𝐴))
14236, 8, 140, 40fsuppmptdm 8147 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘)))) finSupp (0g‘(ℂflds ℂ)))
1435, 51, 8, 66, 141, 142gsumsubmcl 18091 . . . . . . 7 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → ((ℂflds ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))) ∈ (𝐸𝐴))
14447, 143eqeltrrd 2688 . . . . . 6 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) ∈ (𝐸𝐴))
145 eleq1 2675 . . . . . 6 (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) → (𝑓 ∈ (𝐸𝐴) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) ∈ (𝐸𝐴)))
146144, 145syl5ibrcom 235 . . . . 5 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0))) → (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) → 𝑓 ∈ (𝐸𝐴)))
147146rexlimdvva 3019 . . . 4 (𝑆 ∈ (SubRing‘ℂfld) → (∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) → 𝑓 ∈ (𝐸𝐴)))
1482, 147syl5 33 . . 3 (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) → 𝑓 ∈ (𝐸𝐴)))
149 ffun 5947 . . . . . 6 (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂflds ℂ)) → Fun 𝐸)
15096, 149ax-mp 5 . . . . 5 Fun 𝐸
151 fvelima 6143 . . . . 5 ((Fun 𝐸𝑓 ∈ (𝐸𝐴)) → ∃𝑎𝐴 (𝐸𝑎) = 𝑓)
152150, 151mpan 701 . . . 4 (𝑓 ∈ (𝐸𝐴) → ∃𝑎𝐴 (𝐸𝑎) = 𝑓)
153100sselda 3567 . . . . . . . . . . 11 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝑎 ∈ (Base‘(Poly1‘ℂfld)))
154 eqid 2609 . . . . . . . . . . . 12 ( ·𝑠 ‘(Poly1‘ℂfld)) = ( ·𝑠 ‘(Poly1‘ℂfld))
155 eqid 2609 . . . . . . . . . . . 12 (coe1𝑎) = (coe1𝑎)
15654, 115, 94, 154, 111, 117, 155ply1coe 19436 . . . . . . . . . . 11 ((ℂfld ∈ Ring ∧ 𝑎 ∈ (Base‘(Poly1‘ℂfld))) → 𝑎 = ((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
1579, 153, 156sylancr 693 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝑎 = ((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
158157fveq2d 6092 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸𝑎) = (𝐸‘((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))))
159 eqid 2609 . . . . . . . . . 10 (0g‘(Poly1‘ℂfld)) = (0g‘(Poly1‘ℂfld))
16054ply1ring 19388 . . . . . . . . . . . 12 (ℂfld ∈ Ring → (Poly1‘ℂfld) ∈ Ring)
1619, 160ax-mp 5 . . . . . . . . . . 11 (Poly1‘ℂfld) ∈ Ring
162 ringcmn 18353 . . . . . . . . . . 11 ((Poly1‘ℂfld) ∈ Ring → (Poly1‘ℂfld) ∈ CMnd)
163161, 162mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (Poly1‘ℂfld) ∈ CMnd)
164 ringmnd 18328 . . . . . . . . . . 11 ((ℂflds ℂ) ∈ Ring → (ℂflds ℂ) ∈ Mnd)
16549, 164mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (ℂflds ℂ) ∈ Mnd)
166 nn0ex 11148 . . . . . . . . . . 11 0 ∈ V
167166a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ℕ0 ∈ V)
168 rhmghm 18497 . . . . . . . . . . . 12 (𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂflds ℂ)) → 𝐸 ∈ ((Poly1‘ℂfld) GrpHom (ℂflds ℂ)))
16956, 168ax-mp 5 . . . . . . . . . . 11 𝐸 ∈ ((Poly1‘ℂfld) GrpHom (ℂflds ℂ))
170 ghmmhm 17442 . . . . . . . . . . 11 (𝐸 ∈ ((Poly1‘ℂfld) GrpHom (ℂflds ℂ)) → 𝐸 ∈ ((Poly1‘ℂfld) MndHom (ℂflds ℂ)))
171169, 170mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝐸 ∈ ((Poly1‘ℂfld) MndHom (ℂflds ℂ)))
17254ply1lmod 19392 . . . . . . . . . . . . 13 (ℂfld ∈ Ring → (Poly1‘ℂfld) ∈ LMod)
1739, 172mp1i 13 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (Poly1‘ℂfld) ∈ LMod)
17412ad2antrr 757 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑆 ⊆ ℂ)
175 eqid 2609 . . . . . . . . . . . . . . . . 17 (Base‘𝑅) = (Base‘𝑅)
176155, 59, 58, 175coe1f 19351 . . . . . . . . . . . . . . . 16 (𝑎𝐴 → (coe1𝑎):ℕ0⟶(Base‘𝑅))
17757subrgbas 18561 . . . . . . . . . . . . . . . . 17 (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 = (Base‘𝑅))
178177feq3d 5931 . . . . . . . . . . . . . . . 16 (𝑆 ∈ (SubRing‘ℂfld) → ((coe1𝑎):ℕ0𝑆 ↔ (coe1𝑎):ℕ0⟶(Base‘𝑅)))
179176, 178syl5ibr 234 . . . . . . . . . . . . . . 15 (𝑆 ∈ (SubRing‘ℂfld) → (𝑎𝐴 → (coe1𝑎):ℕ0𝑆))
180179imp 443 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (coe1𝑎):ℕ0𝑆)
181180ffvelrnda 6252 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1𝑎)‘𝑘) ∈ 𝑆)
182174, 181sseldd 3568 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1𝑎)‘𝑘) ∈ ℂ)
183111ringmgp 18325 . . . . . . . . . . . . . 14 ((Poly1‘ℂfld) ∈ Ring → (mulGrp‘(Poly1‘ℂfld)) ∈ Mnd)
184161, 183mp1i 13 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (mulGrp‘(Poly1‘ℂfld)) ∈ Mnd)
185 simpr 475 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
186115, 54, 94vr1cl 19357 . . . . . . . . . . . . . 14 (ℂfld ∈ Ring → (var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)))
1879, 186mp1i 13 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)))
188111, 94mgpbas 18267 . . . . . . . . . . . . . 14 (Base‘(Poly1‘ℂfld)) = (Base‘(mulGrp‘(Poly1‘ℂfld)))
189188, 117mulgnn0cl 17330 . . . . . . . . . . . . 13 (((mulGrp‘(Poly1‘ℂfld)) ∈ Mnd ∧ 𝑘 ∈ ℕ0 ∧ (var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld))) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)))
190184, 185, 187, 189syl3anc 1317 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)))
19154ply1sca 19393 . . . . . . . . . . . . . 14 (ℂfld ∈ Ring → ℂfld = (Scalar‘(Poly1‘ℂfld)))
1929, 191ax-mp 5 . . . . . . . . . . . . 13 fld = (Scalar‘(Poly1‘ℂfld))
19394, 192, 154, 4lmodvscl 18652 . . . . . . . . . . . 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)))
194173, 182, 190, 193syl3anc 1317 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(Poly1‘ℂfld)))
195 eqid 2609 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) = (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
196194, 195fmptd 6277 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℕ0⟶(Base‘(Poly1‘ℂfld)))
197166mptex 6368 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ V
198 funmpt 5826 . . . . . . . . . . . . 13 Fun (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
199 fvex 6098 . . . . . . . . . . . . 13 (0g‘(Poly1‘ℂfld)) ∈ V
200197, 198, 1993pm3.2i 1231 . . . . . . . . . . . 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)
201200a1i 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))
202155, 94, 54, 17coe1sfi 19353 . . . . . . . . . . . . 13 (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → (coe1𝑎) finSupp 0)
203153, 202syl 17 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (coe1𝑎) finSupp 0)
204203fsuppimpd 8143 . . . . . . . . . . 11 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((coe1𝑎) supp 0) ∈ Fin)
205180feqmptd 6144 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (coe1𝑎) = (𝑘 ∈ ℕ0 ↦ ((coe1𝑎)‘𝑘)))
206205oveq1d 6542 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((coe1𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦ ((coe1𝑎)‘𝑘)) supp 0))
207 eqimss2 3620 . . . . . . . . . . . . 13 (((coe1𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦ ((coe1𝑎)‘𝑘)) supp 0) → ((𝑘 ∈ ℕ0 ↦ ((coe1𝑎)‘𝑘)) supp 0) ⊆ ((coe1𝑎) supp 0))
208206, 207syl 17 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((𝑘 ∈ ℕ0 ↦ ((coe1𝑎)‘𝑘)) supp 0) ⊆ ((coe1𝑎) supp 0))
2099, 172mp1i 13 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (Poly1‘ℂfld) ∈ LMod)
21094, 192, 154, 17, 159lmod0vs 18668 . . . . . . . . . . . . 13 (((Poly1‘ℂfld) ∈ LMod ∧ 𝑥 ∈ (Base‘(Poly1‘ℂfld))) → (0( ·𝑠 ‘(Poly1‘ℂfld))𝑥) = (0g‘(Poly1‘ℂfld)))
211209, 210sylan 486 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑥 ∈ (Base‘(Poly1‘ℂfld))) → (0( ·𝑠 ‘(Poly1‘ℂfld))𝑥) = (0g‘(Poly1‘ℂfld)))
212 c0ex 9891 . . . . . . . . . . . . 13 0 ∈ V
213212a1i 11 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 0 ∈ V)
214208, 211, 181, 190, 213suppssov1 7192 . . . . . . . . . . 11 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) supp (0g‘(Poly1‘ℂfld))) ⊆ ((coe1𝑎) supp 0))
215 suppssfifsupp 8151 . . . . . . . . . . 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)))
216201, 204, 214, 215syl12anc 1315 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) finSupp (0g‘(Poly1‘ℂfld)))
21794, 159, 163, 165, 167, 171, 196, 216gsummhm 18110 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((ℂflds ℂ) Σg (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))) = (𝐸‘((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))))
218 eqidd 2610 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) = (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))
21996a1i 11 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂflds ℂ)))
220219feqmptd 6144 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝐸 = (𝑥 ∈ (Base‘(Poly1‘ℂfld)) ↦ (𝐸𝑥)))
221 fveq2 6088 . . . . . . . . . . . 12 (𝑥 = (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) → (𝐸𝑥) = (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))
222194, 218, 220, 221fmptco 6288 . . . . . . . . . . 11 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
2239a1i 11 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → ℂfld ∈ Ring)
2246a1i 11 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → ℂ ∈ V)
22596ffvelrni 6251 . . . . . . . . . . . . . . . 16 ((((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(Poly1‘ℂfld)) → (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ (Base‘(ℂflds ℂ)))
226194, 225syl 17 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ (Base‘(ℂflds ℂ)))
2273, 4, 67, 223, 224, 226pwselbas 15921 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℂ⟶ℂ)
228227feqmptd 6144 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) = (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧)))
22952a1i 11 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ℂfld ∈ CRing)
230 simpr 475 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
23153, 115, 4, 54, 94, 229, 230evl1vard 19471 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧))
232185adantr 479 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0)
23353, 54, 4, 94, 229, 230, 231, 117, 128, 232evl1expd 19479 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧)))
234230, 232, 132syl2anc 690 . . . . . . . . . . . . . . . . . . 19 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧𝑘))
235234eqeq2d 2619 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧) ↔ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧𝑘)))
236235anbi2d 735 . . . . . . . . . . . . . . . . 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)))‘𝑧) = (𝑧𝑘))))
237233, 236mpbid 220 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧𝑘)))
238182adantr 479 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((coe1𝑎)‘𝑘) ∈ ℂ)
23953, 54, 4, 94, 229, 230, 237, 238, 154, 81evl1vsd 19478 . . . . . . . . . . . . . . 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𝑎)‘𝑘) · (𝑧𝑘))))
240239simprd 477 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧) = (((coe1𝑎)‘𝑘) · (𝑧𝑘)))
241240mpteq2dva 4666 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧)) = (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))
242228, 241eqtrd 2643 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) = (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))
243242mpteq2dva 4666 . . . . . . . . . . 11 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))))
244222, 243eqtrd 2643 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))))
245244oveq2d 6543 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((ℂflds ℂ) Σg (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))) = ((ℂflds ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))))
246158, 217, 2453eqtr2d 2649 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸𝑎) = ((ℂflds ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))))
2476a1i 11 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ℂ ∈ V)
2489, 10mp1i 13 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ℂfld ∈ CMnd)
249182adantlr 746 . . . . . . . . . . 11 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((coe1𝑎)‘𝑘) ∈ ℂ)
25033adantll 745 . . . . . . . . . . 11 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧𝑘) ∈ ℂ)
251249, 250mulcld 9917 . . . . . . . . . 10 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) ∈ ℂ)
252251anasss 676 . . . . . . . . 9 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) ∈ ℂ)
253166mptex 6368 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∈ V
254 funmpt 5826 . . . . . . . . . . . 12 Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))
255253, 254, 393pm3.2i 1231 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∧ (0g‘(ℂflds ℂ)) ∈ V)
256255a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∧ (0g‘(ℂflds ℂ)) ∈ V))
257 fzfid 12592 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ∈ Fin)
258 eldifn 3694 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))) → ¬ 𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
259258adantl 480 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → ¬ 𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
260153ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → 𝑎 ∈ (Base‘(Poly1‘ℂfld)))
261 eldifi 3693 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))) → 𝑘 ∈ ℕ0)
262261adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℕ0)
263 eqid 2609 . . . . . . . . . . . . . . . . . . . . . . . 24 ( deg1 ‘ℂfld) = ( deg1 ‘ℂfld)
264263, 54, 94, 17, 155deg1ge 23607 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎 ∈ (Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0 ∧ ((coe1𝑎)‘𝑘) ≠ 0) → 𝑘 ≤ (( deg1 ‘ℂfld)‘𝑎))
2652643expia 1258 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ (Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0) → (((coe1𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ (( deg1 ‘ℂfld)‘𝑎)))
266260, 262, 265syl2anc 690 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ (( deg1 ‘ℂfld)‘𝑎)))
267 0xr 9943 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℝ*
268263, 54, 94deg1xrcl 23591 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → (( deg1 ‘ℂfld)‘𝑎) ∈ ℝ*)
269153, 268syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (( deg1 ‘ℂfld)‘𝑎) ∈ ℝ*)
270269ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (( deg1 ‘ℂfld)‘𝑎) ∈ ℝ*)
271 xrmax2 11843 . . . . . . . . . . . . . . . . . . . . . . 23 ((0 ∈ ℝ* ∧ (( deg1 ‘ℂfld)‘𝑎) ∈ ℝ*) → (( deg1 ‘ℂfld)‘𝑎) ≤ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))
272267, 270, 271sylancr 693 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (( deg1 ‘ℂfld)‘𝑎) ≤ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))
273262nn0red 11202 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ)
274273rexrd 9946 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ*)
275 ifcl 4079 . . . . . . . . . . . . . . . . . . . . . . . 24 (((( deg1 ‘ℂfld)‘𝑎) ∈ ℝ* ∧ 0 ∈ ℝ*) → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℝ*)
276270, 267, 275sylancl 692 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℝ*)
277 xrletr 11827 . . . . . . . . . . . . . . . . . . . . . . 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)))
278274, 270, 276, 277syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . 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)))
279272, 278mpan2d 705 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (𝑘 ≤ (( deg1 ‘ℂfld)‘𝑎) → 𝑘 ≤ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
280266, 279syld 45 . . . . . . . . . . . . . . . . . . . 20 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
281280, 262jctild 563 . . . . . . . . . . . . . . . . . . 19 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) ≠ 0 → (𝑘 ∈ ℕ0𝑘 ≤ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))))
282263, 54, 94deg1cl 23592 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → (( deg1 ‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
283153, 282syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (( deg1 ‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
284 elun 3714 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 ‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}) ↔ ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 ∨ (( deg1 ‘ℂfld)‘𝑎) ∈ {-∞}))
285283, 284sylib 206 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 ∨ (( deg1 ‘ℂfld)‘𝑎) ∈ {-∞}))
286 nn0ge0 11168 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → 0 ≤ (( deg1 ‘ℂfld)‘𝑎))
287286iftrued 4043 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) = (( deg1 ‘ℂfld)‘𝑎))
288 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → (( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0)
289287, 288eqeltrd 2687 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0)
290 mnflt0 11799 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -∞ < 0
291 mnfxr 11786 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 -∞ ∈ ℝ*
292 xrltnle 9957 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*) → (-∞ < 0 ↔ ¬ 0 ≤ -∞))
293291, 267, 292mp2an 703 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (-∞ < 0 ↔ ¬ 0 ≤ -∞)
294290, 293mpbi 218 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ¬ 0 ≤ -∞
295 elsni 4141 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((( deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → (( deg1 ‘ℂfld)‘𝑎) = -∞)
296295breq2d 4589 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → (0 ≤ (( deg1 ‘ℂfld)‘𝑎) ↔ 0 ≤ -∞))
297294, 296mtbiri 315 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → ¬ 0 ≤ (( deg1 ‘ℂfld)‘𝑎))
298297iffalsed 4046 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) = 0)
299 0nn0 11157 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ ℕ0
300298, 299syl6eqel 2695 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0)
301289, 300jaoi 392 . . . . . . . . . . . . . . . . . . . . . 22 (((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 ∨ (( deg1 ‘ℂfld)‘𝑎) ∈ {-∞}) → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0)
302285, 301syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0)
303302ad2antrr 757 . . . . . . . . . . . . . . . . . . . 20 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0)
304 fznn0 12259 . . . . . . . . . . . . . . . . . . . 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))))
305303, 304syl 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))))
306281, 305sylibrd 247 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) ≠ 0 → 𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))))
307306necon1bd 2799 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (¬ 𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) → ((coe1𝑎)‘𝑘) = 0))
308259, 307mpd 15 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → ((coe1𝑎)‘𝑘) = 0)
309308oveq1d 6542 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) = (0 · (𝑧𝑘)))
310261, 250sylan2 489 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (𝑧𝑘) ∈ ℂ)
311310mul02d 10086 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (0 · (𝑧𝑘)) = 0)
312309, 311eqtrd 2643 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) = 0)
313312an32s 841 . . . . . . . . . . . . 13 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) ∧ 𝑧 ∈ ℂ) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) = 0)
314313mpteq2dva 4666 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ 0))
315 fconstmpt 5075 . . . . . . . . . . . . 13 (ℂ × {0}) = (𝑧 ∈ ℂ ↦ 0)
316 ringmnd 18328 . . . . . . . . . . . . . . 15 (ℂfld ∈ Ring → ℂfld ∈ Mnd)
3179, 316ax-mp 5 . . . . . . . . . . . . . 14 fld ∈ Mnd
3183, 17pws0g 17098 . . . . . . . . . . . . . 14 ((ℂfld ∈ Mnd ∧ ℂ ∈ V) → (ℂ × {0}) = (0g‘(ℂflds ℂ)))
319317, 6, 318mp2an 703 . . . . . . . . . . . . 13 (ℂ × {0}) = (0g‘(ℂflds ℂ))
320315, 319eqtr3i 2633 . . . . . . . . . . . 12 (𝑧 ∈ ℂ ↦ 0) = (0g‘(ℂflds ℂ))
321314, 320syl6eq 2659 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) = (0g‘(ℂflds ℂ)))
322321, 167suppss2 7194 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) supp (0g‘(ℂflds ℂ))) ⊆ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
323 suppssfifsupp 8151 . . . . . . . . . 10 ((((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∧ (0g‘(ℂflds ℂ)) ∈ V) ∧ ((0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ∈ Fin ∧ ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) supp (0g‘(ℂflds ℂ))) ⊆ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) finSupp (0g‘(ℂflds ℂ)))
324256, 257, 322, 323syl12anc 1315 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) finSupp (0g‘(ℂflds ℂ)))
3253, 4, 5, 247, 167, 248, 252, 324pwsgsum 18150 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((ℂflds ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))))
326 fz0ssnn0 12262 . . . . . . . . . . . 12 (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ⊆ ℕ0
327 resmpt 5356 . . . . . . . . . . . 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𝑎)‘𝑘) · (𝑧𝑘))))
328326, 327ax-mp 5 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ↾ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))) = (𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))
329328oveq2i 6538 . . . . . . . . . 10 (ℂfld Σg ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ↾ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) = (ℂfld Σg (𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))
3309, 10mp1i 13 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → ℂfld ∈ CMnd)
331166a1i 11 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → ℕ0 ∈ V)
332 eqid 2609 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) = (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))
333251, 332fmptd 6277 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))):ℕ0⟶ℂ)
334312, 331suppss2 7194 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) supp 0) ⊆ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
335166mptex 6368 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∈ V
336 funmpt 5826 . . . . . . . . . . . . . 14 Fun (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))
337335, 336, 2123pm3.2i 1231 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∧ 0 ∈ V)
338337a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∧ 0 ∈ V))
339 fzfid 12592 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ∈ Fin)
340 suppssfifsupp 8151 . . . . . . . . . . . 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)
341338, 339, 334, 340syl12anc 1315 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) finSupp 0)
3424, 17, 330, 331, 333, 334, 341gsumres 18086 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ↾ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) = (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))))
343 elfznn0 12260 . . . . . . . . . . . 12 (𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) → 𝑘 ∈ ℕ0)
344343, 251sylan2 489 . . . . . . . . . . 11 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) ∈ ℂ)
345339, 344gsumfsum 19581 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘)))
346329, 342, 3453eqtr3a 2667 . . . . . . . . 9 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘)))
347346mpteq2dva 4666 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘))))
348246, 325, 3473eqtrd 2647 . . . . . . 7 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸𝑎) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘))))
34912adantr 479 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝑆 ⊆ ℂ)
350 elplyr 23706 . . . . . . . 8 ((𝑆 ⊆ ℂ ∧ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0 ∧ (coe1𝑎):ℕ0𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∈ (Poly‘𝑆))
351349, 302, 180, 350syl3anc 1317 . . . . . . 7 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∈ (Poly‘𝑆))
352348, 351eqeltrd 2687 . . . . . 6 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸𝑎) ∈ (Poly‘𝑆))
353 eleq1 2675 . . . . . 6 ((𝐸𝑎) = 𝑓 → ((𝐸𝑎) ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (Poly‘𝑆)))
354352, 353syl5ibcom 233 . . . . 5 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((𝐸𝑎) = 𝑓𝑓 ∈ (Poly‘𝑆)))
355354rexlimdva 3012 . . . 4 (𝑆 ∈ (SubRing‘ℂfld) → (∃𝑎𝐴 (𝐸𝑎) = 𝑓𝑓 ∈ (Poly‘𝑆)))
356152, 355syl5 33 . . 3 (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (𝐸𝐴) → 𝑓 ∈ (Poly‘𝑆)))
357148, 356impbid 200 . 2 (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (𝐸𝐴)))
358357eqrdv 2607 1 (𝑆 ∈ (SubRing‘ℂfld) → (Poly‘𝑆) = (𝐸𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wrex 2896  Vcvv 3172  cdif 3536  cun 3537  wss 3539  ifcif 4035  {csn 4124   class class class wbr 4577  cmpt 4637   × cxp 5026  cres 5030  cima 5031  ccom 5032  Fun wfun 5784   Fn wfn 5785  wf 5786  cfv 5790  (class class class)co 6527  𝑓 cof 6771   supp csupp 7160  𝑚 cmap 7722  Fincfn 7819   finSupp cfsupp 8136  cc 9791  0cc0 9793   · cmul 9798  -∞cmnf 9929  *cxr 9930   < clt 9931  cle 9932  0cn0 11142  ...cfz 12155  cexp 12680  Σcsu 14213  Basecbs 15644  s cress 15645  .rcmulr 15718  Scalarcsca 15720   ·𝑠 cvsca 15721  0gc0g 15872   Σg cgsu 15873  s cpws 15879  Mndcmnd 17066   MndHom cmhm 17105  SubMndcsubmnd 17106  .gcmg 17312  SubGrpcsubg 17360   GrpHom cghm 17429  CMndccmn 17965  mulGrpcmgp 18261  Ringcrg 18319  CRingccrg 18320   RingHom crh 18484  SubRingcsubrg 18548  LModclmod 18635  algSccascl 19081  var1cv1 19316  Poly1cpl1 19317  coe1cco1 19318  eval1ce1 19449  fldccnfld 19516   deg1 cdg1 23563  Polycply 23689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871  ax-addf 9872  ax-mulf 9873
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-ofr 6774  df-om 6936  df-1st 7037  df-2nd 7038  df-supp 7161  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-map 7724  df-pm 7725  df-ixp 7773  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fsupp 8137  df-sup 8209  df-oi 8276  df-card 8626  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-4 10931  df-5 10932  df-6 10933  df-7 10934  df-8 10935  df-9 10936  df-n0 11143  df-z 11214  df-dec 11329  df-uz 11523  df-rp 11668  df-fz 12156  df-fzo 12293  df-seq 12622  df-exp 12681  df-hash 12938  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-clim 14016  df-sum 14214  df-struct 15646  df-ndx 15647  df-slot 15648  df-base 15649  df-sets 15650  df-ress 15651  df-plusg 15730  df-mulr 15731  df-starv 15732  df-sca 15733  df-vsca 15734  df-ip 15735  df-tset 15736  df-ple 15737  df-ds 15740  df-unif 15741  df-hom 15742  df-cco 15743  df-0g 15874  df-gsum 15875  df-prds 15880  df-pws 15882  df-mre 16018  df-mrc 16019  df-acs 16021  df-mgm 17014  df-sgrp 17056  df-mnd 17067  df-mhm 17107  df-submnd 17108  df-grp 17197  df-minusg 17198  df-sbg 17199  df-mulg 17313  df-subg 17363  df-ghm 17430  df-cntz 17522  df-cmn 17967  df-abl 17968  df-mgp 18262  df-ur 18274  df-srg 18278  df-ring 18321  df-cring 18322  df-rnghom 18487  df-subrg 18550  df-lmod 18637  df-lss 18703  df-lsp 18742  df-assa 19082  df-asp 19083  df-ascl 19084  df-psr 19126  df-mvr 19127  df-mpl 19128  df-opsr 19130  df-evls 19276  df-evl 19277  df-psr1 19320  df-vr1 19321  df-ply1 19322  df-coe1 19323  df-evl1 19451  df-cnfld 19517  df-mdeg 23564  df-deg1 23565  df-ply 23693
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator