MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  plypf1 Structured version   Visualization version   GIF version
Theorem plypf1 25717
Description: Write the set of complex polynomials in a subring in terms of the abstract polynomial construction. (Contributed by Mario Carneiro, 3-Jul-2015.) (Proof shortened by AV, 29-Sep-2019.)
Hypotheses
Ref Expression
plypf1.r 𝑅 = (β„‚fld β†Ύs 𝑆)
plypf1.p 𝑃 = (Poly1β€˜π‘…)
plypf1.a 𝐴 = (Baseβ€˜π‘ƒ)
plypf1.e 𝐸 = (eval1β€˜β„‚fld)
Assertion
Ref Expression
plypf1 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (Polyβ€˜π‘†) = (𝐸 β€œ 𝐴))
Proof of Theorem plypf1
Dummy variables 𝑓 π‘Ž π‘˜ 𝑛 π‘₯ 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elply 25700 . . . . 5 (𝑓 ∈ (Polyβ€˜π‘†) ↔ (𝑆 βŠ† β„‚ ∧ βˆƒπ‘› ∈ β„•0 βˆƒπ‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0)𝑓 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))))
21simprbi 497 . . . 4 (𝑓 ∈ (Polyβ€˜π‘†) β†’ βˆƒπ‘› ∈ β„•0 βˆƒπ‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0)𝑓 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
3 eqid 2732 . . . . . . . . 9 (β„‚fld ↑s β„‚) = (β„‚fld ↑s β„‚)
4 cnfldbas 20940 . . . . . . . . 9 β„‚ = (Baseβ€˜β„‚fld)
5 eqid 2732 . . . . . . . . 9 (0gβ€˜(β„‚fld ↑s β„‚)) = (0gβ€˜(β„‚fld ↑s β„‚))
6 cnex 11187 . . . . . . . . . 10 β„‚ ∈ V
76a1i 11 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ β„‚ ∈ V)
8 fzfid 13934 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (0...𝑛) ∈ Fin)
9 cnring 20959 . . . . . . . . . 10 β„‚fld ∈ Ring
10 ringcmn 20092 . . . . . . . . . 10 (β„‚fld ∈ Ring β†’ β„‚fld ∈ CMnd)
119, 10mp1i 13 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ β„‚fld ∈ CMnd)
124subrgss 20356 . . . . . . . . . . . . 13 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 𝑆 βŠ† β„‚)
1312ad2antrr 724 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ 𝑆 βŠ† β„‚)
14 elmapi 8839 . . . . . . . . . . . . . . 15 (π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0) β†’ π‘Ž:β„•0⟢(𝑆 βˆͺ {0}))
1514ad2antll 727 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ π‘Ž:β„•0⟢(𝑆 βˆͺ {0}))
16 subrgsubg 20361 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 𝑆 ∈ (SubGrpβ€˜β„‚fld))
17 cnfld0 20961 . . . . . . . . . . . . . . . . . . . 20 0 = (0gβ€˜β„‚fld)
1817subg0cl 19008 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ (SubGrpβ€˜β„‚fld) β†’ 0 ∈ 𝑆)
1916, 18syl 17 . . . . . . . . . . . . . . . . . 18 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 0 ∈ 𝑆)
2019adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ 0 ∈ 𝑆)
2120snssd 4811 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ {0} βŠ† 𝑆)
22 ssequn2 4182 . . . . . . . . . . . . . . . 16 ({0} βŠ† 𝑆 ↔ (𝑆 βˆͺ {0}) = 𝑆)
2321, 22sylib 217 . . . . . . . . . . . . . . 15 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝑆 βˆͺ {0}) = 𝑆)
2423feq3d 6701 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (π‘Ž:β„•0⟢(𝑆 βˆͺ {0}) ↔ π‘Ž:β„•0βŸΆπ‘†))
2515, 24mpbid 231 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ π‘Ž:β„•0βŸΆπ‘†)
26 elfznn0 13590 . . . . . . . . . . . . 13 (π‘˜ ∈ (0...𝑛) β†’ π‘˜ ∈ β„•0)
27 ffvelcdm 7080 . . . . . . . . . . . . 13 ((π‘Ž:β„•0βŸΆπ‘† ∧ π‘˜ ∈ β„•0) β†’ (π‘Žβ€˜π‘˜) ∈ 𝑆)
2825, 26, 27syl2an 596 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (π‘Žβ€˜π‘˜) ∈ 𝑆)
2913, 28sseldd 3982 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (π‘Žβ€˜π‘˜) ∈ β„‚)
3029adantrl 714 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ (𝑧 ∈ β„‚ ∧ π‘˜ ∈ (0...𝑛))) β†’ (π‘Žβ€˜π‘˜) ∈ β„‚)
31 simprl 769 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ (𝑧 ∈ β„‚ ∧ π‘˜ ∈ (0...𝑛))) β†’ 𝑧 ∈ β„‚)
3226ad2antll 727 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ (𝑧 ∈ β„‚ ∧ π‘˜ ∈ (0...𝑛))) β†’ π‘˜ ∈ β„•0)
33 expcl 14041 . . . . . . . . . . 11 ((𝑧 ∈ β„‚ ∧ π‘˜ ∈ β„•0) β†’ (π‘§β†‘π‘˜) ∈ β„‚)
3431, 32, 33syl2anc 584 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ (𝑧 ∈ β„‚ ∧ π‘˜ ∈ (0...𝑛))) β†’ (π‘§β†‘π‘˜) ∈ β„‚)
3530, 34mulcld 11230 . . . . . . . . 9 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ (𝑧 ∈ β„‚ ∧ π‘˜ ∈ (0...𝑛))) β†’ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)) ∈ β„‚)
36 eqid 2732 . . . . . . . . . 10 (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))) = (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
376mptex 7221 . . . . . . . . . . 11 (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ V
3837a1i 11 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ V)
39 fvex 6901 . . . . . . . . . . 11 (0gβ€˜(β„‚fld ↑s β„‚)) ∈ V
4039a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (0gβ€˜(β„‚fld ↑s β„‚)) ∈ V)
4136, 8, 38, 40fsuppmptdm 9370 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))) finSupp (0gβ€˜(β„‚fld ↑s β„‚)))
423, 4, 5, 7, 8, 11, 35, 41pwsgsum 19844 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))) = (𝑧 ∈ β„‚ ↦ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑛) ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))))
43 fzfid 13934 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ 𝑧 ∈ β„‚) β†’ (0...𝑛) ∈ Fin)
4435anassrs 468 . . . . . . . . . 10 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (0...𝑛)) β†’ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)) ∈ β„‚)
4543, 44gsumfsum 21004 . . . . . . . . 9 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ 𝑧 ∈ β„‚) β†’ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑛) ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))) = Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))
4645mpteq2dva 5247 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝑧 ∈ β„‚ ↦ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑛) ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))) = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
4742, 46eqtrd 2772 . . . . . . 7 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))) = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
483pwsring 20130 . . . . . . . . . 10 ((β„‚fld ∈ Ring ∧ β„‚ ∈ V) β†’ (β„‚fld ↑s β„‚) ∈ Ring)
499, 6, 48mp2an 690 . . . . . . . . 9 (β„‚fld ↑s β„‚) ∈ Ring
50 ringcmn 20092 . . . . . . . . 9 ((β„‚fld ↑s β„‚) ∈ Ring β†’ (β„‚fld ↑s β„‚) ∈ CMnd)
5149, 50mp1i 13 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (β„‚fld ↑s β„‚) ∈ CMnd)
52 cncrng 20958 . . . . . . . . . . 11 β„‚fld ∈ CRing
53 plypf1.e . . . . . . . . . . . 12 𝐸 = (eval1β€˜β„‚fld)
54 eqid 2732 . . . . . . . . . . . 12 (Poly1β€˜β„‚fld) = (Poly1β€˜β„‚fld)
5553, 54, 3, 4evl1rhm 21842 . . . . . . . . . . 11 (β„‚fld ∈ CRing β†’ 𝐸 ∈ ((Poly1β€˜β„‚fld) RingHom (β„‚fld ↑s β„‚)))
5652, 55ax-mp 5 . . . . . . . . . 10 𝐸 ∈ ((Poly1β€˜β„‚fld) RingHom (β„‚fld ↑s β„‚))
57 plypf1.r . . . . . . . . . . . 12 𝑅 = (β„‚fld β†Ύs 𝑆)
58 plypf1.p . . . . . . . . . . . 12 𝑃 = (Poly1β€˜π‘…)
59 plypf1.a . . . . . . . . . . . 12 𝐴 = (Baseβ€˜π‘ƒ)
6054, 57, 58, 59subrgply1 21746 . . . . . . . . . . 11 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld)))
6160adantr 481 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ 𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld)))
62 rhmima 20388 . . . . . . . . . 10 ((𝐸 ∈ ((Poly1β€˜β„‚fld) RingHom (β„‚fld ↑s β„‚)) ∧ 𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld))) β†’ (𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)))
6356, 61, 62sylancr 587 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)))
64 subrgsubg 20361 . . . . . . . . 9 ((𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)) β†’ (𝐸 β€œ 𝐴) ∈ (SubGrpβ€˜(β„‚fld ↑s β„‚)))
65 subgsubm 19022 . . . . . . . . 9 ((𝐸 β€œ 𝐴) ∈ (SubGrpβ€˜(β„‚fld ↑s β„‚)) β†’ (𝐸 β€œ 𝐴) ∈ (SubMndβ€˜(β„‚fld ↑s β„‚)))
6663, 64, 653syl 18 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝐸 β€œ 𝐴) ∈ (SubMndβ€˜(β„‚fld ↑s β„‚)))
67 eqid 2732 . . . . . . . . . . . 12 (Baseβ€˜(β„‚fld ↑s β„‚)) = (Baseβ€˜(β„‚fld ↑s β„‚))
689a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ β„‚fld ∈ Ring)
696a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ β„‚ ∈ V)
70 fconst6g 6777 . . . . . . . . . . . . . 14 ((π‘Žβ€˜π‘˜) ∈ β„‚ β†’ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}):β„‚βŸΆβ„‚)
7129, 70syl 17 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}):β„‚βŸΆβ„‚)
723, 4, 67pwselbasb 17430 . . . . . . . . . . . . . 14 ((β„‚fld ∈ Ring ∧ β„‚ ∈ V) β†’ ((β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)) ↔ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}):β„‚βŸΆβ„‚))
739, 6, 72mp2an 690 . . . . . . . . . . . . 13 ((β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)) ↔ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}):β„‚βŸΆβ„‚)
7471, 73sylibr 233 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)))
7534anass1rs 653 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ (π‘§β†‘π‘˜) ∈ β„‚)
7675fmpttd 7111 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)):β„‚βŸΆβ„‚)
773, 4, 67pwselbasb 17430 . . . . . . . . . . . . . 14 ((β„‚fld ∈ Ring ∧ β„‚ ∈ V) β†’ ((𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)) ↔ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)):β„‚βŸΆβ„‚))
789, 6, 77mp2an 690 . . . . . . . . . . . . 13 ((𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)) ↔ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)):β„‚βŸΆβ„‚)
7976, 78sylibr 233 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)))
80 cnfldmul 20942 . . . . . . . . . . . 12 Β· = (.rβ€˜β„‚fld)
81 eqid 2732 . . . . . . . . . . . 12 (.rβ€˜(β„‚fld ↑s β„‚)) = (.rβ€˜(β„‚fld ↑s β„‚))
823, 67, 68, 69, 74, 79, 80, 81pwsmulrval 17433 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ ((β„‚ Γ— {(π‘Žβ€˜π‘˜)})(.rβ€˜(β„‚fld ↑s β„‚))(𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜))) = ((β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∘f Β· (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜))))
8329adantr 481 . . . . . . . . . . . 12 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ (π‘Žβ€˜π‘˜) ∈ β„‚)
84 fconstmpt 5736 . . . . . . . . . . . . 13 (β„‚ Γ— {(π‘Žβ€˜π‘˜)}) = (𝑧 ∈ β„‚ ↦ (π‘Žβ€˜π‘˜))
8584a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}) = (𝑧 ∈ β„‚ ↦ (π‘Žβ€˜π‘˜)))
86 eqidd 2733 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)) = (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)))
8769, 83, 75, 85, 86offval2 7686 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ ((β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∘f Β· (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜))) = (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
8882, 87eqtrd 2772 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ ((β„‚ Γ— {(π‘Žβ€˜π‘˜)})(.rβ€˜(β„‚fld ↑s β„‚))(𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜))) = (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
8963adantr 481 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)))
90 eqid 2732 . . . . . . . . . . . . . 14 (algScβ€˜(Poly1β€˜β„‚fld)) = (algScβ€˜(Poly1β€˜β„‚fld))
9153, 54, 4, 90evl1sca 21844 . . . . . . . . . . . . 13 ((β„‚fld ∈ CRing ∧ (π‘Žβ€˜π‘˜) ∈ β„‚) β†’ (πΈβ€˜((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜))) = (β„‚ Γ— {(π‘Žβ€˜π‘˜)}))
9252, 29, 91sylancr 587 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜))) = (β„‚ Γ— {(π‘Žβ€˜π‘˜)}))
93 eqid 2732 . . . . . . . . . . . . . . . 16 (Baseβ€˜(Poly1β€˜β„‚fld)) = (Baseβ€˜(Poly1β€˜β„‚fld))
9493, 67rhmf 20255 . . . . . . . . . . . . . . 15 (𝐸 ∈ ((Poly1β€˜β„‚fld) RingHom (β„‚fld ↑s β„‚)) β†’ 𝐸:(Baseβ€˜(Poly1β€˜β„‚fld))⟢(Baseβ€˜(β„‚fld ↑s β„‚)))
9556, 94ax-mp 5 . . . . . . . . . . . . . 14 𝐸:(Baseβ€˜(Poly1β€˜β„‚fld))⟢(Baseβ€˜(β„‚fld ↑s β„‚))
96 ffn 6714 . . . . . . . . . . . . . 14 (𝐸:(Baseβ€˜(Poly1β€˜β„‚fld))⟢(Baseβ€˜(β„‚fld ↑s β„‚)) β†’ 𝐸 Fn (Baseβ€˜(Poly1β€˜β„‚fld)))
9795, 96mp1i 13 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ 𝐸 Fn (Baseβ€˜(Poly1β€˜β„‚fld)))
9893subrgss 20356 . . . . . . . . . . . . . . 15 (𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld)) β†’ 𝐴 βŠ† (Baseβ€˜(Poly1β€˜β„‚fld)))
9960, 98syl 17 . . . . . . . . . . . . . 14 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 𝐴 βŠ† (Baseβ€˜(Poly1β€˜β„‚fld)))
10099ad2antrr 724 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ 𝐴 βŠ† (Baseβ€˜(Poly1β€˜β„‚fld)))
101 simpll 765 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ 𝑆 ∈ (SubRingβ€˜β„‚fld))
10254, 90, 57, 58, 101, 59, 4, 29subrg1asclcl 21773 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜)) ∈ 𝐴 ↔ (π‘Žβ€˜π‘˜) ∈ 𝑆))
10328, 102mpbird 256 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ ((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜)) ∈ 𝐴)
104 fnfvima 7231 . . . . . . . . . . . . 13 ((𝐸 Fn (Baseβ€˜(Poly1β€˜β„‚fld)) ∧ 𝐴 βŠ† (Baseβ€˜(Poly1β€˜β„‚fld)) ∧ ((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜)) ∈ 𝐴) β†’ (πΈβ€˜((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜))) ∈ (𝐸 β€œ 𝐴))
10597, 100, 103, 104syl3anc 1371 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜))) ∈ (𝐸 β€œ 𝐴))
10692, 105eqeltrrd 2834 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∈ (𝐸 β€œ 𝐴))
10767subrgss 20356 . . . . . . . . . . . . . . . . 17 ((𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)) β†’ (𝐸 β€œ 𝐴) βŠ† (Baseβ€˜(β„‚fld ↑s β„‚)))
10889, 107syl 17 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝐸 β€œ 𝐴) βŠ† (Baseβ€˜(β„‚fld ↑s β„‚)))
10960ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ 𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld)))
110 eqid 2732 . . . . . . . . . . . . . . . . . . . 20 (mulGrpβ€˜(Poly1β€˜β„‚fld)) = (mulGrpβ€˜(Poly1β€˜β„‚fld))
111110subrgsubm 20368 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld)) β†’ 𝐴 ∈ (SubMndβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld))))
112109, 111syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ 𝐴 ∈ (SubMndβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld))))
11326adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ π‘˜ ∈ β„•0)
114 eqid 2732 . . . . . . . . . . . . . . . . . . 19 (var1β€˜β„‚fld) = (var1β€˜β„‚fld)
115114, 101, 57, 58, 59subrgvr1cl 21775 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (var1β€˜β„‚fld) ∈ 𝐴)
116 eqid 2732 . . . . . . . . . . . . . . . . . . 19 (.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld))) = (.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))
117116submmulgcl 18991 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ (SubMndβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld))) ∧ π‘˜ ∈ β„•0 ∧ (var1β€˜β„‚fld) ∈ 𝐴) β†’ (π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)) ∈ 𝐴)
118112, 113, 115, 117syl3anc 1371 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)) ∈ 𝐴)
119 fnfvima 7231 . . . . . . . . . . . . . . . . 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}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))) ∈ (𝐸 β€œ 𝐴))
121108, 120sseldd 3982 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)))
1223, 4, 67, 68, 69, 121pwselbas 17431 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))):β„‚βŸΆβ„‚)
123122feqmptd 6957 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))) = (𝑧 ∈ β„‚ ↦ ((πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))β€˜π‘§)))
12452a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ β„‚fld ∈ CRing)
125 simpr 485 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ 𝑧 ∈ β„‚)
12653, 114, 4, 54, 93, 124, 125evl1vard 21847 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ ((var1β€˜β„‚fld) ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) ∧ ((πΈβ€˜(var1β€˜β„‚fld))β€˜π‘§) = 𝑧))
127 eqid 2732 . . . . . . . . . . . . . . . . 17 (.gβ€˜(mulGrpβ€˜β„‚fld)) = (.gβ€˜(mulGrpβ€˜β„‚fld))
128113adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ π‘˜ ∈ β„•0)
12953, 54, 4, 93, 124, 125, 126, 116, 127, 128evl1expd 21855 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ ((π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)) ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) ∧ ((πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))β€˜π‘§) = (π‘˜(.gβ€˜(mulGrpβ€˜β„‚fld))𝑧)))
130129simprd 496 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ ((πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))β€˜π‘§) = (π‘˜(.gβ€˜(mulGrpβ€˜β„‚fld))𝑧))
131 cnfldexp 20970 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ β„‚ ∧ π‘˜ ∈ β„•0) β†’ (π‘˜(.gβ€˜(mulGrpβ€˜β„‚fld))𝑧) = (π‘§β†‘π‘˜))
132125, 128, 131syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ (π‘˜(.gβ€˜(mulGrpβ€˜β„‚fld))𝑧) = (π‘§β†‘π‘˜))
133130, 132eqtrd 2772 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ ((πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))β€˜π‘§) = (π‘§β†‘π‘˜))
134133mpteq2dva 5247 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ ((πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))β€˜π‘§)) = (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)))
135123, 134eqtrd 2772 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))) = (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)))
136135, 120eqeltrrd 2834 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)) ∈ (𝐸 β€œ 𝐴))
13781subrgmcl 20367 . . . . . . . . . . 11 (((𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)) ∧ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∈ (𝐸 β€œ 𝐴) ∧ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)) ∈ (𝐸 β€œ 𝐴)) β†’ ((β„‚ Γ— {(π‘Žβ€˜π‘˜)})(.rβ€˜(β„‚fld ↑s β„‚))(𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜))) ∈ (𝐸 β€œ 𝐴))
13889, 106, 136, 137syl3anc 1371 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ ((β„‚ Γ— {(π‘Žβ€˜π‘˜)})(.rβ€˜(β„‚fld ↑s β„‚))(𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜))) ∈ (𝐸 β€œ 𝐴))
13988, 138eqeltrrd 2834 . . . . . . . . 9 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ (𝐸 β€œ 𝐴))
140139fmpttd 7111 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))):(0...𝑛)⟢(𝐸 β€œ 𝐴))
14136, 8, 139, 40fsuppmptdm 9370 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))) finSupp (0gβ€˜(β„‚fld ↑s β„‚)))
1425, 51, 8, 66, 140, 141gsumsubmcl 19781 . . . . . . 7 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))) ∈ (𝐸 β€œ 𝐴))
14347, 142eqeltrrd 2834 . . . . . 6 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ (𝐸 β€œ 𝐴))
144 eleq1 2821 . . . . . 6 (𝑓 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) β†’ (𝑓 ∈ (𝐸 β€œ 𝐴) ↔ (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ (𝐸 β€œ 𝐴)))
145143, 144syl5ibrcom 246 . . . . 5 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝑓 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) β†’ 𝑓 ∈ (𝐸 β€œ 𝐴)))
146145rexlimdvva 3211 . . . 4 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (βˆƒπ‘› ∈ β„•0 βˆƒπ‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0)𝑓 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) β†’ 𝑓 ∈ (𝐸 β€œ 𝐴)))
1472, 146syl5 34 . . 3 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (𝑓 ∈ (Polyβ€˜π‘†) β†’ 𝑓 ∈ (𝐸 β€œ 𝐴)))
148 ffun 6717 . . . . . 6 (𝐸:(Baseβ€˜(Poly1β€˜β„‚fld))⟢(Baseβ€˜(β„‚fld ↑s β„‚)) β†’ Fun 𝐸)
14995, 148ax-mp 5 . . . . 5 Fun 𝐸
150 fvelima 6954 . . . . 5 ((Fun 𝐸 ∧ 𝑓 ∈ (𝐸 β€œ 𝐴)) β†’ βˆƒπ‘Ž ∈ 𝐴 (πΈβ€˜π‘Ž) = 𝑓)
151149, 150mpan 688 . . . 4 (𝑓 ∈ (𝐸 β€œ 𝐴) β†’ βˆƒπ‘Ž ∈ 𝐴 (πΈβ€˜π‘Ž) = 𝑓)
15299sselda 3981 . . . . . . . . . . 11 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld)))
153 eqid 2732 . . . . . . . . . . . 12 ( ·𝑠 β€˜(Poly1β€˜β„‚fld)) = ( ·𝑠 β€˜(Poly1β€˜β„‚fld))
154 eqid 2732 . . . . . . . . . . . 12 (coe1β€˜π‘Ž) = (coe1β€˜π‘Ž)
15554, 114, 93, 153, 110, 116, 154ply1coe 21811 . . . . . . . . . . 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 6892 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (πΈβ€˜π‘Ž) = (πΈβ€˜((Poly1β€˜β„‚fld) Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))))))
158 eqid 2732 . . . . . . . . . 10 (0gβ€˜(Poly1β€˜β„‚fld)) = (0gβ€˜(Poly1β€˜β„‚fld))
15954ply1ring 21761 . . . . . . . . . . . 12 (β„‚fld ∈ Ring β†’ (Poly1β€˜β„‚fld) ∈ Ring)
1609, 159ax-mp 5 . . . . . . . . . . 11 (Poly1β€˜β„‚fld) ∈ Ring
161 ringcmn 20092 . . . . . . . . . . 11 ((Poly1β€˜β„‚fld) ∈ Ring β†’ (Poly1β€˜β„‚fld) ∈ CMnd)
162160, 161mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (Poly1β€˜β„‚fld) ∈ CMnd)
163 ringmnd 20059 . . . . . . . . . . 11 ((β„‚fld ↑s β„‚) ∈ Ring β†’ (β„‚fld ↑s β„‚) ∈ Mnd)
16449, 163mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (β„‚fld ↑s β„‚) ∈ Mnd)
165 nn0ex 12474 . . . . . . . . . . 11 β„•0 ∈ V
166165a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ β„•0 ∈ V)
167 rhmghm 20254 . . . . . . . . . . . 12 (𝐸 ∈ ((Poly1β€˜β„‚fld) RingHom (β„‚fld ↑s β„‚)) β†’ 𝐸 ∈ ((Poly1β€˜β„‚fld) GrpHom (β„‚fld ↑s β„‚)))
16856, 167ax-mp 5 . . . . . . . . . . 11 𝐸 ∈ ((Poly1β€˜β„‚fld) GrpHom (β„‚fld ↑s β„‚))
169 ghmmhm 19096 . . . . . . . . . . 11 (𝐸 ∈ ((Poly1β€˜β„‚fld) GrpHom (β„‚fld ↑s β„‚)) β†’ 𝐸 ∈ ((Poly1β€˜β„‚fld) MndHom (β„‚fld ↑s β„‚)))
170168, 169mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ 𝐸 ∈ ((Poly1β€˜β„‚fld) MndHom (β„‚fld ↑s β„‚)))
17154ply1lmod 21765 . . . . . . . . . . . . 13 (β„‚fld ∈ Ring β†’ (Poly1β€˜β„‚fld) ∈ LMod)
1729, 171mp1i 13 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (Poly1β€˜β„‚fld) ∈ LMod)
17312ad2antrr 724 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ 𝑆 βŠ† β„‚)
174 eqid 2732 . . . . . . . . . . . . . . . . 17 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
175154, 59, 58, 174coe1f 21726 . . . . . . . . . . . . . . . 16 (π‘Ž ∈ 𝐴 β†’ (coe1β€˜π‘Ž):β„•0⟢(Baseβ€˜π‘…))
17657subrgbas 20364 . . . . . . . . . . . . . . . . 17 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 𝑆 = (Baseβ€˜π‘…))
177176feq3d 6701 . . . . . . . . . . . . . . . 16 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ ((coe1β€˜π‘Ž):β„•0βŸΆπ‘† ↔ (coe1β€˜π‘Ž):β„•0⟢(Baseβ€˜π‘…)))
178175, 177imbitrrid 245 . . . . . . . . . . . . . . 15 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (π‘Ž ∈ 𝐴 β†’ (coe1β€˜π‘Ž):β„•0βŸΆπ‘†))
179178imp 407 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (coe1β€˜π‘Ž):β„•0βŸΆπ‘†)
180179ffvelcdmda 7083 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ ((coe1β€˜π‘Ž)β€˜π‘˜) ∈ 𝑆)
181173, 180sseldd 3982 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ ((coe1β€˜π‘Ž)β€˜π‘˜) ∈ β„‚)
182110, 93mgpbas 19987 . . . . . . . . . . . . 13 (Baseβ€˜(Poly1β€˜β„‚fld)) = (Baseβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))
183110ringmgp 20055 . . . . . . . . . . . . . 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 21732 . . . . . . . . . . . . . 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 18969 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)) ∈ (Baseβ€˜(Poly1β€˜β„‚fld)))
18954ply1sca 21766 . . . . . . . . . . . . . 14 (β„‚fld ∈ Ring β†’ β„‚fld = (Scalarβ€˜(Poly1β€˜β„‚fld)))
1909, 189ax-mp 5 . . . . . . . . . . . . 13 β„‚fld = (Scalarβ€˜(Poly1β€˜β„‚fld))
19193, 190, 153, 4lmodvscl 20481 . . . . . . . . . . . 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 7111 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))):β„•0⟢(Baseβ€˜(Poly1β€˜β„‚fld)))
194165mptex 7221 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))) ∈ V
195 funmpt 6583 . . . . . . . . . . . . 13 Fun (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))
196 fvex 6901 . . . . . . . . . . . . 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 21728 . . . . . . . . . . . . 13 (π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) β†’ (coe1β€˜π‘Ž) finSupp 0)
200152, 199syl 17 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (coe1β€˜π‘Ž) finSupp 0)
201200fsuppimpd 9365 . . . . . . . . . . 11 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((coe1β€˜π‘Ž) supp 0) ∈ Fin)
202179feqmptd 6957 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (coe1β€˜π‘Ž) = (π‘˜ ∈ β„•0 ↦ ((coe1β€˜π‘Ž)β€˜π‘˜)))
203202oveq1d 7420 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((coe1β€˜π‘Ž) supp 0) = ((π‘˜ ∈ β„•0 ↦ ((coe1β€˜π‘Ž)β€˜π‘˜)) supp 0))
204 eqimss2 4040 . . . . . . . . . . . . 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 20497 . . . . . . . . . . . . 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 11204 . . . . . . . . . . . . 13 0 ∈ V
210209a1i 11 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ 0 ∈ V)
211205, 208, 180, 188, 210suppssov1 8179 . . . . . . . . . . 11 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))) supp (0gβ€˜(Poly1β€˜β„‚fld))) βŠ† ((coe1β€˜π‘Ž) supp 0))
212 suppssfifsupp 9374 . . . . . . . . . . 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 19800 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((β„‚fld ↑s β„‚) Ξ£g (𝐸 ∘ (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))))) = (πΈβ€˜((Poly1β€˜β„‚fld) Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))))))
21595a1i 11 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ 𝐸:(Baseβ€˜(Poly1β€˜β„‚fld))⟢(Baseβ€˜(β„‚fld ↑s β„‚)))
216215, 192cofmpt 7126 . . . . . . . . . . 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 7082 . . . . . . . . . . . . . . . 16 ((((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))) ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) β†’ (πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)))
220192, 219syl 17 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)))
2213, 4, 67, 217, 218, 220pwselbas 17431 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))):β„‚βŸΆβ„‚)
222221feqmptd 6957 . . . . . . . . . . . . 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 21847 . . . . . . . . . . . . . . . . . 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 21855 . . . . . . . . . . . . . . . . 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 2743 . . . . . . . . . . . . . . . . . 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 21854 . . . . . . . . . . . . . . 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 5247 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (𝑧 ∈ β„‚ ↦ ((πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))β€˜π‘§)) = (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
236222, 235eqtrd 2772 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))) = (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
237236mpteq2dva 5247 . . . . . . . . . . 11 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (π‘˜ ∈ β„•0 ↦ (πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))) = (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))))
238216, 237eqtrd 2772 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (𝐸 ∘ (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))) = (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))))
239238oveq2d 7421 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((β„‚fld ↑s β„‚) Ξ£g (𝐸 ∘ (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))))) = ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))))
240157, 214, 2393eqtr2d 2778 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (πΈβ€˜π‘Ž) = ((β„‚fld ↑s β„‚) Ξ£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 11230 . . . . . . . . . 10 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ β„•0) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)) ∈ β„‚)
246245anasss 467 . . . . . . . . 9 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ (𝑧 ∈ β„‚ ∧ π‘˜ ∈ β„•0)) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)) ∈ β„‚)
247165mptex 7221 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) ∈ V
248 funmpt 6583 . . . . . . . . . . . 12 Fun (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
249247, 248, 393pm3.2i 1339 . . . . . . . . . . 11 ((π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) ∈ V ∧ Fun (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) ∧ (0gβ€˜(β„‚fld ↑s β„‚)) ∈ V)
250249a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) ∈ V ∧ Fun (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) ∧ (0gβ€˜(β„‚fld ↑s β„‚)) ∈ V))
251 fzfid 13934 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)) ∈ Fin)
252 eldifn 4126 . . . . . . . . . . . . . . . . . 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 4125 . . . . . . . . . . . . . . . . . . . . . . 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 2732 . . . . . . . . . . . . . . . . . . . . . . . 24 ( deg1 β€˜β„‚fld) = ( deg1 β€˜β„‚fld)
258257, 54, 93, 17, 154deg1ge 25607 . . . . . . . . . . . . . . . . . . . . . . 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 11257 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℝ*
262257, 54, 93deg1xrcl 25591 . . . . . . . . . . . . . . . . . . . . . . . . 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 13151 . . . . . . . . . . . . . . . . . . . . . . 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 12529 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ π‘˜ ∈ ℝ)
268267rexrd 11260 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ π‘˜ ∈ ℝ*)
269 ifcl 4572 . . . . . . . . . . . . . . . . . . . . . . . 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 13133 . . . . . . . . . . . . . . . . . . . . . . 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 25592 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ (β„•0 βˆͺ {-∞}))
277152, 276syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ (β„•0 βˆͺ {-∞}))
278 elun 4147 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ (β„•0 βˆͺ {-∞}) ↔ ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ β„•0 ∨ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞}))
279277, 278sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ β„•0 ∨ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞}))
280 nn0ge0 12493 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ β„•0 β†’ 0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž))
281280iftrued 4535 . . . . . . . . . . . . . . . . . . . . . . . 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 2833 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ β„•0 β†’ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0) ∈ β„•0)
284 mnflt0 13101 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -∞ < 0
285 mnfxr 11267 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 -∞ ∈ ℝ*
286 xrltnle 11277 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*) β†’ (-∞ < 0 ↔ Β¬ 0 ≀ -∞))
287285, 261, 286mp2an 690 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (-∞ < 0 ↔ Β¬ 0 ≀ -∞)
288284, 287mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Β¬ 0 ≀ -∞
289 elsni 4644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞} β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) = -∞)
290289breq2d 5159 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞} β†’ (0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ↔ 0 ≀ -∞))
291288, 290mtbiri 326 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞} β†’ Β¬ 0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž))
292291iffalsed 4538 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞} β†’ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0) = 0)
293 0nn0 12483 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ β„•0
294292, 293eqeltrdi 2841 . . . . . . . . . . . . . . . . . . . . . . 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 13589 . . . . . . . . . . . . . . . . . . . 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 2958 . . . . . . . . . . . . . . . . 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 7420 . . . . . . . . . . . . . . 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 11408 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (0 Β· (π‘§β†‘π‘˜)) = 0)
306303, 305eqtrd 2772 . . . . . . . . . . . . . 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 5247 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) = (𝑧 ∈ β„‚ ↦ 0))
309 fconstmpt 5736 . . . . . . . . . . . . 13 (β„‚ Γ— {0}) = (𝑧 ∈ β„‚ ↦ 0)
310 ringmnd 20059 . . . . . . . . . . . . . . 15 (β„‚fld ∈ Ring β†’ β„‚fld ∈ Mnd)
3119, 310ax-mp 5 . . . . . . . . . . . . . 14 β„‚fld ∈ Mnd
3123, 17pws0g 18657 . . . . . . . . . . . . . 14 ((β„‚fld ∈ Mnd ∧ β„‚ ∈ V) β†’ (β„‚ Γ— {0}) = (0gβ€˜(β„‚fld ↑s β„‚)))
313311, 6, 312mp2an 690 . . . . . . . . . . . . 13 (β„‚ Γ— {0}) = (0gβ€˜(β„‚fld ↑s β„‚))
314309, 313eqtr3i 2762 . . . . . . . . . . . 12 (𝑧 ∈ β„‚ ↦ 0) = (0gβ€˜(β„‚fld ↑s β„‚))
315308, 314eqtrdi 2788 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) = (0gβ€˜(β„‚fld ↑s β„‚)))
316315, 166suppss2 8181 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) supp (0gβ€˜(β„‚fld ↑s β„‚))) βŠ† (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))
317 suppssfifsupp 9374 . . . . . . . . . 10 ((((π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) ∈ V ∧ Fun (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) ∧ (0gβ€˜(β„‚fld ↑s β„‚)) ∈ V) ∧ ((0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)) ∈ Fin ∧ ((π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) supp (0gβ€˜(β„‚fld ↑s β„‚))) βŠ† (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) finSupp (0gβ€˜(β„‚fld ↑s β„‚)))
318250, 251, 316, 317syl12anc 835 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) finSupp (0gβ€˜(β„‚fld ↑s β„‚)))
3193, 4, 5, 241, 166, 242, 246, 318pwsgsum 19844 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))) = (𝑧 ∈ β„‚ ↦ (β„‚fld Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))))
320 fz0ssnn0 13592 . . . . . . . . . . . 12 (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)) βŠ† β„•0
321 resmpt 6035 . . . . . . . . . . . 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 7416 . . . . . . . . . 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 7111 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))):β„•0βŸΆβ„‚)
327306, 325suppss2 8181 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ ((π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) supp 0) βŠ† (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))
328165mptex 7221 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ V
329 funmpt 6583 . . . . . . . . . . . . . 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 13934 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)) ∈ Fin)
333 suppssfifsupp 9374 . . . . . . . . . . . 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 19775 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ (β„‚fld Ξ£g ((π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) β†Ύ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) = (β„‚fld Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))))
336 elfznn0 13590 . . . . . . . . . . . 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 21004 . . . . . . . . . 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 2796 . . . . . . . . 9 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ (β„‚fld Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) = Ξ£π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))(((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))
340339mpteq2dva 5247 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (𝑧 ∈ β„‚ ↦ (β„‚fld Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))) = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))(((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
341240, 319, 3403eqtrd 2776 . . . . . . 7 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (πΈβ€˜π‘Ž) = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))(((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
34212adantr 481 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ 𝑆 βŠ† β„‚)
343 elplyr 25706 . . . . . . . 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 2833 . . . . . 6 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (πΈβ€˜π‘Ž) ∈ (Polyβ€˜π‘†))
346 eleq1 2821 . . . . . 6 ((πΈβ€˜π‘Ž) = 𝑓 β†’ ((πΈβ€˜π‘Ž) ∈ (Polyβ€˜π‘†) ↔ 𝑓 ∈ (Polyβ€˜π‘†)))
347345, 346syl5ibcom 244 . . . . 5 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((πΈβ€˜π‘Ž) = 𝑓 β†’ 𝑓 ∈ (Polyβ€˜π‘†)))
348347rexlimdva 3155 . . . 4 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (βˆƒπ‘Ž ∈ 𝐴 (πΈβ€˜π‘Ž) = 𝑓 β†’ 𝑓 ∈ (Polyβ€˜π‘†)))
349151, 348syl5 34 . . 3 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (𝑓 ∈ (𝐸 β€œ 𝐴) β†’ 𝑓 ∈ (Polyβ€˜π‘†)))
350147, 349impbid 211 . 2 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (𝑓 ∈ (Polyβ€˜π‘†) ↔ 𝑓 ∈ (𝐸 β€œ 𝐴)))
351350eqrdv 2730 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 2940  βˆƒwrex 3070  Vcvv 3474   βˆ– cdif 3944   βˆͺ cun 3945   βŠ† wss 3947  ifcif 4527  {csn 4627   class class class wbr 5147   ↦ cmpt 5230   Γ— cxp 5673   β†Ύ cres 5677   β€œ cima 5678   ∘ ccom 5679  Fun wfun 6534   Fn wfn 6535  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405   ∘f cof 7664   supp csupp 8142   ↑m cmap 8816  Fincfn 8935   finSupp cfsupp 9357  β„‚cc 11104  0cc0 11106   Β· cmul 11111  -∞cmnf 11242  β„*cxr 11243   < clt 11244   ≀ cle 11245  β„•0cn0 12468  ...cfz 13480  β†‘cexp 14023  Ξ£csu 15628  Basecbs 17140   β†Ύs cress 17169  .rcmulr 17194  Scalarcsca 17196   ·𝑠 cvsca 17197  0gc0g 17381   Ξ£g cgsu 17382   ↑s cpws 17388  Mndcmnd 18621   MndHom cmhm 18665  SubMndcsubmnd 18666  .gcmg 18944  SubGrpcsubg 18994   GrpHom cghm 19083  CMndccmn 19642  mulGrpcmgp 19981  Ringcrg 20049  CRingccrg 20050   RingHom crh 20240  SubRingcsubrg 20351  LModclmod 20463  β„‚fldccnfld 20936  algSccascl 21398  var1cv1 21691  Poly1cpl1 21692  coe1cco1 21693  eval1ce1 21824   deg1 cdg1 25560  Polycply 25689
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 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186
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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-ofr 7667  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8143  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-sup 9433  df-oi 9501  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-rp 12971  df-fz 13481  df-fzo 13624  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428  df-sum 15629  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-0g 17383  df-gsum 17384  df-prds 17389  df-pws 17391  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-mhm 18667  df-submnd 18668  df-grp 18818  df-minusg 18819  df-sbg 18820  df-mulg 18945  df-subg 18997  df-ghm 19084  df-cntz 19175  df-cmn 19644  df-abl 19645  df-mgp 19982  df-ur 19999  df-srg 20003  df-ring 20051  df-cring 20052  df-rnghom 20243  df-subrg 20353  df-lmod 20465  df-lss 20535  df-lsp 20575  df-cnfld 20937  df-assa 21399  df-asp 21400  df-ascl 21401  df-psr 21453  df-mvr 21454  df-mpl 21455  df-opsr 21457  df-evls 21626  df-evl 21627  df-psr1 21695  df-vr1 21696  df-ply1 21697  df-coe1 21698  df-evl1 21826  df-mdeg 25561  df-deg1 25562  df-ply 25693
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator