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

Theorem plypf1 25573
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 25556 . . . . 5 (𝑓 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))))
21simprbi 497 . . . 4 (𝑓 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))
3 eqid 2736 . . . . . . . . 9 (ℂflds ℂ) = (ℂflds ℂ)
4 cnfldbas 20800 . . . . . . . . 9 ℂ = (Base‘ℂfld)
5 eqid 2736 . . . . . . . . 9 (0g‘(ℂflds ℂ)) = (0g‘(ℂflds ℂ))
6 cnex 11132 . . . . . . . . . 10 ℂ ∈ V
76a1i 11 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → ℂ ∈ V)
8 fzfid 13878 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (0...𝑛) ∈ Fin)
9 cnring 20819 . . . . . . . . . 10 fld ∈ Ring
10 ringcmn 20003 . . . . . . . . . 10 (ℂfld ∈ Ring → ℂfld ∈ CMnd)
119, 10mp1i 13 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → ℂfld ∈ CMnd)
124subrgss 20223 . . . . . . . . . . . . 13 (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ⊆ ℂ)
1312ad2antrr 724 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ⊆ ℂ)
14 elmapi 8787 . . . . . . . . . . . . . . 15 (𝑎 ∈ ((𝑆 ∪ {0}) ↑m0) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
1514ad2antll 727 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
16 subrgsubg 20228 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ∈ (SubGrp‘ℂfld))
17 cnfld0 20821 . . . . . . . . . . . . . . . . . . . 20 0 = (0g‘ℂfld)
1817subg0cl 18936 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ (SubGrp‘ℂfld) → 0 ∈ 𝑆)
1916, 18syl 17 . . . . . . . . . . . . . . . . . 18 (𝑆 ∈ (SubRing‘ℂfld) → 0 ∈ 𝑆)
2019adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → 0 ∈ 𝑆)
2120snssd 4769 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → {0} ⊆ 𝑆)
22 ssequn2 4143 . . . . . . . . . . . . . . . 16 ({0} ⊆ 𝑆 ↔ (𝑆 ∪ {0}) = 𝑆)
2321, 22sylib 217 . . . . . . . . . . . . . . 15 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑆 ∪ {0}) = 𝑆)
2423feq3d 6655 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑎:ℕ0⟶(𝑆 ∪ {0}) ↔ 𝑎:ℕ0𝑆))
2515, 24mpbid 231 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → 𝑎:ℕ0𝑆)
26 elfznn0 13534 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0)
27 ffvelcdm 7032 . . . . . . . . . . . . 13 ((𝑎:ℕ0𝑆𝑘 ∈ ℕ0) → (𝑎𝑘) ∈ 𝑆)
2825, 26, 27syl2an 596 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎𝑘) ∈ 𝑆)
2913, 28sseldd 3945 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎𝑘) ∈ ℂ)
3029adantrl 714 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑎𝑘) ∈ ℂ)
31 simprl 769 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑧 ∈ ℂ)
3226ad2antll 727 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑘 ∈ ℕ0)
33 expcl 13985 . . . . . . . . . . 11 ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑧𝑘) ∈ ℂ)
3431, 32, 33syl2anc 584 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑧𝑘) ∈ ℂ)
3530, 34mulcld 11175 . . . . . . . . 9 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → ((𝑎𝑘) · (𝑧𝑘)) ∈ ℂ)
36 eqid 2736 . . . . . . . . . 10 (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘)))) = (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))
376mptex 7173 . . . . . . . . . . 11 (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))) ∈ V
3837a1i 11 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))) ∈ V)
39 fvex 6855 . . . . . . . . . . 11 (0g‘(ℂflds ℂ)) ∈ V
4039a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (0g‘(ℂflds ℂ)) ∈ V)
4136, 8, 38, 40fsuppmptdm 9316 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘)))) finSupp (0g‘(ℂflds ℂ)))
423, 4, 5, 7, 8, 11, 35, 41pwsgsum 19759 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → ((ℂflds ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎𝑘) · (𝑧𝑘))))))
43 fzfid 13878 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑧 ∈ ℂ) → (0...𝑛) ∈ Fin)
4435anassrs 468 . . . . . . . . . 10 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑛)) → ((𝑎𝑘) · (𝑧𝑘)) ∈ ℂ)
4543, 44gsumfsum 20864 . . . . . . . . 9 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎𝑘) · (𝑧𝑘)))) = Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))
4645mpteq2dva 5205 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎𝑘) · (𝑧𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))
4742, 46eqtrd 2776 . . . . . . 7 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → ((ℂflds ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))
483pwsring 20039 . . . . . . . . . 10 ((ℂfld ∈ Ring ∧ ℂ ∈ V) → (ℂflds ℂ) ∈ Ring)
499, 6, 48mp2an 690 . . . . . . . . 9 (ℂflds ℂ) ∈ Ring
50 ringcmn 20003 . . . . . . . . 9 ((ℂflds ℂ) ∈ Ring → (ℂflds ℂ) ∈ CMnd)
5149, 50mp1i 13 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (ℂflds ℂ) ∈ CMnd)
52 cncrng 20818 . . . . . . . . . . 11 fld ∈ CRing
53 plypf1.e . . . . . . . . . . . 12 𝐸 = (eval1‘ℂfld)
54 eqid 2736 . . . . . . . . . . . 12 (Poly1‘ℂfld) = (Poly1‘ℂfld)
5553, 54, 3, 4evl1rhm 21698 . . . . . . . . . . 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 21604 . . . . . . . . . . 11 (𝑆 ∈ (SubRing‘ℂfld) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
6160adantr 481 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
62 rhmima 20253 . . . . . . . . . 10 ((𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂflds ℂ)) ∧ 𝐴 ∈ (SubRing‘(Poly1‘ℂfld))) → (𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)))
6356, 61, 62sylancr 587 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)))
64 subrgsubg 20228 . . . . . . . . 9 ((𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)) → (𝐸𝐴) ∈ (SubGrp‘(ℂflds ℂ)))
65 subgsubm 18950 . . . . . . . . 9 ((𝐸𝐴) ∈ (SubGrp‘(ℂflds ℂ)) → (𝐸𝐴) ∈ (SubMnd‘(ℂflds ℂ)))
6663, 64, 653syl 18 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝐸𝐴) ∈ (SubMnd‘(ℂflds ℂ)))
67 eqid 2736 . . . . . . . . . . . 12 (Base‘(ℂflds ℂ)) = (Base‘(ℂflds ℂ))
689a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → ℂfld ∈ Ring)
696a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → ℂ ∈ V)
70 fconst6g 6731 . . . . . . . . . . . . . 14 ((𝑎𝑘) ∈ ℂ → (ℂ × {(𝑎𝑘)}):ℂ⟶ℂ)
7129, 70syl 17 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎𝑘)}):ℂ⟶ℂ)
723, 4, 67pwselbasb 17370 . . . . . . . . . . . . . 14 ((ℂfld ∈ Ring ∧ ℂ ∈ V) → ((ℂ × {(𝑎𝑘)}) ∈ (Base‘(ℂflds ℂ)) ↔ (ℂ × {(𝑎𝑘)}):ℂ⟶ℂ))
739, 6, 72mp2an 690 . . . . . . . . . . . . 13 ((ℂ × {(𝑎𝑘)}) ∈ (Base‘(ℂflds ℂ)) ↔ (ℂ × {(𝑎𝑘)}):ℂ⟶ℂ)
7471, 73sylibr 233 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎𝑘)}) ∈ (Base‘(ℂflds ℂ)))
7534anass1rs 653 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑧𝑘) ∈ ℂ)
7675fmpttd 7063 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧𝑘)):ℂ⟶ℂ)
773, 4, 67pwselbasb 17370 . . . . . . . . . . . . . 14 ((ℂfld ∈ Ring ∧ ℂ ∈ V) → ((𝑧 ∈ ℂ ↦ (𝑧𝑘)) ∈ (Base‘(ℂflds ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧𝑘)):ℂ⟶ℂ))
789, 6, 77mp2an 690 . . . . . . . . . . . . 13 ((𝑧 ∈ ℂ ↦ (𝑧𝑘)) ∈ (Base‘(ℂflds ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧𝑘)):ℂ⟶ℂ)
7976, 78sylibr 233 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧𝑘)) ∈ (Base‘(ℂflds ℂ)))
80 cnfldmul 20802 . . . . . . . . . . . 12 · = (.r‘ℂfld)
81 eqid 2736 . . . . . . . . . . . 12 (.r‘(ℂflds ℂ)) = (.r‘(ℂflds ℂ))
823, 67, 68, 69, 74, 79, 80, 81pwsmulrval 17373 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎𝑘)})(.r‘(ℂflds ℂ))(𝑧 ∈ ℂ ↦ (𝑧𝑘))) = ((ℂ × {(𝑎𝑘)}) ∘f · (𝑧 ∈ ℂ ↦ (𝑧𝑘))))
8329adantr 481 . . . . . . . . . . . 12 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑎𝑘) ∈ ℂ)
84 fconstmpt 5694 . . . . . . . . . . . . 13 (ℂ × {(𝑎𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎𝑘))
8584a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎𝑘)))
86 eqidd 2737 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧𝑘)) = (𝑧 ∈ ℂ ↦ (𝑧𝑘)))
8769, 83, 75, 85, 86offval2 7637 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎𝑘)}) ∘f · (𝑧 ∈ ℂ ↦ (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))
8882, 87eqtrd 2776 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎𝑘)})(.r‘(ℂflds ℂ))(𝑧 ∈ ℂ ↦ (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))
8963adantr 481 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)))
90 eqid 2736 . . . . . . . . . . . . . 14 (algSc‘(Poly1‘ℂfld)) = (algSc‘(Poly1‘ℂfld))
9153, 54, 4, 90evl1sca 21700 . . . . . . . . . . . . 13 ((ℂfld ∈ CRing ∧ (𝑎𝑘) ∈ ℂ) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘))) = (ℂ × {(𝑎𝑘)}))
9252, 29, 91sylancr 587 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘))) = (ℂ × {(𝑎𝑘)}))
93 eqid 2736 . . . . . . . . . . . . . . . 16 (Base‘(Poly1‘ℂfld)) = (Base‘(Poly1‘ℂfld))
9493, 67rhmf 20158 . . . . . . . . . . . . . . 15 (𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂflds ℂ)) → 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂflds ℂ)))
9556, 94ax-mp 5 . . . . . . . . . . . . . 14 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂflds ℂ))
96 ffn 6668 . . . . . . . . . . . . . 14 (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂflds ℂ)) → 𝐸 Fn (Base‘(Poly1‘ℂfld)))
9795, 96mp1i 13 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐸 Fn (Base‘(Poly1‘ℂfld)))
9893subrgss 20223 . . . . . . . . . . . . . . 15 (𝐴 ∈ (SubRing‘(Poly1‘ℂfld)) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
9960, 98syl 17 . . . . . . . . . . . . . 14 (𝑆 ∈ (SubRing‘ℂfld) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
10099ad2antrr 724 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
101 simpll 765 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ∈ (SubRing‘ℂfld))
10254, 90, 57, 58, 101, 59, 4, 29subrg1asclcl 21631 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘)) ∈ 𝐴 ↔ (𝑎𝑘) ∈ 𝑆))
10328, 102mpbird 256 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → ((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘)) ∈ 𝐴)
104 fnfvima 7183 . . . . . . . . . . . . 13 ((𝐸 Fn (Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆ (Base‘(Poly1‘ℂfld)) ∧ ((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘)) ∈ 𝐴) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘))) ∈ (𝐸𝐴))
10597, 100, 103, 104syl3anc 1371 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘))) ∈ (𝐸𝐴))
10692, 105eqeltrrd 2839 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎𝑘)}) ∈ (𝐸𝐴))
10767subrgss 20223 . . . . . . . . . . . . . . . . 17 ((𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)) → (𝐸𝐴) ⊆ (Base‘(ℂflds ℂ)))
10889, 107syl 17 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸𝐴) ⊆ (Base‘(ℂflds ℂ)))
10960ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
110 eqid 2736 . . . . . . . . . . . . . . . . . . . 20 (mulGrp‘(Poly1‘ℂfld)) = (mulGrp‘(Poly1‘ℂfld))
111110subrgsubm 20235 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ (SubRing‘(Poly1‘ℂfld)) → 𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))))
112109, 111syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))))
11326adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑘 ∈ ℕ0)
114 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (var1‘ℂfld) = (var1‘ℂfld)
115114, 101, 57, 58, 59subrgvr1cl 21633 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (var1‘ℂfld) ∈ 𝐴)
116 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (.g‘(mulGrp‘(Poly1‘ℂfld))) = (.g‘(mulGrp‘(Poly1‘ℂfld)))
117116submmulgcl 18919 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))) ∧ 𝑘 ∈ ℕ0 ∧ (var1‘ℂfld) ∈ 𝐴) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
118112, 113, 115, 117syl3anc 1371 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
119 fnfvima 7183 . . . . . . . . . . . . . . . . 17 ((𝐸 Fn (Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆ (Base‘(Poly1‘ℂfld)) ∧ (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (𝐸𝐴))
12097, 100, 118, 119syl3anc 1371 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (𝐸𝐴))
121108, 120sseldd 3945 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(ℂflds ℂ)))
1223, 4, 67, 68, 69, 121pwselbas 17371 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))):ℂ⟶ℂ)
123122feqmptd 6910 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) = (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧)))
12452a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ℂfld ∈ CRing)
125 simpr 485 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
12653, 114, 4, 54, 93, 124, 125evl1vard 21703 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧))
127 eqid 2736 . . . . . . . . . . . . . . . . 17 (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
128113adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0)
12953, 54, 4, 93, 124, 125, 126, 116, 127, 128evl1expd 21711 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧)))
130129simprd 496 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧))
131 cnfldexp 20830 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧𝑘))
132125, 128, 131syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧𝑘))
133130, 132eqtrd 2776 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧𝑘))
134133mpteq2dva 5205 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧)) = (𝑧 ∈ ℂ ↦ (𝑧𝑘)))
135123, 134eqtrd 2776 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) = (𝑧 ∈ ℂ ↦ (𝑧𝑘)))
136135, 120eqeltrrd 2839 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧𝑘)) ∈ (𝐸𝐴))
13781subrgmcl 20234 . . . . . . . . . . 11 (((𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)) ∧ (ℂ × {(𝑎𝑘)}) ∈ (𝐸𝐴) ∧ (𝑧 ∈ ℂ ↦ (𝑧𝑘)) ∈ (𝐸𝐴)) → ((ℂ × {(𝑎𝑘)})(.r‘(ℂflds ℂ))(𝑧 ∈ ℂ ↦ (𝑧𝑘))) ∈ (𝐸𝐴))
13889, 106, 136, 137syl3anc 1371 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎𝑘)})(.r‘(ℂflds ℂ))(𝑧 ∈ ℂ ↦ (𝑧𝑘))) ∈ (𝐸𝐴))
13988, 138eqeltrrd 2839 . . . . . . . . 9 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))) ∈ (𝐸𝐴))
140139fmpttd 7063 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘)))):(0...𝑛)⟶(𝐸𝐴))
14136, 8, 139, 40fsuppmptdm 9316 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘)))) finSupp (0g‘(ℂflds ℂ)))
1425, 51, 8, 66, 140, 141gsumsubmcl 19696 . . . . . . 7 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → ((ℂflds ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))) ∈ (𝐸𝐴))
14347, 142eqeltrrd 2839 . . . . . 6 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) ∈ (𝐸𝐴))
144 eleq1 2825 . . . . . 6 (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) → (𝑓 ∈ (𝐸𝐴) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) ∈ (𝐸𝐴)))
145143, 144syl5ibrcom 246 . . . . 5 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) → 𝑓 ∈ (𝐸𝐴)))
146145rexlimdvva 3205 . . . 4 (𝑆 ∈ (SubRing‘ℂfld) → (∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) → 𝑓 ∈ (𝐸𝐴)))
1472, 146syl5 34 . . 3 (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) → 𝑓 ∈ (𝐸𝐴)))
148 ffun 6671 . . . . . 6 (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂflds ℂ)) → Fun 𝐸)
14995, 148ax-mp 5 . . . . 5 Fun 𝐸
150 fvelima 6908 . . . . 5 ((Fun 𝐸𝑓 ∈ (𝐸𝐴)) → ∃𝑎𝐴 (𝐸𝑎) = 𝑓)
151149, 150mpan 688 . . . 4 (𝑓 ∈ (𝐸𝐴) → ∃𝑎𝐴 (𝐸𝑎) = 𝑓)
15299sselda 3944 . . . . . . . . . . 11 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝑎 ∈ (Base‘(Poly1‘ℂfld)))
153 eqid 2736 . . . . . . . . . . . 12 ( ·𝑠 ‘(Poly1‘ℂfld)) = ( ·𝑠 ‘(Poly1‘ℂfld))
154 eqid 2736 . . . . . . . . . . . 12 (coe1𝑎) = (coe1𝑎)
15554, 114, 93, 153, 110, 116, 154ply1coe 21667 . . . . . . . . . . 11 ((ℂfld ∈ Ring ∧ 𝑎 ∈ (Base‘(Poly1‘ℂfld))) → 𝑎 = ((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
1569, 152, 155sylancr 587 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝑎 = ((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
157156fveq2d 6846 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸𝑎) = (𝐸‘((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))))
158 eqid 2736 . . . . . . . . . 10 (0g‘(Poly1‘ℂfld)) = (0g‘(Poly1‘ℂfld))
15954ply1ring 21619 . . . . . . . . . . . 12 (ℂfld ∈ Ring → (Poly1‘ℂfld) ∈ Ring)
1609, 159ax-mp 5 . . . . . . . . . . 11 (Poly1‘ℂfld) ∈ Ring
161 ringcmn 20003 . . . . . . . . . . 11 ((Poly1‘ℂfld) ∈ Ring → (Poly1‘ℂfld) ∈ CMnd)
162160, 161mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (Poly1‘ℂfld) ∈ CMnd)
163 ringmnd 19974 . . . . . . . . . . 11 ((ℂflds ℂ) ∈ Ring → (ℂflds ℂ) ∈ Mnd)
16449, 163mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (ℂflds ℂ) ∈ Mnd)
165 nn0ex 12419 . . . . . . . . . . 11 0 ∈ V
166165a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ℕ0 ∈ V)
167 rhmghm 20157 . . . . . . . . . . . 12 (𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂflds ℂ)) → 𝐸 ∈ ((Poly1‘ℂfld) GrpHom (ℂflds ℂ)))
16856, 167ax-mp 5 . . . . . . . . . . 11 𝐸 ∈ ((Poly1‘ℂfld) GrpHom (ℂflds ℂ))
169 ghmmhm 19018 . . . . . . . . . . 11 (𝐸 ∈ ((Poly1‘ℂfld) GrpHom (ℂflds ℂ)) → 𝐸 ∈ ((Poly1‘ℂfld) MndHom (ℂflds ℂ)))
170168, 169mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝐸 ∈ ((Poly1‘ℂfld) MndHom (ℂflds ℂ)))
17154ply1lmod 21623 . . . . . . . . . . . . 13 (ℂfld ∈ Ring → (Poly1‘ℂfld) ∈ LMod)
1729, 171mp1i 13 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (Poly1‘ℂfld) ∈ LMod)
17312ad2antrr 724 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑆 ⊆ ℂ)
174 eqid 2736 . . . . . . . . . . . . . . . . 17 (Base‘𝑅) = (Base‘𝑅)
175154, 59, 58, 174coe1f 21582 . . . . . . . . . . . . . . . 16 (𝑎𝐴 → (coe1𝑎):ℕ0⟶(Base‘𝑅))
17657subrgbas 20231 . . . . . . . . . . . . . . . . 17 (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 = (Base‘𝑅))
177176feq3d 6655 . . . . . . . . . . . . . . . 16 (𝑆 ∈ (SubRing‘ℂfld) → ((coe1𝑎):ℕ0𝑆 ↔ (coe1𝑎):ℕ0⟶(Base‘𝑅)))
178175, 177syl5ibr 245 . . . . . . . . . . . . . . 15 (𝑆 ∈ (SubRing‘ℂfld) → (𝑎𝐴 → (coe1𝑎):ℕ0𝑆))
179178imp 407 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (coe1𝑎):ℕ0𝑆)
180179ffvelcdmda 7035 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1𝑎)‘𝑘) ∈ 𝑆)
181173, 180sseldd 3945 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1𝑎)‘𝑘) ∈ ℂ)
182110, 93mgpbas 19902 . . . . . . . . . . . . 13 (Base‘(Poly1‘ℂfld)) = (Base‘(mulGrp‘(Poly1‘ℂfld)))
183110ringmgp 19970 . . . . . . . . . . . . . 14 ((Poly1‘ℂfld) ∈ Ring → (mulGrp‘(Poly1‘ℂfld)) ∈ Mnd)
184160, 183mp1i 13 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (mulGrp‘(Poly1‘ℂfld)) ∈ Mnd)
185 simpr 485 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
186114, 54, 93vr1cl 21588 . . . . . . . . . . . . . 14 (ℂfld ∈ Ring → (var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)))
1879, 186mp1i 13 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)))
188182, 116, 184, 185, 187mulgnn0cld 18897 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)))
18954ply1sca 21624 . . . . . . . . . . . . . 14 (ℂfld ∈ Ring → ℂfld = (Scalar‘(Poly1‘ℂfld)))
1909, 189ax-mp 5 . . . . . . . . . . . . 13 fld = (Scalar‘(Poly1‘ℂfld))
19193, 190, 153, 4lmodvscl 20339 . . . . . . . . . . . 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)))
192172, 181, 188, 191syl3anc 1371 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(Poly1‘ℂfld)))
193192fmpttd 7063 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℕ0⟶(Base‘(Poly1‘ℂfld)))
194165mptex 7173 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ V
195 funmpt 6539 . . . . . . . . . . . . 13 Fun (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
196 fvex 6855 . . . . . . . . . . . . 13 (0g‘(Poly1‘ℂfld)) ∈ V
197194, 195, 1963pm3.2i 1339 . . . . . . . . . . . 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)
198197a1i 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))
199154, 93, 54, 17coe1sfi 21584 . . . . . . . . . . . . 13 (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → (coe1𝑎) finSupp 0)
200152, 199syl 17 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (coe1𝑎) finSupp 0)
201200fsuppimpd 9312 . . . . . . . . . . 11 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((coe1𝑎) supp 0) ∈ Fin)
202179feqmptd 6910 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (coe1𝑎) = (𝑘 ∈ ℕ0 ↦ ((coe1𝑎)‘𝑘)))
203202oveq1d 7372 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((coe1𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦ ((coe1𝑎)‘𝑘)) supp 0))
204 eqimss2 4001 . . . . . . . . . . . . 13 (((coe1𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦ ((coe1𝑎)‘𝑘)) supp 0) → ((𝑘 ∈ ℕ0 ↦ ((coe1𝑎)‘𝑘)) supp 0) ⊆ ((coe1𝑎) supp 0))
205203, 204syl 17 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((𝑘 ∈ ℕ0 ↦ ((coe1𝑎)‘𝑘)) supp 0) ⊆ ((coe1𝑎) supp 0))
2069, 171mp1i 13 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (Poly1‘ℂfld) ∈ LMod)
20793, 190, 153, 17, 158lmod0vs 20355 . . . . . . . . . . . . 13 (((Poly1‘ℂfld) ∈ LMod ∧ 𝑥 ∈ (Base‘(Poly1‘ℂfld))) → (0( ·𝑠 ‘(Poly1‘ℂfld))𝑥) = (0g‘(Poly1‘ℂfld)))
208206, 207sylan 580 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑥 ∈ (Base‘(Poly1‘ℂfld))) → (0( ·𝑠 ‘(Poly1‘ℂfld))𝑥) = (0g‘(Poly1‘ℂfld)))
209 c0ex 11149 . . . . . . . . . . . . 13 0 ∈ V
210209a1i 11 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 0 ∈ V)
211205, 208, 180, 188, 210suppssov1 8129 . . . . . . . . . . 11 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) supp (0g‘(Poly1‘ℂfld))) ⊆ ((coe1𝑎) supp 0))
212 suppssfifsupp 9320 . . . . . . . . . . 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)))
213198, 201, 211, 212syl12anc 835 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) finSupp (0g‘(Poly1‘ℂfld)))
21493, 158, 162, 164, 166, 170, 193, 213gsummhm 19715 . . . . . . . . 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)))))))
21595a1i 11 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂflds ℂ)))
216215, 192cofmpt 7078 . . . . . . . . . . 11 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
2179a1i 11 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → ℂfld ∈ Ring)
2186a1i 11 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → ℂ ∈ V)
21995ffvelcdmi 7034 . . . . . . . . . . . . . . . 16 ((((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(Poly1‘ℂfld)) → (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ (Base‘(ℂflds ℂ)))
220192, 219syl 17 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ (Base‘(ℂflds ℂ)))
2213, 4, 67, 217, 218, 220pwselbas 17371 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℂ⟶ℂ)
222221feqmptd 6910 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) = (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧)))
22352a1i 11 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ℂfld ∈ CRing)
224 simpr 485 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
22553, 114, 4, 54, 93, 223, 224evl1vard 21703 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧))
226185adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0)
22753, 54, 4, 93, 223, 224, 225, 116, 127, 226evl1expd 21711 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧)))
228224, 226, 131syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧𝑘))
229228eqeq2d 2747 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧) ↔ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧𝑘)))
230229anbi2d 629 . . . . . . . . . . . . . . . . 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)))‘𝑧) = (𝑧𝑘))))
231227, 230mpbid 231 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧𝑘)))
232181adantr 481 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((coe1𝑎)‘𝑘) ∈ ℂ)
23353, 54, 4, 93, 223, 224, 231, 232, 153, 80evl1vsd 21710 . . . . . . . . . . . . . . 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𝑎)‘𝑘) · (𝑧𝑘))))
234233simprd 496 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧) = (((coe1𝑎)‘𝑘) · (𝑧𝑘)))
235234mpteq2dva 5205 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧)) = (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))
236222, 235eqtrd 2776 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) = (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))
237236mpteq2dva 5205 . . . . . . . . . . 11 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))))
238216, 237eqtrd 2776 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))))
239238oveq2d 7373 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((ℂflds ℂ) Σg (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))) = ((ℂflds ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))))
240157, 214, 2393eqtr2d 2782 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸𝑎) = ((ℂflds ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))))
2416a1i 11 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ℂ ∈ V)
2429, 10mp1i 13 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ℂfld ∈ CMnd)
243181adantlr 713 . . . . . . . . . . 11 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((coe1𝑎)‘𝑘) ∈ ℂ)
24433adantll 712 . . . . . . . . . . 11 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧𝑘) ∈ ℂ)
245243, 244mulcld 11175 . . . . . . . . . 10 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) ∈ ℂ)
246245anasss 467 . . . . . . . . 9 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) ∈ ℂ)
247165mptex 7173 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∈ V
248 funmpt 6539 . . . . . . . . . . . 12 Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))
249247, 248, 393pm3.2i 1339 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∧ (0g‘(ℂflds ℂ)) ∈ V)
250249a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∧ (0g‘(ℂflds ℂ)) ∈ V))
251 fzfid 13878 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ∈ Fin)
252 eldifn 4087 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))) → ¬ 𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
253252adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → ¬ 𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
254152ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → 𝑎 ∈ (Base‘(Poly1‘ℂfld)))
255 eldifi 4086 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))) → 𝑘 ∈ ℕ0)
256255adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℕ0)
257 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . 24 ( deg1 ‘ℂfld) = ( deg1 ‘ℂfld)
258257, 54, 93, 17, 154deg1ge 25463 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎 ∈ (Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0 ∧ ((coe1𝑎)‘𝑘) ≠ 0) → 𝑘 ≤ (( deg1 ‘ℂfld)‘𝑎))
2592583expia 1121 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ (Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0) → (((coe1𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ (( deg1 ‘ℂfld)‘𝑎)))
260254, 256, 259syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ (( deg1 ‘ℂfld)‘𝑎)))
261 0xr 11202 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℝ*
262257, 54, 93deg1xrcl 25447 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → (( deg1 ‘ℂfld)‘𝑎) ∈ ℝ*)
263152, 262syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (( deg1 ‘ℂfld)‘𝑎) ∈ ℝ*)
264263ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (( deg1 ‘ℂfld)‘𝑎) ∈ ℝ*)
265 xrmax2 13095 . . . . . . . . . . . . . . . . . . . . . . 23 ((0 ∈ ℝ* ∧ (( deg1 ‘ℂfld)‘𝑎) ∈ ℝ*) → (( deg1 ‘ℂfld)‘𝑎) ≤ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))
266261, 264, 265sylancr 587 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (( deg1 ‘ℂfld)‘𝑎) ≤ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))
267256nn0red 12474 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ)
268267rexrd 11205 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ*)
269 ifcl 4531 . . . . . . . . . . . . . . . . . . . . . . . 24 (((( deg1 ‘ℂfld)‘𝑎) ∈ ℝ* ∧ 0 ∈ ℝ*) → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℝ*)
270264, 261, 269sylancl 586 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℝ*)
271 xrletr 13077 . . . . . . . . . . . . . . . . . . . . . . 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)))
272268, 264, 270, 271syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . 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)))
273266, 272mpan2d 692 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (𝑘 ≤ (( deg1 ‘ℂfld)‘𝑎) → 𝑘 ≤ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
274260, 273syld 47 . . . . . . . . . . . . . . . . . . . 20 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
275274, 256jctild 526 . . . . . . . . . . . . . . . . . . 19 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) ≠ 0 → (𝑘 ∈ ℕ0𝑘 ≤ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))))
276257, 54, 93deg1cl 25448 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → (( deg1 ‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
277152, 276syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (( deg1 ‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
278 elun 4108 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 ‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}) ↔ ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 ∨ (( deg1 ‘ℂfld)‘𝑎) ∈ {-∞}))
279277, 278sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 ∨ (( deg1 ‘ℂfld)‘𝑎) ∈ {-∞}))
280 nn0ge0 12438 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → 0 ≤ (( deg1 ‘ℂfld)‘𝑎))
281280iftrued 4494 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) = (( deg1 ‘ℂfld)‘𝑎))
282 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → (( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0)
283281, 282eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0)
284 mnflt0 13046 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -∞ < 0
285 mnfxr 11212 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 -∞ ∈ ℝ*
286 xrltnle 11222 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*) → (-∞ < 0 ↔ ¬ 0 ≤ -∞))
287285, 261, 286mp2an 690 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (-∞ < 0 ↔ ¬ 0 ≤ -∞)
288284, 287mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ¬ 0 ≤ -∞
289 elsni 4603 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((( deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → (( deg1 ‘ℂfld)‘𝑎) = -∞)
290289breq2d 5117 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → (0 ≤ (( deg1 ‘ℂfld)‘𝑎) ↔ 0 ≤ -∞))
291288, 290mtbiri 326 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → ¬ 0 ≤ (( deg1 ‘ℂfld)‘𝑎))
292291iffalsed 4497 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) = 0)
293 0nn0 12428 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ ℕ0
294292, 293eqeltrdi 2846 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0)
295283, 294jaoi 855 . . . . . . . . . . . . . . . . . . . . . 22 (((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 ∨ (( deg1 ‘ℂfld)‘𝑎) ∈ {-∞}) → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0)
296279, 295syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0)
297296ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0)
298 fznn0 13533 . . . . . . . . . . . . . . . . . . . 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))))
299297, 298syl 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))))
300275, 299sylibrd 258 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) ≠ 0 → 𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))))
301300necon1bd 2961 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (¬ 𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) → ((coe1𝑎)‘𝑘) = 0))
302253, 301mpd 15 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → ((coe1𝑎)‘𝑘) = 0)
303302oveq1d 7372 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) = (0 · (𝑧𝑘)))
304255, 244sylan2 593 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (𝑧𝑘) ∈ ℂ)
305304mul02d 11353 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (0 · (𝑧𝑘)) = 0)
306303, 305eqtrd 2776 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) = 0)
307306an32s 650 . . . . . . . . . . . . 13 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) ∧ 𝑧 ∈ ℂ) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) = 0)
308307mpteq2dva 5205 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ 0))
309 fconstmpt 5694 . . . . . . . . . . . . 13 (ℂ × {0}) = (𝑧 ∈ ℂ ↦ 0)
310 ringmnd 19974 . . . . . . . . . . . . . . 15 (ℂfld ∈ Ring → ℂfld ∈ Mnd)
3119, 310ax-mp 5 . . . . . . . . . . . . . 14 fld ∈ Mnd
3123, 17pws0g 18592 . . . . . . . . . . . . . 14 ((ℂfld ∈ Mnd ∧ ℂ ∈ V) → (ℂ × {0}) = (0g‘(ℂflds ℂ)))
313311, 6, 312mp2an 690 . . . . . . . . . . . . 13 (ℂ × {0}) = (0g‘(ℂflds ℂ))
314309, 313eqtr3i 2766 . . . . . . . . . . . 12 (𝑧 ∈ ℂ ↦ 0) = (0g‘(ℂflds ℂ))
315308, 314eqtrdi 2792 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) = (0g‘(ℂflds ℂ)))
316315, 166suppss2 8131 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) supp (0g‘(ℂflds ℂ))) ⊆ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
317 suppssfifsupp 9320 . . . . . . . . . 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 ℂ)))
318250, 251, 316, 317syl12anc 835 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) finSupp (0g‘(ℂflds ℂ)))
3193, 4, 5, 241, 166, 242, 246, 318pwsgsum 19759 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((ℂflds ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))))
320 fz0ssnn0 13536 . . . . . . . . . . . 12 (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ⊆ ℕ0
321 resmpt 5991 . . . . . . . . . . . 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𝑎)‘𝑘) · (𝑧𝑘))))
322320, 321ax-mp 5 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ↾ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))) = (𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))
323322oveq2i 7368 . . . . . . . . . 10 (ℂfld Σg ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ↾ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) = (ℂfld Σg (𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))
3249, 10mp1i 13 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → ℂfld ∈ CMnd)
325165a1i 11 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → ℕ0 ∈ V)
326245fmpttd 7063 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))):ℕ0⟶ℂ)
327306, 325suppss2 8131 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) supp 0) ⊆ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
328165mptex 7173 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∈ V
329 funmpt 6539 . . . . . . . . . . . . . 14 Fun (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))
330328, 329, 2093pm3.2i 1339 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∧ 0 ∈ V)
331330a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∧ 0 ∈ V))
332 fzfid 13878 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ∈ Fin)
333 suppssfifsupp 9320 . . . . . . . . . . . 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)
334331, 332, 327, 333syl12anc 835 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) finSupp 0)
3354, 17, 324, 325, 326, 327, 334gsumres 19690 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ↾ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) = (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))))
336 elfznn0 13534 . . . . . . . . . . . 12 (𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) → 𝑘 ∈ ℕ0)
337336, 245sylan2 593 . . . . . . . . . . 11 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) ∈ ℂ)
338332, 337gsumfsum 20864 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘)))
339323, 335, 3383eqtr3a 2800 . . . . . . . . 9 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘)))
340339mpteq2dva 5205 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘))))
341240, 319, 3403eqtrd 2780 . . . . . . 7 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸𝑎) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘))))
34212adantr 481 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝑆 ⊆ ℂ)
343 elplyr 25562 . . . . . . . 8 ((𝑆 ⊆ ℂ ∧ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0 ∧ (coe1𝑎):ℕ0𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∈ (Poly‘𝑆))
344342, 296, 179, 343syl3anc 1371 . . . . . . 7 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∈ (Poly‘𝑆))
345341, 344eqeltrd 2838 . . . . . 6 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸𝑎) ∈ (Poly‘𝑆))
346 eleq1 2825 . . . . . 6 ((𝐸𝑎) = 𝑓 → ((𝐸𝑎) ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (Poly‘𝑆)))
347345, 346syl5ibcom 244 . . . . 5 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((𝐸𝑎) = 𝑓𝑓 ∈ (Poly‘𝑆)))
348347rexlimdva 3152 . . . 4 (𝑆 ∈ (SubRing‘ℂfld) → (∃𝑎𝐴 (𝐸𝑎) = 𝑓𝑓 ∈ (Poly‘𝑆)))
349151, 348syl5 34 . . 3 (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (𝐸𝐴) → 𝑓 ∈ (Poly‘𝑆)))
350147, 349impbid 211 . 2 (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (𝐸𝐴)))
351350eqrdv 2734 1 (𝑆 ∈ (SubRing‘ℂfld) → (Poly‘𝑆) = (𝐸𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wrex 3073  Vcvv 3445  cdif 3907  cun 3908  wss 3910  ifcif 4486  {csn 4586   class class class wbr 5105  cmpt 5188   × cxp 5631  cres 5635  cima 5636  ccom 5637  Fun wfun 6490   Fn wfn 6491  wf 6492  cfv 6496  (class class class)co 7357  f cof 7615   supp csupp 8092  m cmap 8765  Fincfn 8883   finSupp cfsupp 9305  cc 11049  0cc0 11051   · cmul 11056  -∞cmnf 11187  *cxr 11188   < clt 11189  cle 11190  0cn0 12413  ...cfz 13424  cexp 13967  Σcsu 15570  Basecbs 17083  s cress 17112  .rcmulr 17134  Scalarcsca 17136   ·𝑠 cvsca 17137  0gc0g 17321   Σg cgsu 17322  s cpws 17328  Mndcmnd 18556   MndHom cmhm 18599  SubMndcsubmnd 18600  .gcmg 18872  SubGrpcsubg 18922   GrpHom cghm 19005  CMndccmn 19562  mulGrpcmgp 19896  Ringcrg 19964  CRingccrg 19965   RingHom crh 20143  SubRingcsubrg 20218  LModclmod 20322  fldccnfld 20796  algSccascl 21258  var1cv1 21547  Poly1cpl1 21548  coe1cco1 21549  eval1ce1 21680   deg1 cdg1 25416  Polycply 25545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-ofr 7618  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-sup 9378  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-rp 12916  df-fz 13425  df-fzo 13568  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-sum 15571  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-0g 17323  df-gsum 17324  df-prds 17329  df-pws 17331  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-mhm 18601  df-submnd 18602  df-grp 18751  df-minusg 18752  df-sbg 18753  df-mulg 18873  df-subg 18925  df-ghm 19006  df-cntz 19097  df-cmn 19564  df-abl 19565  df-mgp 19897  df-ur 19914  df-srg 19918  df-ring 19966  df-cring 19967  df-rnghom 20146  df-subrg 20220  df-lmod 20324  df-lss 20393  df-lsp 20433  df-cnfld 20797  df-assa 21259  df-asp 21260  df-ascl 21261  df-psr 21311  df-mvr 21312  df-mpl 21313  df-opsr 21315  df-evls 21482  df-evl 21483  df-psr1 21551  df-vr1 21552  df-ply1 21553  df-coe1 21554  df-evl1 21682  df-mdeg 25417  df-deg1 25418  df-ply 25549
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator