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

Theorem plypf1 24816
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 24799 . . . . 5 (𝑓 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))))
21simprbi 500 . . . 4 (𝑓 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))
3 eqid 2824 . . . . . . . . 9 (ℂflds ℂ) = (ℂflds ℂ)
4 cnfldbas 20102 . . . . . . . . 9 ℂ = (Base‘ℂfld)
5 eqid 2824 . . . . . . . . 9 (0g‘(ℂflds ℂ)) = (0g‘(ℂflds ℂ))
6 cnex 10616 . . . . . . . . . 10 ℂ ∈ V
76a1i 11 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → ℂ ∈ V)
8 fzfid 13345 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (0...𝑛) ∈ Fin)
9 cnring 20120 . . . . . . . . . 10 fld ∈ Ring
10 ringcmn 19334 . . . . . . . . . 10 (ℂfld ∈ Ring → ℂfld ∈ CMnd)
119, 10mp1i 13 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → ℂfld ∈ CMnd)
124subrgss 19536 . . . . . . . . . . . . 13 (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ⊆ ℂ)
1312ad2antrr 725 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ⊆ ℂ)
14 elmapi 8424 . . . . . . . . . . . . . . 15 (𝑎 ∈ ((𝑆 ∪ {0}) ↑m0) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
1514ad2antll 728 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → 𝑎:ℕ0⟶(𝑆 ∪ {0}))
16 subrgsubg 19541 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 ∈ (SubGrp‘ℂfld))
17 cnfld0 20122 . . . . . . . . . . . . . . . . . . . 20 0 = (0g‘ℂfld)
1817subg0cl 18287 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ (SubGrp‘ℂfld) → 0 ∈ 𝑆)
1916, 18syl 17 . . . . . . . . . . . . . . . . . 18 (𝑆 ∈ (SubRing‘ℂfld) → 0 ∈ 𝑆)
2019adantr 484 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → 0 ∈ 𝑆)
2120snssd 4726 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → {0} ⊆ 𝑆)
22 ssequn2 4145 . . . . . . . . . . . . . . . 16 ({0} ⊆ 𝑆 ↔ (𝑆 ∪ {0}) = 𝑆)
2321, 22sylib 221 . . . . . . . . . . . . . . 15 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑆 ∪ {0}) = 𝑆)
2423feq3d 6490 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑎:ℕ0⟶(𝑆 ∪ {0}) ↔ 𝑎:ℕ0𝑆))
2515, 24mpbid 235 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → 𝑎:ℕ0𝑆)
26 elfznn0 13004 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0)
27 ffvelrn 6840 . . . . . . . . . . . . 13 ((𝑎:ℕ0𝑆𝑘 ∈ ℕ0) → (𝑎𝑘) ∈ 𝑆)
2825, 26, 27syl2an 598 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎𝑘) ∈ 𝑆)
2913, 28sseldd 3954 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎𝑘) ∈ ℂ)
3029adantrl 715 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑎𝑘) ∈ ℂ)
31 simprl 770 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑧 ∈ ℂ)
3226ad2antll 728 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → 𝑘 ∈ ℕ0)
33 expcl 13452 . . . . . . . . . . 11 ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑧𝑘) ∈ ℂ)
3431, 32, 33syl2anc 587 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → (𝑧𝑘) ∈ ℂ)
3530, 34mulcld 10659 . . . . . . . . 9 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ (0...𝑛))) → ((𝑎𝑘) · (𝑧𝑘)) ∈ ℂ)
36 eqid 2824 . . . . . . . . . 10 (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘)))) = (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))
376mptex 6977 . . . . . . . . . . 11 (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))) ∈ V
3837a1i 11 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))) ∈ V)
39 fvex 6674 . . . . . . . . . . 11 (0g‘(ℂflds ℂ)) ∈ V
4039a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (0g‘(ℂflds ℂ)) ∈ V)
4136, 8, 38, 40fsuppmptdm 8841 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘)))) finSupp (0g‘(ℂflds ℂ)))
423, 4, 5, 7, 8, 11, 35, 41pwsgsum 19102 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → ((ℂflds ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎𝑘) · (𝑧𝑘))))))
43 fzfid 13345 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑧 ∈ ℂ) → (0...𝑛) ∈ Fin)
4435anassrs 471 . . . . . . . . . 10 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑛)) → ((𝑎𝑘) · (𝑧𝑘)) ∈ ℂ)
4543, 44gsumfsum 20165 . . . . . . . . 9 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎𝑘) · (𝑧𝑘)))) = Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))
4645mpteq2dva 5147 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑎𝑘) · (𝑧𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))
4742, 46eqtrd 2859 . . . . . . 7 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → ((ℂflds ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))
483pwsring 19368 . . . . . . . . . 10 ((ℂfld ∈ Ring ∧ ℂ ∈ V) → (ℂflds ℂ) ∈ Ring)
499, 6, 48mp2an 691 . . . . . . . . 9 (ℂflds ℂ) ∈ Ring
50 ringcmn 19334 . . . . . . . . 9 ((ℂflds ℂ) ∈ Ring → (ℂflds ℂ) ∈ CMnd)
5149, 50mp1i 13 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (ℂflds ℂ) ∈ CMnd)
52 cncrng 20119 . . . . . . . . . . 11 fld ∈ CRing
53 plypf1.e . . . . . . . . . . . 12 𝐸 = (eval1‘ℂfld)
54 eqid 2824 . . . . . . . . . . . 12 (Poly1‘ℂfld) = (Poly1‘ℂfld)
5553, 54, 3, 4evl1rhm 20963 . . . . . . . . . . 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 20869 . . . . . . . . . . 11 (𝑆 ∈ (SubRing‘ℂfld) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
6160adantr 484 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
62 rhmima 19566 . . . . . . . . . 10 ((𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂflds ℂ)) ∧ 𝐴 ∈ (SubRing‘(Poly1‘ℂfld))) → (𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)))
6356, 61, 62sylancr 590 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)))
64 subrgsubg 19541 . . . . . . . . 9 ((𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)) → (𝐸𝐴) ∈ (SubGrp‘(ℂflds ℂ)))
65 subgsubm 18301 . . . . . . . . 9 ((𝐸𝐴) ∈ (SubGrp‘(ℂflds ℂ)) → (𝐸𝐴) ∈ (SubMnd‘(ℂflds ℂ)))
6663, 64, 653syl 18 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝐸𝐴) ∈ (SubMnd‘(ℂflds ℂ)))
67 eqid 2824 . . . . . . . . . . . 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 6558 . . . . . . . . . . . . . 14 ((𝑎𝑘) ∈ ℂ → (ℂ × {(𝑎𝑘)}):ℂ⟶ℂ)
7129, 70syl 17 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎𝑘)}):ℂ⟶ℂ)
723, 4, 67pwselbasb 16761 . . . . . . . . . . . . . 14 ((ℂfld ∈ Ring ∧ ℂ ∈ V) → ((ℂ × {(𝑎𝑘)}) ∈ (Base‘(ℂflds ℂ)) ↔ (ℂ × {(𝑎𝑘)}):ℂ⟶ℂ))
739, 6, 72mp2an 691 . . . . . . . . . . . . 13 ((ℂ × {(𝑎𝑘)}) ∈ (Base‘(ℂflds ℂ)) ↔ (ℂ × {(𝑎𝑘)}):ℂ⟶ℂ)
7471, 73sylibr 237 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎𝑘)}) ∈ (Base‘(ℂflds ℂ)))
7534anass1rs 654 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑧𝑘) ∈ ℂ)
7675fmpttd 6870 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧𝑘)):ℂ⟶ℂ)
773, 4, 67pwselbasb 16761 . . . . . . . . . . . . . 14 ((ℂfld ∈ Ring ∧ ℂ ∈ V) → ((𝑧 ∈ ℂ ↦ (𝑧𝑘)) ∈ (Base‘(ℂflds ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧𝑘)):ℂ⟶ℂ))
789, 6, 77mp2an 691 . . . . . . . . . . . . 13 ((𝑧 ∈ ℂ ↦ (𝑧𝑘)) ∈ (Base‘(ℂflds ℂ)) ↔ (𝑧 ∈ ℂ ↦ (𝑧𝑘)):ℂ⟶ℂ)
7976, 78sylibr 237 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧𝑘)) ∈ (Base‘(ℂflds ℂ)))
80 cnfldmul 20104 . . . . . . . . . . . 12 · = (.r‘ℂfld)
81 eqid 2824 . . . . . . . . . . . 12 (.r‘(ℂflds ℂ)) = (.r‘(ℂflds ℂ))
823, 67, 68, 69, 74, 79, 80, 81pwsmulrval 16764 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎𝑘)})(.r‘(ℂflds ℂ))(𝑧 ∈ ℂ ↦ (𝑧𝑘))) = ((ℂ × {(𝑎𝑘)}) ∘f · (𝑧 ∈ ℂ ↦ (𝑧𝑘))))
8329adantr 484 . . . . . . . . . . . 12 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑎𝑘) ∈ ℂ)
84 fconstmpt 5601 . . . . . . . . . . . . 13 (ℂ × {(𝑎𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎𝑘))
8584a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎𝑘)}) = (𝑧 ∈ ℂ ↦ (𝑎𝑘)))
86 eqidd 2825 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧𝑘)) = (𝑧 ∈ ℂ ↦ (𝑧𝑘)))
8769, 83, 75, 85, 86offval2 7420 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎𝑘)}) ∘f · (𝑧 ∈ ℂ ↦ (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))
8882, 87eqtrd 2859 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎𝑘)})(.r‘(ℂflds ℂ))(𝑧 ∈ ℂ ↦ (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))
8963adantr 484 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)))
90 eqid 2824 . . . . . . . . . . . . . 14 (algSc‘(Poly1‘ℂfld)) = (algSc‘(Poly1‘ℂfld))
9153, 54, 4, 90evl1sca 20965 . . . . . . . . . . . . 13 ((ℂfld ∈ CRing ∧ (𝑎𝑘) ∈ ℂ) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘))) = (ℂ × {(𝑎𝑘)}))
9252, 29, 91sylancr 590 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘))) = (ℂ × {(𝑎𝑘)}))
93 eqid 2824 . . . . . . . . . . . . . . . 16 (Base‘(Poly1‘ℂfld)) = (Base‘(Poly1‘ℂfld))
9493, 67rhmf 19481 . . . . . . . . . . . . . . 15 (𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂflds ℂ)) → 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂflds ℂ)))
9556, 94ax-mp 5 . . . . . . . . . . . . . 14 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂflds ℂ))
96 ffn 6503 . . . . . . . . . . . . . 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 19536 . . . . . . . . . . . . . . 15 (𝐴 ∈ (SubRing‘(Poly1‘ℂfld)) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
9960, 98syl 17 . . . . . . . . . . . . . 14 (𝑆 ∈ (SubRing‘ℂfld) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
10099ad2antrr 725 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ⊆ (Base‘(Poly1‘ℂfld)))
101 simpll 766 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑆 ∈ (SubRing‘ℂfld))
10254, 90, 57, 58, 101, 59, 4, 29subrg1asclcl 20896 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘)) ∈ 𝐴 ↔ (𝑎𝑘) ∈ 𝑆))
10328, 102mpbird 260 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → ((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘)) ∈ 𝐴)
104 fnfvima 6987 . . . . . . . . . . . . 13 ((𝐸 Fn (Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆ (Base‘(Poly1‘ℂfld)) ∧ ((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘)) ∈ 𝐴) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘))) ∈ (𝐸𝐴))
10597, 100, 103, 104syl3anc 1368 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘((algSc‘(Poly1‘ℂfld))‘(𝑎𝑘))) ∈ (𝐸𝐴))
10692, 105eqeltrrd 2917 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (ℂ × {(𝑎𝑘)}) ∈ (𝐸𝐴))
10767subrgss 19536 . . . . . . . . . . . . . . . . 17 ((𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)) → (𝐸𝐴) ⊆ (Base‘(ℂflds ℂ)))
10889, 107syl 17 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸𝐴) ⊆ (Base‘(ℂflds ℂ)))
10960ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈ (SubRing‘(Poly1‘ℂfld)))
110 eqid 2824 . . . . . . . . . . . . . . . . . . . 20 (mulGrp‘(Poly1‘ℂfld)) = (mulGrp‘(Poly1‘ℂfld))
111110subrgsubm 19548 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ (SubRing‘(Poly1‘ℂfld)) → 𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))))
112109, 111syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))))
11326adantl 485 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑘 ∈ ℕ0)
114 eqid 2824 . . . . . . . . . . . . . . . . . . 19 (var1‘ℂfld) = (var1‘ℂfld)
115114, 101, 57, 58, 59subrgvr1cl 20898 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (var1‘ℂfld) ∈ 𝐴)
116 eqid 2824 . . . . . . . . . . . . . . . . . . 19 (.g‘(mulGrp‘(Poly1‘ℂfld))) = (.g‘(mulGrp‘(Poly1‘ℂfld)))
117116submmulgcl 18270 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ (SubMnd‘(mulGrp‘(Poly1‘ℂfld))) ∧ 𝑘 ∈ ℕ0 ∧ (var1‘ℂfld) ∈ 𝐴) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
118112, 113, 115, 117syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴)
119 fnfvima 6987 . . . . . . . . . . . . . . . . 17 ((𝐸 Fn (Base‘(Poly1‘ℂfld)) ∧ 𝐴 ⊆ (Base‘(Poly1‘ℂfld)) ∧ (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ 𝐴) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (𝐸𝐴))
12097, 100, 118, 119syl3anc 1368 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (𝐸𝐴))
121108, 120sseldd 3954 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(ℂflds ℂ)))
1223, 4, 67, 68, 69, 121pwselbas 16762 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))):ℂ⟶ℂ)
123122feqmptd 6724 . . . . . . . . . . . . 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 488 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
12653, 114, 4, 54, 93, 124, 125evl1vard 20968 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧))
127 eqid 2824 . . . . . . . . . . . . . . . . 17 (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
128113adantr 484 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0)
12953, 54, 4, 93, 124, 125, 126, 116, 127, 128evl1expd 20976 . . . . . . . . . . . . . . . 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 499 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧))
131 cnfldexp 20131 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧𝑘))
132125, 128, 131syl2anc 587 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧𝑘))
133130, 132eqtrd 2859 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧𝑘))
134133mpteq2dva 5147 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧)) = (𝑧 ∈ ℂ ↦ (𝑧𝑘)))
135123, 134eqtrd 2859 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) = (𝑧 ∈ ℂ ↦ (𝑧𝑘)))
136135, 120eqeltrrd 2917 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ (𝑧𝑘)) ∈ (𝐸𝐴))
13781subrgmcl 19547 . . . . . . . . . . 11 (((𝐸𝐴) ∈ (SubRing‘(ℂflds ℂ)) ∧ (ℂ × {(𝑎𝑘)}) ∈ (𝐸𝐴) ∧ (𝑧 ∈ ℂ ↦ (𝑧𝑘)) ∈ (𝐸𝐴)) → ((ℂ × {(𝑎𝑘)})(.r‘(ℂflds ℂ))(𝑧 ∈ ℂ ↦ (𝑧𝑘))) ∈ (𝐸𝐴))
13889, 106, 136, 137syl3anc 1368 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → ((ℂ × {(𝑎𝑘)})(.r‘(ℂflds ℂ))(𝑧 ∈ ℂ ↦ (𝑧𝑘))) ∈ (𝐸𝐴))
13988, 138eqeltrrd 2917 . . . . . . . . 9 (((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))) ∈ (𝐸𝐴))
140139fmpttd 6870 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘)))):(0...𝑛)⟶(𝐸𝐴))
14136, 8, 139, 40fsuppmptdm 8841 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘)))) finSupp (0g‘(ℂflds ℂ)))
1425, 51, 8, 66, 140, 141gsumsubmcl 19039 . . . . . . 7 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → ((ℂflds ℂ) Σg (𝑘 ∈ (0...𝑛) ↦ (𝑧 ∈ ℂ ↦ ((𝑎𝑘) · (𝑧𝑘))))) ∈ (𝐸𝐴))
14347, 142eqeltrrd 2917 . . . . . 6 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) ∈ (𝐸𝐴))
144 eleq1 2903 . . . . . 6 (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) → (𝑓 ∈ (𝐸𝐴) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) ∈ (𝐸𝐴)))
145143, 144syl5ibrcom 250 . . . . 5 ((𝑆 ∈ (SubRing‘ℂfld) ∧ (𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0))) → (𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) → 𝑓 ∈ (𝐸𝐴)))
146145rexlimdvva 3286 . . . 4 (𝑆 ∈ (SubRing‘ℂfld) → (∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑m0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) → 𝑓 ∈ (𝐸𝐴)))
1472, 146syl5 34 . . 3 (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) → 𝑓 ∈ (𝐸𝐴)))
148 ffun 6506 . . . . . 6 (𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂflds ℂ)) → Fun 𝐸)
14995, 148ax-mp 5 . . . . 5 Fun 𝐸
150 fvelima 6722 . . . . 5 ((Fun 𝐸𝑓 ∈ (𝐸𝐴)) → ∃𝑎𝐴 (𝐸𝑎) = 𝑓)
151149, 150mpan 689 . . . 4 (𝑓 ∈ (𝐸𝐴) → ∃𝑎𝐴 (𝐸𝑎) = 𝑓)
15299sselda 3953 . . . . . . . . . . 11 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝑎 ∈ (Base‘(Poly1‘ℂfld)))
153 eqid 2824 . . . . . . . . . . . 12 ( ·𝑠 ‘(Poly1‘ℂfld)) = ( ·𝑠 ‘(Poly1‘ℂfld))
154 eqid 2824 . . . . . . . . . . . 12 (coe1𝑎) = (coe1𝑎)
15554, 114, 93, 153, 110, 116, 154ply1coe 20932 . . . . . . . . . . 11 ((ℂfld ∈ Ring ∧ 𝑎 ∈ (Base‘(Poly1‘ℂfld))) → 𝑎 = ((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
1569, 152, 155sylancr 590 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝑎 = ((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
157156fveq2d 6665 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸𝑎) = (𝐸‘((Poly1‘ℂfld) Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))))
158 eqid 2824 . . . . . . . . . 10 (0g‘(Poly1‘ℂfld)) = (0g‘(Poly1‘ℂfld))
15954ply1ring 20884 . . . . . . . . . . . 12 (ℂfld ∈ Ring → (Poly1‘ℂfld) ∈ Ring)
1609, 159ax-mp 5 . . . . . . . . . . 11 (Poly1‘ℂfld) ∈ Ring
161 ringcmn 19334 . . . . . . . . . . 11 ((Poly1‘ℂfld) ∈ Ring → (Poly1‘ℂfld) ∈ CMnd)
162160, 161mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (Poly1‘ℂfld) ∈ CMnd)
163 ringmnd 19307 . . . . . . . . . . 11 ((ℂflds ℂ) ∈ Ring → (ℂflds ℂ) ∈ Mnd)
16449, 163mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (ℂflds ℂ) ∈ Mnd)
165 nn0ex 11900 . . . . . . . . . . 11 0 ∈ V
166165a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ℕ0 ∈ V)
167 rhmghm 19480 . . . . . . . . . . . 12 (𝐸 ∈ ((Poly1‘ℂfld) RingHom (ℂflds ℂ)) → 𝐸 ∈ ((Poly1‘ℂfld) GrpHom (ℂflds ℂ)))
16856, 167ax-mp 5 . . . . . . . . . . 11 𝐸 ∈ ((Poly1‘ℂfld) GrpHom (ℂflds ℂ))
169 ghmmhm 18368 . . . . . . . . . . 11 (𝐸 ∈ ((Poly1‘ℂfld) GrpHom (ℂflds ℂ)) → 𝐸 ∈ ((Poly1‘ℂfld) MndHom (ℂflds ℂ)))
170168, 169mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝐸 ∈ ((Poly1‘ℂfld) MndHom (ℂflds ℂ)))
17154ply1lmod 20888 . . . . . . . . . . . . 13 (ℂfld ∈ Ring → (Poly1‘ℂfld) ∈ LMod)
1729, 171mp1i 13 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (Poly1‘ℂfld) ∈ LMod)
17312ad2antrr 725 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑆 ⊆ ℂ)
174 eqid 2824 . . . . . . . . . . . . . . . . 17 (Base‘𝑅) = (Base‘𝑅)
175154, 59, 58, 174coe1f 20847 . . . . . . . . . . . . . . . 16 (𝑎𝐴 → (coe1𝑎):ℕ0⟶(Base‘𝑅))
17657subrgbas 19544 . . . . . . . . . . . . . . . . 17 (𝑆 ∈ (SubRing‘ℂfld) → 𝑆 = (Base‘𝑅))
177176feq3d 6490 . . . . . . . . . . . . . . . 16 (𝑆 ∈ (SubRing‘ℂfld) → ((coe1𝑎):ℕ0𝑆 ↔ (coe1𝑎):ℕ0⟶(Base‘𝑅)))
178175, 177syl5ibr 249 . . . . . . . . . . . . . . 15 (𝑆 ∈ (SubRing‘ℂfld) → (𝑎𝐴 → (coe1𝑎):ℕ0𝑆))
179178imp 410 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (coe1𝑎):ℕ0𝑆)
180179ffvelrnda 6842 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1𝑎)‘𝑘) ∈ 𝑆)
181173, 180sseldd 3954 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → ((coe1𝑎)‘𝑘) ∈ ℂ)
182110ringmgp 19303 . . . . . . . . . . . . . 14 ((Poly1‘ℂfld) ∈ Ring → (mulGrp‘(Poly1‘ℂfld)) ∈ Mnd)
183160, 182mp1i 13 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (mulGrp‘(Poly1‘ℂfld)) ∈ Mnd)
184 simpr 488 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
185114, 54, 93vr1cl 20853 . . . . . . . . . . . . . 14 (ℂfld ∈ Ring → (var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)))
1869, 185mp1i 13 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)))
187110, 93mgpbas 19245 . . . . . . . . . . . . . 14 (Base‘(Poly1‘ℂfld)) = (Base‘(mulGrp‘(Poly1‘ℂfld)))
188187, 116mulgnn0cl 18244 . . . . . . . . . . . . 13 (((mulGrp‘(Poly1‘ℂfld)) ∈ Mnd ∧ 𝑘 ∈ ℕ0 ∧ (var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld))) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)))
189183, 184, 186, 188syl3anc 1368 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)))
19054ply1sca 20889 . . . . . . . . . . . . . 14 (ℂfld ∈ Ring → ℂfld = (Scalar‘(Poly1‘ℂfld)))
1919, 190ax-mp 5 . . . . . . . . . . . . 13 fld = (Scalar‘(Poly1‘ℂfld))
19293, 191, 153, 4lmodvscl 19651 . . . . . . . . . . . 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)))
193172, 181, 189, 192syl3anc 1368 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(Poly1‘ℂfld)))
194193fmpttd 6870 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℕ0⟶(Base‘(Poly1‘ℂfld)))
195165mptex 6977 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ V
196 funmpt 6381 . . . . . . . . . . . . 13 Fun (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))
197 fvex 6674 . . . . . . . . . . . . 13 (0g‘(Poly1‘ℂfld)) ∈ V
198195, 196, 1973pm3.2i 1336 . . . . . . . . . . . 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)
199198a1i 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))
200154, 93, 54, 17coe1sfi 20849 . . . . . . . . . . . . 13 (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → (coe1𝑎) finSupp 0)
201152, 200syl 17 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (coe1𝑎) finSupp 0)
202201fsuppimpd 8837 . . . . . . . . . . 11 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((coe1𝑎) supp 0) ∈ Fin)
203179feqmptd 6724 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (coe1𝑎) = (𝑘 ∈ ℕ0 ↦ ((coe1𝑎)‘𝑘)))
204203oveq1d 7164 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((coe1𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦ ((coe1𝑎)‘𝑘)) supp 0))
205 eqimss2 4010 . . . . . . . . . . . . 13 (((coe1𝑎) supp 0) = ((𝑘 ∈ ℕ0 ↦ ((coe1𝑎)‘𝑘)) supp 0) → ((𝑘 ∈ ℕ0 ↦ ((coe1𝑎)‘𝑘)) supp 0) ⊆ ((coe1𝑎) supp 0))
206204, 205syl 17 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((𝑘 ∈ ℕ0 ↦ ((coe1𝑎)‘𝑘)) supp 0) ⊆ ((coe1𝑎) supp 0))
2079, 171mp1i 13 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (Poly1‘ℂfld) ∈ LMod)
20893, 191, 153, 17, 158lmod0vs 19667 . . . . . . . . . . . . 13 (((Poly1‘ℂfld) ∈ LMod ∧ 𝑥 ∈ (Base‘(Poly1‘ℂfld))) → (0( ·𝑠 ‘(Poly1‘ℂfld))𝑥) = (0g‘(Poly1‘ℂfld)))
209207, 208sylan 583 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑥 ∈ (Base‘(Poly1‘ℂfld))) → (0( ·𝑠 ‘(Poly1‘ℂfld))𝑥) = (0g‘(Poly1‘ℂfld)))
210 c0ex 10633 . . . . . . . . . . . . 13 0 ∈ V
211210a1i 11 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 0 ∈ V)
212206, 209, 180, 189, 211suppssov1 7858 . . . . . . . . . . 11 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) supp (0g‘(Poly1‘ℂfld))) ⊆ ((coe1𝑎) supp 0))
213 suppssfifsupp 8845 . . . . . . . . . . 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)))
214199, 202, 212, 213syl12anc 835 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) finSupp (0g‘(Poly1‘ℂfld)))
21593, 158, 162, 164, 166, 170, 194, 214gsummhm 19058 . . . . . . . . 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)))))))
21695a1i 11 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝐸:(Base‘(Poly1‘ℂfld))⟶(Base‘(ℂflds ℂ)))
217216, 193cofmpt 6885 . . . . . . . . . . 11 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))))
2189a1i 11 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → ℂfld ∈ Ring)
2196a1i 11 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → ℂ ∈ V)
22095ffvelrni 6841 . . . . . . . . . . . . . . . 16 ((((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))) ∈ (Base‘(Poly1‘ℂfld)) → (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ (Base‘(ℂflds ℂ)))
221193, 220syl 17 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) ∈ (Base‘(ℂflds ℂ)))
2223, 4, 67, 218, 219, 221pwselbas 16762 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))):ℂ⟶ℂ)
223222feqmptd 6724 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) = (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧)))
22452a1i 11 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ℂfld ∈ CRing)
225 simpr 488 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
22653, 114, 4, 54, 93, 224, 225evl1vard 20968 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((var1‘ℂfld) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(var1‘ℂfld))‘𝑧) = 𝑧))
227184adantr 484 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0)
22853, 54, 4, 93, 224, 225, 226, 116, 127, 227evl1expd 20976 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧)))
229225, 227, 131syl2anc 587 . . . . . . . . . . . . . . . . . . 19 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (𝑘(.g‘(mulGrp‘ℂfld))𝑧) = (𝑧𝑘))
230229eqeq2d 2835 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑘(.g‘(mulGrp‘ℂfld))𝑧) ↔ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧𝑘)))
231230anbi2d 631 . . . . . . . . . . . . . . . . 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)))‘𝑧) = (𝑧𝑘))))
232228, 231mpbid 235 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)) ∈ (Base‘(Poly1‘ℂfld)) ∧ ((𝐸‘(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))‘𝑧) = (𝑧𝑘)))
233181adantr 484 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((coe1𝑎)‘𝑘) ∈ ℂ)
23453, 54, 4, 93, 224, 225, 232, 233, 153, 80evl1vsd 20975 . . . . . . . . . . . . . . 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𝑎)‘𝑘) · (𝑧𝑘))))
235234simprd 499 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧) = (((coe1𝑎)‘𝑘) · (𝑧𝑘)))
236235mpteq2dva 5147 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ ((𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))‘𝑧)) = (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))
237223, 236eqtrd 2859 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ ℕ0) → (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))) = (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))
238237mpteq2dva 5147 . . . . . . . . . . 11 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑘 ∈ ℕ0 ↦ (𝐸‘(((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))))
239217, 238eqtrd 2859 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld))))) = (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))))
240239oveq2d 7165 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((ℂflds ℂ) Σg (𝐸 ∘ (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘)( ·𝑠 ‘(Poly1‘ℂfld))(𝑘(.g‘(mulGrp‘(Poly1‘ℂfld)))(var1‘ℂfld)))))) = ((ℂflds ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))))
241157, 215, 2403eqtr2d 2865 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸𝑎) = ((ℂflds ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))))
2426a1i 11 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ℂ ∈ V)
2439, 10mp1i 13 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ℂfld ∈ CMnd)
244181adantlr 714 . . . . . . . . . . 11 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((coe1𝑎)‘𝑘) ∈ ℂ)
24533adantll 713 . . . . . . . . . . 11 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧𝑘) ∈ ℂ)
246244, 245mulcld 10659 . . . . . . . . . 10 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) ∈ ℂ)
247246anasss 470 . . . . . . . . 9 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ (𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) ∈ ℂ)
248165mptex 6977 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∈ V
249 funmpt 6381 . . . . . . . . . . . 12 Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))
250248, 249, 393pm3.2i 1336 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∧ (0g‘(ℂflds ℂ)) ∈ V)
251250a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) ∧ (0g‘(ℂflds ℂ)) ∈ V))
252 fzfid 13345 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ∈ Fin)
253 eldifn 4090 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))) → ¬ 𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
254253adantl 485 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → ¬ 𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
255152ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → 𝑎 ∈ (Base‘(Poly1‘ℂfld)))
256 eldifi 4089 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))) → 𝑘 ∈ ℕ0)
257256adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℕ0)
258 eqid 2824 . . . . . . . . . . . . . . . . . . . . . . . 24 ( deg1 ‘ℂfld) = ( deg1 ‘ℂfld)
259258, 54, 93, 17, 154deg1ge 24706 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎 ∈ (Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0 ∧ ((coe1𝑎)‘𝑘) ≠ 0) → 𝑘 ≤ (( deg1 ‘ℂfld)‘𝑎))
2602593expia 1118 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ (Base‘(Poly1‘ℂfld)) ∧ 𝑘 ∈ ℕ0) → (((coe1𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ (( deg1 ‘ℂfld)‘𝑎)))
261255, 257, 260syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ (( deg1 ‘ℂfld)‘𝑎)))
262 0xr 10686 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℝ*
263258, 54, 93deg1xrcl 24690 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → (( deg1 ‘ℂfld)‘𝑎) ∈ ℝ*)
264152, 263syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (( deg1 ‘ℂfld)‘𝑎) ∈ ℝ*)
265264ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (( deg1 ‘ℂfld)‘𝑎) ∈ ℝ*)
266 xrmax2 12566 . . . . . . . . . . . . . . . . . . . . . . 23 ((0 ∈ ℝ* ∧ (( deg1 ‘ℂfld)‘𝑎) ∈ ℝ*) → (( deg1 ‘ℂfld)‘𝑎) ≤ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))
267262, 265, 266sylancr 590 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (( deg1 ‘ℂfld)‘𝑎) ≤ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))
268257nn0red 11953 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ)
269268rexrd 10689 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → 𝑘 ∈ ℝ*)
270 ifcl 4494 . . . . . . . . . . . . . . . . . . . . . . . 24 (((( deg1 ‘ℂfld)‘𝑎) ∈ ℝ* ∧ 0 ∈ ℝ*) → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℝ*)
271265, 262, 270sylancl 589 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℝ*)
272 xrletr 12548 . . . . . . . . . . . . . . . . . . . . . . 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)))
273269, 265, 271, 272syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . 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)))
274267, 273mpan2d 693 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (𝑘 ≤ (( deg1 ‘ℂfld)‘𝑎) → 𝑘 ≤ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
275261, 274syld 47 . . . . . . . . . . . . . . . . . . . 20 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) ≠ 0 → 𝑘 ≤ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
276275, 257jctild 529 . . . . . . . . . . . . . . . . . . 19 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) ≠ 0 → (𝑘 ∈ ℕ0𝑘 ≤ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))))
277258, 54, 93deg1cl 24691 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ (Base‘(Poly1‘ℂfld)) → (( deg1 ‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
278152, 277syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (( deg1 ‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}))
279 elun 4111 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 ‘ℂfld)‘𝑎) ∈ (ℕ0 ∪ {-∞}) ↔ ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 ∨ (( deg1 ‘ℂfld)‘𝑎) ∈ {-∞}))
280278, 279sylib 221 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 ∨ (( deg1 ‘ℂfld)‘𝑎) ∈ {-∞}))
281 nn0ge0 11919 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → 0 ≤ (( deg1 ‘ℂfld)‘𝑎))
282281iftrued 4458 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) = (( deg1 ‘ℂfld)‘𝑎))
283 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → (( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0)
284282, 283eqeltrd 2916 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0)
285 mnflt0 12517 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -∞ < 0
286 mnfxr 10696 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 -∞ ∈ ℝ*
287 xrltnle 10706 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*) → (-∞ < 0 ↔ ¬ 0 ≤ -∞))
288286, 262, 287mp2an 691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (-∞ < 0 ↔ ¬ 0 ≤ -∞)
289285, 288mpbi 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ¬ 0 ≤ -∞
290 elsni 4567 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((( deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → (( deg1 ‘ℂfld)‘𝑎) = -∞)
291290breq2d 5064 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → (0 ≤ (( deg1 ‘ℂfld)‘𝑎) ↔ 0 ≤ -∞))
292289, 291mtbiri 330 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → ¬ 0 ≤ (( deg1 ‘ℂfld)‘𝑎))
293292iffalsed 4461 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) = 0)
294 0nn0 11909 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ ℕ0
295293, 294eqeltrdi 2924 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 ‘ℂfld)‘𝑎) ∈ {-∞} → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0)
296284, 295jaoi 854 . . . . . . . . . . . . . . . . . . . . . 22 (((( deg1 ‘ℂfld)‘𝑎) ∈ ℕ0 ∨ (( deg1 ‘ℂfld)‘𝑎) ∈ {-∞}) → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0)
297280, 296syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0)
298297ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0)
299 fznn0 13003 . . . . . . . . . . . . . . . . . . . 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))))
300298, 299syl 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))))
301276, 300sylibrd 262 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) ≠ 0 → 𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))))
302301necon1bd 3032 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (¬ 𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) → ((coe1𝑎)‘𝑘) = 0))
303254, 302mpd 15 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → ((coe1𝑎)‘𝑘) = 0)
304303oveq1d 7164 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) = (0 · (𝑧𝑘)))
305256, 245sylan2 595 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (𝑧𝑘) ∈ ℂ)
306305mul02d 10836 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (0 · (𝑧𝑘)) = 0)
307304, 306eqtrd 2859 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) = 0)
308307an32s 651 . . . . . . . . . . . . 13 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) ∧ 𝑧 ∈ ℂ) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) = 0)
309308mpteq2dva 5147 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ 0))
310 fconstmpt 5601 . . . . . . . . . . . . 13 (ℂ × {0}) = (𝑧 ∈ ℂ ↦ 0)
311 ringmnd 19307 . . . . . . . . . . . . . . 15 (ℂfld ∈ Ring → ℂfld ∈ Mnd)
3129, 311ax-mp 5 . . . . . . . . . . . . . 14 fld ∈ Mnd
3133, 17pws0g 17947 . . . . . . . . . . . . . 14 ((ℂfld ∈ Mnd ∧ ℂ ∈ V) → (ℂ × {0}) = (0g‘(ℂflds ℂ)))
314312, 6, 313mp2an 691 . . . . . . . . . . . . 13 (ℂ × {0}) = (0g‘(ℂflds ℂ))
315310, 314eqtr3i 2849 . . . . . . . . . . . 12 (𝑧 ∈ ℂ ↦ 0) = (0g‘(ℂflds ℂ))
316309, 315syl6eq 2875 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑘 ∈ (ℕ0 ∖ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) → (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) = (0g‘(ℂflds ℂ)))
317316, 166suppss2 7860 . . . . . . . . . 10 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) supp (0g‘(ℂflds ℂ))) ⊆ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
318 suppssfifsupp 8845 . . . . . . . . . 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 ℂ)))
319251, 252, 317, 318syl12anc 835 . . . . . . . . 9 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) finSupp (0g‘(ℂflds ℂ)))
3203, 4, 5, 242, 166, 243, 247, 319pwsgsum 19102 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((ℂflds ℂ) Σg (𝑘 ∈ ℕ0 ↦ (𝑧 ∈ ℂ ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))) = (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))))
321 fz0ssnn0 13006 . . . . . . . . . . . 12 (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ⊆ ℕ0
322 resmpt 5892 . . . . . . . . . . . 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𝑎)‘𝑘) · (𝑧𝑘))))
323321, 322ax-mp 5 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ↾ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))) = (𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))
324323oveq2i 7160 . . . . . . . . . 10 (ℂfld Σg ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ↾ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) = (ℂfld Σg (𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))
3259, 10mp1i 13 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → ℂfld ∈ CMnd)
326165a1i 11 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → ℕ0 ∈ V)
327246fmpttd 6870 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))):ℕ0⟶ℂ)
328307, 326suppss2 7860 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) supp 0) ⊆ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))
329165mptex 6977 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∈ V
330 funmpt 6381 . . . . . . . . . . . . . 14 Fun (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))
331329, 330, 2103pm3.2i 1336 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∧ 0 ∈ V)
332331a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∧ 0 ∈ V))
333 fzfid 13345 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ∈ Fin)
334 suppssfifsupp 8845 . . . . . . . . . . . 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)
335332, 333, 328, 334syl12anc 835 . . . . . . . . . . 11 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) finSupp 0)
3364, 17, 325, 326, 327, 328, 335gsumres 19033 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg ((𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))) ↾ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)))) = (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))))
337 elfznn0 13004 . . . . . . . . . . . 12 (𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) → 𝑘 ∈ ℕ0)
338337, 246sylan2 595 . . . . . . . . . . 11 ((((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))) → (((coe1𝑎)‘𝑘) · (𝑧𝑘)) ∈ ℂ)
339333, 338gsumfsum 20165 . . . . . . . . . 10 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0)) ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘)))
340324, 336, 3393eqtr3a 2883 . . . . . . . . 9 (((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) ∧ 𝑧 ∈ ℂ) → (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘)))) = Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘)))
341340mpteq2dva 5147 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑧 ∈ ℂ ↦ (ℂfld Σg (𝑘 ∈ ℕ0 ↦ (((coe1𝑎)‘𝑘) · (𝑧𝑘))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘))))
342241, 320, 3413eqtrd 2863 . . . . . . 7 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸𝑎) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘))))
34312adantr 484 . . . . . . . 8 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → 𝑆 ⊆ ℂ)
344 elplyr 24805 . . . . . . . 8 ((𝑆 ⊆ ℂ ∧ if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0) ∈ ℕ0 ∧ (coe1𝑎):ℕ0𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∈ (Poly‘𝑆))
345343, 297, 179, 344syl3anc 1368 . . . . . . 7 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(0 ≤ (( deg1 ‘ℂfld)‘𝑎), (( deg1 ‘ℂfld)‘𝑎), 0))(((coe1𝑎)‘𝑘) · (𝑧𝑘))) ∈ (Poly‘𝑆))
346342, 345eqeltrd 2916 . . . . . 6 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → (𝐸𝑎) ∈ (Poly‘𝑆))
347 eleq1 2903 . . . . . 6 ((𝐸𝑎) = 𝑓 → ((𝐸𝑎) ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (Poly‘𝑆)))
348346, 347syl5ibcom 248 . . . . 5 ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝑎𝐴) → ((𝐸𝑎) = 𝑓𝑓 ∈ (Poly‘𝑆)))
349348rexlimdva 3276 . . . 4 (𝑆 ∈ (SubRing‘ℂfld) → (∃𝑎𝐴 (𝐸𝑎) = 𝑓𝑓 ∈ (Poly‘𝑆)))
350151, 349syl5 34 . . 3 (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (𝐸𝐴) → 𝑓 ∈ (Poly‘𝑆)))
351147, 350impbid 215 . 2 (𝑆 ∈ (SubRing‘ℂfld) → (𝑓 ∈ (Poly‘𝑆) ↔ 𝑓 ∈ (𝐸𝐴)))
352351eqrdv 2822 1 (𝑆 ∈ (SubRing‘ℂfld) → (Poly‘𝑆) = (𝐸𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3a 1084   = wceq 1538  wcel 2115  wne 3014  wrex 3134  Vcvv 3480  cdif 3916  cun 3917  wss 3919  ifcif 4450  {csn 4550   class class class wbr 5052  cmpt 5132   × cxp 5540  cres 5544  cima 5545  ccom 5546  Fun wfun 6337   Fn wfn 6338  wf 6339  cfv 6343  (class class class)co 7149  f cof 7401   supp csupp 7826  m cmap 8402  Fincfn 8505   finSupp cfsupp 8830  cc 10533  0cc0 10535   · cmul 10540  -∞cmnf 10671  *cxr 10672   < clt 10673  cle 10674  0cn0 11894  ...cfz 12894  cexp 13434  Σcsu 15042  Basecbs 16483  s cress 16484  .rcmulr 16566  Scalarcsca 16568   ·𝑠 cvsca 16569  0gc0g 16713   Σg cgsu 16714  s cpws 16720  Mndcmnd 17911   MndHom cmhm 17954  SubMndcsubmnd 17955  .gcmg 18224  SubGrpcsubg 18273   GrpHom cghm 18355  CMndccmn 18906  mulGrpcmgp 19239  Ringcrg 19297  CRingccrg 19298   RingHom crh 19467  SubRingcsubrg 19531  LModclmod 19634  fldccnfld 20098  algSccascl 20548  var1cv1 20812  Poly1cpl1 20813  coe1cco1 20814  eval1ce1 20945   deg1 cdg1 24662  Polycply 24788
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-inf2 9101  ax-cnex 10591  ax-resscn 10592  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-mulcom 10599  ax-addass 10600  ax-mulass 10601  ax-distr 10602  ax-i2m1 10603  ax-1ne0 10604  ax-1rid 10605  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608  ax-pre-lttri 10609  ax-pre-lttrn 10610  ax-pre-ltadd 10611  ax-pre-mulgt0 10612  ax-pre-sup 10613  ax-addf 10614  ax-mulf 10615
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-of 7403  df-ofr 7404  df-om 7575  df-1st 7684  df-2nd 7685  df-supp 7827  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-er 8285  df-map 8404  df-pm 8405  df-ixp 8458  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-fsupp 8831  df-sup 8903  df-oi 8971  df-card 9365  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679  df-sub 10870  df-neg 10871  df-div 11296  df-nn 11635  df-2 11697  df-3 11698  df-4 11699  df-5 11700  df-6 11701  df-7 11702  df-8 11703  df-9 11704  df-n0 11895  df-z 11979  df-dec 12096  df-uz 12241  df-rp 12387  df-fz 12895  df-fzo 13038  df-seq 13374  df-exp 13435  df-hash 13696  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-clim 14845  df-sum 15043  df-struct 16485  df-ndx 16486  df-slot 16487  df-base 16489  df-sets 16490  df-ress 16491  df-plusg 16578  df-mulr 16579  df-starv 16580  df-sca 16581  df-vsca 16582  df-ip 16583  df-tset 16584  df-ple 16585  df-ds 16587  df-unif 16588  df-hom 16589  df-cco 16590  df-0g 16715  df-gsum 16716  df-prds 16721  df-pws 16723  df-mre 16857  df-mrc 16858  df-acs 16860  df-mgm 17852  df-sgrp 17901  df-mnd 17912  df-mhm 17956  df-submnd 17957  df-grp 18106  df-minusg 18107  df-sbg 18108  df-mulg 18225  df-subg 18276  df-ghm 18356  df-cntz 18447  df-cmn 18908  df-abl 18909  df-mgp 19240  df-ur 19252  df-srg 19256  df-ring 19299  df-cring 19300  df-rnghom 19470  df-subrg 19533  df-lmod 19636  df-lss 19704  df-lsp 19744  df-cnfld 20099  df-assa 20549  df-asp 20550  df-ascl 20551  df-psr 20601  df-mvr 20602  df-mpl 20603  df-opsr 20605  df-evls 20752  df-evl 20753  df-psr1 20816  df-vr1 20817  df-ply1 20818  df-coe1 20819  df-evl1 20947  df-mdeg 24663  df-deg1 24664  df-ply 24792
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator