MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  plypf1 Structured version   Visualization version   GIF version
Theorem plypf1 26166
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 26149 . . . . 5 (𝑓 ∈ (Polyβ€˜π‘†) ↔ (𝑆 βŠ† β„‚ ∧ βˆƒπ‘› ∈ β„•0 βˆƒπ‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0)𝑓 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))))
21simprbi 495 . . . 4 (𝑓 ∈ (Polyβ€˜π‘†) β†’ βˆƒπ‘› ∈ β„•0 βˆƒπ‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0)𝑓 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
3 eqid 2728 . . . . . . . . 9 (β„‚fld ↑s β„‚) = (β„‚fld ↑s β„‚)
4 cnfldbas 21290 . . . . . . . . 9 β„‚ = (Baseβ€˜β„‚fld)
5 eqid 2728 . . . . . . . . 9 (0gβ€˜(β„‚fld ↑s β„‚)) = (0gβ€˜(β„‚fld ↑s β„‚))
6 cnex 11227 . . . . . . . . . 10 β„‚ ∈ V
76a1i 11 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ β„‚ ∈ V)
8 fzfid 13978 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (0...𝑛) ∈ Fin)
9 cnring 21325 . . . . . . . . . 10 β„‚fld ∈ Ring
10 ringcmn 20225 . . . . . . . . . 10 (β„‚fld ∈ Ring β†’ β„‚fld ∈ CMnd)
119, 10mp1i 13 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ β„‚fld ∈ CMnd)
124subrgss 20518 . . . . . . . . . . . . 13 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 𝑆 βŠ† β„‚)
1312ad2antrr 724 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ 𝑆 βŠ† β„‚)
14 elmapi 8874 . . . . . . . . . . . . . . 15 (π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0) β†’ π‘Ž:β„•0⟢(𝑆 βˆͺ {0}))
1514ad2antll 727 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ π‘Ž:β„•0⟢(𝑆 βˆͺ {0}))
16 subrgsubg 20523 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 𝑆 ∈ (SubGrpβ€˜β„‚fld))
17 cnfld0 21327 . . . . . . . . . . . . . . . . . . . 20 0 = (0gβ€˜β„‚fld)
1817subg0cl 19096 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ (SubGrpβ€˜β„‚fld) β†’ 0 ∈ 𝑆)
1916, 18syl 17 . . . . . . . . . . . . . . . . . 18 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 0 ∈ 𝑆)
2019adantr 479 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ 0 ∈ 𝑆)
2120snssd 4817 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ {0} βŠ† 𝑆)
22 ssequn2 4185 . . . . . . . . . . . . . . . 16 ({0} βŠ† 𝑆 ↔ (𝑆 βˆͺ {0}) = 𝑆)
2321, 22sylib 217 . . . . . . . . . . . . . . 15 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝑆 βˆͺ {0}) = 𝑆)
2423feq3d 6714 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (π‘Ž:β„•0⟢(𝑆 βˆͺ {0}) ↔ π‘Ž:β„•0βŸΆπ‘†))
2515, 24mpbid 231 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ π‘Ž:β„•0βŸΆπ‘†)
26 elfznn0 13634 . . . . . . . . . . . . 13 (π‘˜ ∈ (0...𝑛) β†’ π‘˜ ∈ β„•0)
27 ffvelcdm 7096 . . . . . . . . . . . . 13 ((π‘Ž:β„•0βŸΆπ‘† ∧ π‘˜ ∈ β„•0) β†’ (π‘Žβ€˜π‘˜) ∈ 𝑆)
2825, 26, 27syl2an 594 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (π‘Žβ€˜π‘˜) ∈ 𝑆)
2913, 28sseldd 3983 . . . . . . . . . . 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 14084 . . . . . . . . . . 11 ((𝑧 ∈ β„‚ ∧ π‘˜ ∈ β„•0) β†’ (π‘§β†‘π‘˜) ∈ β„‚)
3431, 32, 33syl2anc 582 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ (𝑧 ∈ β„‚ ∧ π‘˜ ∈ (0...𝑛))) β†’ (π‘§β†‘π‘˜) ∈ β„‚)
3530, 34mulcld 11272 . . . . . . . . 9 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ (𝑧 ∈ β„‚ ∧ π‘˜ ∈ (0...𝑛))) β†’ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)) ∈ β„‚)
36 eqid 2728 . . . . . . . . . 10 (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))) = (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
376mptex 7241 . . . . . . . . . . 11 (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ V
3837a1i 11 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ V)
39 fvex 6915 . . . . . . . . . . 11 (0gβ€˜(β„‚fld ↑s β„‚)) ∈ V
4039a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (0gβ€˜(β„‚fld ↑s β„‚)) ∈ V)
4136, 8, 38, 40fsuppmptdm 9407 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))) finSupp (0gβ€˜(β„‚fld ↑s β„‚)))
423, 4, 5, 7, 8, 11, 35, 41pwsgsum 19944 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))) = (𝑧 ∈ β„‚ ↦ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑛) ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))))
43 fzfid 13978 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ 𝑧 ∈ β„‚) β†’ (0...𝑛) ∈ Fin)
4435anassrs 466 . . . . . . . . . 10 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (0...𝑛)) β†’ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)) ∈ β„‚)
4543, 44gsumfsum 21374 . . . . . . . . 9 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ 𝑧 ∈ β„‚) β†’ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑛) ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))) = Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))
4645mpteq2dva 5252 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝑧 ∈ β„‚ ↦ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑛) ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))) = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
4742, 46eqtrd 2768 . . . . . . 7 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))) = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
483pwsring 20267 . . . . . . . . . 10 ((β„‚fld ∈ Ring ∧ β„‚ ∈ V) β†’ (β„‚fld ↑s β„‚) ∈ Ring)
499, 6, 48mp2an 690 . . . . . . . . 9 (β„‚fld ↑s β„‚) ∈ Ring
50 ringcmn 20225 . . . . . . . . 9 ((β„‚fld ↑s β„‚) ∈ Ring β†’ (β„‚fld ↑s β„‚) ∈ CMnd)
5149, 50mp1i 13 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (β„‚fld ↑s β„‚) ∈ CMnd)
52 cncrng 21323 . . . . . . . . . . 11 β„‚fld ∈ CRing
53 plypf1.e . . . . . . . . . . . 12 𝐸 = (eval1β€˜β„‚fld)
54 eqid 2728 . . . . . . . . . . . 12 (Poly1β€˜β„‚fld) = (Poly1β€˜β„‚fld)
5553, 54, 3, 4evl1rhm 22258 . . . . . . . . . . 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 22158 . . . . . . . . . . 11 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld)))
6160adantr 479 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ 𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld)))
62 rhmima 20550 . . . . . . . . . 10 ((𝐸 ∈ ((Poly1β€˜β„‚fld) RingHom (β„‚fld ↑s β„‚)) ∧ 𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld))) β†’ (𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)))
6356, 61, 62sylancr 585 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)))
64 subrgsubg 20523 . . . . . . . . 9 ((𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)) β†’ (𝐸 β€œ 𝐴) ∈ (SubGrpβ€˜(β„‚fld ↑s β„‚)))
65 subgsubm 19110 . . . . . . . . 9 ((𝐸 β€œ 𝐴) ∈ (SubGrpβ€˜(β„‚fld ↑s β„‚)) β†’ (𝐸 β€œ 𝐴) ∈ (SubMndβ€˜(β„‚fld ↑s β„‚)))
6663, 64, 653syl 18 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝐸 β€œ 𝐴) ∈ (SubMndβ€˜(β„‚fld ↑s β„‚)))
67 eqid 2728 . . . . . . . . . . . 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 6791 . . . . . . . . . . . . . 14 ((π‘Žβ€˜π‘˜) ∈ β„‚ β†’ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}):β„‚βŸΆβ„‚)
7129, 70syl 17 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}):β„‚βŸΆβ„‚)
723, 4, 67pwselbasb 17477 . . . . . . . . . . . . . 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 7130 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)):β„‚βŸΆβ„‚)
773, 4, 67pwselbasb 17477 . . . . . . . . . . . . . 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 21294 . . . . . . . . . . . 12 Β· = (.rβ€˜β„‚fld)
81 eqid 2728 . . . . . . . . . . . 12 (.rβ€˜(β„‚fld ↑s β„‚)) = (.rβ€˜(β„‚fld ↑s β„‚))
823, 67, 68, 69, 74, 79, 80, 81pwsmulrval 17480 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ ((β„‚ Γ— {(π‘Žβ€˜π‘˜)})(.rβ€˜(β„‚fld ↑s β„‚))(𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜))) = ((β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∘f Β· (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜))))
8329adantr 479 . . . . . . . . . . . 12 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ (π‘Žβ€˜π‘˜) ∈ β„‚)
84 fconstmpt 5744 . . . . . . . . . . . . 13 (β„‚ Γ— {(π‘Žβ€˜π‘˜)}) = (𝑧 ∈ β„‚ ↦ (π‘Žβ€˜π‘˜))
8584a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}) = (𝑧 ∈ β„‚ ↦ (π‘Žβ€˜π‘˜)))
86 eqidd 2729 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)) = (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)))
8769, 83, 75, 85, 86offval2 7711 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ ((β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∘f Β· (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜))) = (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
8882, 87eqtrd 2768 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ ((β„‚ Γ— {(π‘Žβ€˜π‘˜)})(.rβ€˜(β„‚fld ↑s β„‚))(𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜))) = (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
8963adantr 479 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)))
90 eqid 2728 . . . . . . . . . . . . . 14 (algScβ€˜(Poly1β€˜β„‚fld)) = (algScβ€˜(Poly1β€˜β„‚fld))
9153, 54, 4, 90evl1sca 22260 . . . . . . . . . . . . 13 ((β„‚fld ∈ CRing ∧ (π‘Žβ€˜π‘˜) ∈ β„‚) β†’ (πΈβ€˜((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜))) = (β„‚ Γ— {(π‘Žβ€˜π‘˜)}))
9252, 29, 91sylancr 585 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜))) = (β„‚ Γ— {(π‘Žβ€˜π‘˜)}))
93 eqid 2728 . . . . . . . . . . . . . . . 16 (Baseβ€˜(Poly1β€˜β„‚fld)) = (Baseβ€˜(Poly1β€˜β„‚fld))
9493, 67rhmf 20431 . . . . . . . . . . . . . . 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 6727 . . . . . . . . . . . . . 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 20518 . . . . . . . . . . . . . . 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 22186 . . . . . . . . . . . . . 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 7251 . . . . . . . . . . . . 13 ((𝐸 Fn (Baseβ€˜(Poly1β€˜β„‚fld)) ∧ 𝐴 βŠ† (Baseβ€˜(Poly1β€˜β„‚fld)) ∧ ((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜)) ∈ 𝐴) β†’ (πΈβ€˜((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜))) ∈ (𝐸 β€œ 𝐴))
10597, 100, 103, 104syl3anc 1368 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜))) ∈ (𝐸 β€œ 𝐴))
10692, 105eqeltrrd 2830 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∈ (𝐸 β€œ 𝐴))
10767subrgss 20518 . . . . . . . . . . . . . . . . 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 2728 . . . . . . . . . . . . . . . . . . . 20 (mulGrpβ€˜(Poly1β€˜β„‚fld)) = (mulGrpβ€˜(Poly1β€˜β„‚fld))
111110subrgsubm 20531 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld)) β†’ 𝐴 ∈ (SubMndβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld))))
112109, 111syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ 𝐴 ∈ (SubMndβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld))))
11326adantl 480 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ π‘˜ ∈ β„•0)
114 eqid 2728 . . . . . . . . . . . . . . . . . . 19 (var1β€˜β„‚fld) = (var1β€˜β„‚fld)
115114, 101, 57, 58, 59subrgvr1cl 22188 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (var1β€˜β„‚fld) ∈ 𝐴)
116 eqid 2728 . . . . . . . . . . . . . . . . . . 19 (.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld))) = (.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))
117116submmulgcl 19079 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ (SubMndβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld))) ∧ π‘˜ ∈ β„•0 ∧ (var1β€˜β„‚fld) ∈ 𝐴) β†’ (π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)) ∈ 𝐴)
118112, 113, 115, 117syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)) ∈ 𝐴)
119 fnfvima 7251 . . . . . . . . . . . . . . . . 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}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))) ∈ (𝐸 β€œ 𝐴))
121108, 120sseldd 3983 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)))
1223, 4, 67, 68, 69, 121pwselbas 17478 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))):β„‚βŸΆβ„‚)
123122feqmptd 6972 . . . . . . . . . . . . 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 483 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ 𝑧 ∈ β„‚)
12653, 114, 4, 54, 93, 124, 125evl1vard 22263 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ ((var1β€˜β„‚fld) ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) ∧ ((πΈβ€˜(var1β€˜β„‚fld))β€˜π‘§) = 𝑧))
127 eqid 2728 . . . . . . . . . . . . . . . . 17 (.gβ€˜(mulGrpβ€˜β„‚fld)) = (.gβ€˜(mulGrpβ€˜β„‚fld))
128113adantr 479 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ π‘˜ ∈ β„•0)
12953, 54, 4, 93, 124, 125, 126, 116, 127, 128evl1expd 22271 . . . . . . . . . . . . . . . 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 494 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ ((πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))β€˜π‘§) = (π‘˜(.gβ€˜(mulGrpβ€˜β„‚fld))𝑧))
131 cnfldexp 21339 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ β„‚ ∧ π‘˜ ∈ β„•0) β†’ (π‘˜(.gβ€˜(mulGrpβ€˜β„‚fld))𝑧) = (π‘§β†‘π‘˜))
132125, 128, 131syl2anc 582 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ (π‘˜(.gβ€˜(mulGrpβ€˜β„‚fld))𝑧) = (π‘§β†‘π‘˜))
133130, 132eqtrd 2768 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ ((πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))β€˜π‘§) = (π‘§β†‘π‘˜))
134133mpteq2dva 5252 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ ((πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))β€˜π‘§)) = (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)))
135123, 134eqtrd 2768 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))) = (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)))
136135, 120eqeltrrd 2830 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)) ∈ (𝐸 β€œ 𝐴))
13781subrgmcl 20530 . . . . . . . . . . 11 (((𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)) ∧ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∈ (𝐸 β€œ 𝐴) ∧ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)) ∈ (𝐸 β€œ 𝐴)) β†’ ((β„‚ Γ— {(π‘Žβ€˜π‘˜)})(.rβ€˜(β„‚fld ↑s β„‚))(𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜))) ∈ (𝐸 β€œ 𝐴))
13889, 106, 136, 137syl3anc 1368 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ ((β„‚ Γ— {(π‘Žβ€˜π‘˜)})(.rβ€˜(β„‚fld ↑s β„‚))(𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜))) ∈ (𝐸 β€œ 𝐴))
13988, 138eqeltrrd 2830 . . . . . . . . 9 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ (𝐸 β€œ 𝐴))
140139fmpttd 7130 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))):(0...𝑛)⟢(𝐸 β€œ 𝐴))
14136, 8, 139, 40fsuppmptdm 9407 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))) finSupp (0gβ€˜(β„‚fld ↑s β„‚)))
1425, 51, 8, 66, 140, 141gsumsubmcl 19881 . . . . . . 7 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))) ∈ (𝐸 β€œ 𝐴))
14347, 142eqeltrrd 2830 . . . . . 6 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ (𝐸 β€œ 𝐴))
144 eleq1 2817 . . . . . 6 (𝑓 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) β†’ (𝑓 ∈ (𝐸 β€œ 𝐴) ↔ (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ (𝐸 β€œ 𝐴)))
145143, 144syl5ibrcom 246 . . . . 5 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝑓 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) β†’ 𝑓 ∈ (𝐸 β€œ 𝐴)))
146145rexlimdvva 3209 . . . 4 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (βˆƒπ‘› ∈ β„•0 βˆƒπ‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0)𝑓 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) β†’ 𝑓 ∈ (𝐸 β€œ 𝐴)))
1472, 146syl5 34 . . 3 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (𝑓 ∈ (Polyβ€˜π‘†) β†’ 𝑓 ∈ (𝐸 β€œ 𝐴)))
148 ffun 6730 . . . . . 6 (𝐸:(Baseβ€˜(Poly1β€˜β„‚fld))⟢(Baseβ€˜(β„‚fld ↑s β„‚)) β†’ Fun 𝐸)
14995, 148ax-mp 5 . . . . 5 Fun 𝐸
150 fvelima 6969 . . . . 5 ((Fun 𝐸 ∧ 𝑓 ∈ (𝐸 β€œ 𝐴)) β†’ βˆƒπ‘Ž ∈ 𝐴 (πΈβ€˜π‘Ž) = 𝑓)
151149, 150mpan 688 . . . 4 (𝑓 ∈ (𝐸 β€œ 𝐴) β†’ βˆƒπ‘Ž ∈ 𝐴 (πΈβ€˜π‘Ž) = 𝑓)
15299sselda 3982 . . . . . . . . . . 11 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld)))
153 eqid 2728 . . . . . . . . . . . 12 ( ·𝑠 β€˜(Poly1β€˜β„‚fld)) = ( ·𝑠 β€˜(Poly1β€˜β„‚fld))
154 eqid 2728 . . . . . . . . . . . 12 (coe1β€˜π‘Ž) = (coe1β€˜π‘Ž)
15554, 114, 93, 153, 110, 116, 154ply1coe 22224 . . . . . . . . . . 11 ((β„‚fld ∈ Ring ∧ π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld))) β†’ π‘Ž = ((Poly1β€˜β„‚fld) Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))))
1569, 152, 155sylancr 585 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ π‘Ž = ((Poly1β€˜β„‚fld) Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))))
157156fveq2d 6906 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (πΈβ€˜π‘Ž) = (πΈβ€˜((Poly1β€˜β„‚fld) Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))))))
158 eqid 2728 . . . . . . . . . 10 (0gβ€˜(Poly1β€˜β„‚fld)) = (0gβ€˜(Poly1β€˜β„‚fld))
15954ply1ring 22173 . . . . . . . . . . . 12 (β„‚fld ∈ Ring β†’ (Poly1β€˜β„‚fld) ∈ Ring)
1609, 159ax-mp 5 . . . . . . . . . . 11 (Poly1β€˜β„‚fld) ∈ Ring
161 ringcmn 20225 . . . . . . . . . . 11 ((Poly1β€˜β„‚fld) ∈ Ring β†’ (Poly1β€˜β„‚fld) ∈ CMnd)
162160, 161mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (Poly1β€˜β„‚fld) ∈ CMnd)
163 ringmnd 20190 . . . . . . . . . . 11 ((β„‚fld ↑s β„‚) ∈ Ring β†’ (β„‚fld ↑s β„‚) ∈ Mnd)
16449, 163mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (β„‚fld ↑s β„‚) ∈ Mnd)
165 nn0ex 12516 . . . . . . . . . . 11 β„•0 ∈ V
166165a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ β„•0 ∈ V)
167 rhmghm 20430 . . . . . . . . . . . 12 (𝐸 ∈ ((Poly1β€˜β„‚fld) RingHom (β„‚fld ↑s β„‚)) β†’ 𝐸 ∈ ((Poly1β€˜β„‚fld) GrpHom (β„‚fld ↑s β„‚)))
16856, 167ax-mp 5 . . . . . . . . . . 11 𝐸 ∈ ((Poly1β€˜β„‚fld) GrpHom (β„‚fld ↑s β„‚))
169 ghmmhm 19187 . . . . . . . . . . 11 (𝐸 ∈ ((Poly1β€˜β„‚fld) GrpHom (β„‚fld ↑s β„‚)) β†’ 𝐸 ∈ ((Poly1β€˜β„‚fld) MndHom (β„‚fld ↑s β„‚)))
170168, 169mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ 𝐸 ∈ ((Poly1β€˜β„‚fld) MndHom (β„‚fld ↑s β„‚)))
17154ply1lmod 22177 . . . . . . . . . . . . 13 (β„‚fld ∈ Ring β†’ (Poly1β€˜β„‚fld) ∈ LMod)
1729, 171mp1i 13 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (Poly1β€˜β„‚fld) ∈ LMod)
17312ad2antrr 724 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ 𝑆 βŠ† β„‚)
174 eqid 2728 . . . . . . . . . . . . . . . . 17 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
175154, 59, 58, 174coe1f 22137 . . . . . . . . . . . . . . . 16 (π‘Ž ∈ 𝐴 β†’ (coe1β€˜π‘Ž):β„•0⟢(Baseβ€˜π‘…))
17657subrgbas 20527 . . . . . . . . . . . . . . . . 17 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 𝑆 = (Baseβ€˜π‘…))
177176feq3d 6714 . . . . . . . . . . . . . . . 16 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ ((coe1β€˜π‘Ž):β„•0βŸΆπ‘† ↔ (coe1β€˜π‘Ž):β„•0⟢(Baseβ€˜π‘…)))
178175, 177imbitrrid 245 . . . . . . . . . . . . . . 15 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (π‘Ž ∈ 𝐴 β†’ (coe1β€˜π‘Ž):β„•0βŸΆπ‘†))
179178imp 405 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (coe1β€˜π‘Ž):β„•0βŸΆπ‘†)
180179ffvelcdmda 7099 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ ((coe1β€˜π‘Ž)β€˜π‘˜) ∈ 𝑆)
181173, 180sseldd 3983 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ ((coe1β€˜π‘Ž)β€˜π‘˜) ∈ β„‚)
182110, 93mgpbas 20087 . . . . . . . . . . . . 13 (Baseβ€˜(Poly1β€˜β„‚fld)) = (Baseβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))
183110ringmgp 20186 . . . . . . . . . . . . . 14 ((Poly1β€˜β„‚fld) ∈ Ring β†’ (mulGrpβ€˜(Poly1β€˜β„‚fld)) ∈ Mnd)
184160, 183mp1i 13 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (mulGrpβ€˜(Poly1β€˜β„‚fld)) ∈ Mnd)
185 simpr 483 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„•0)
186114, 54, 93vr1cl 22143 . . . . . . . . . . . . . 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 19057 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)) ∈ (Baseβ€˜(Poly1β€˜β„‚fld)))
18954ply1sca 22178 . . . . . . . . . . . . . 14 (β„‚fld ∈ Ring β†’ β„‚fld = (Scalarβ€˜(Poly1β€˜β„‚fld)))
1909, 189ax-mp 5 . . . . . . . . . . . . 13 β„‚fld = (Scalarβ€˜(Poly1β€˜β„‚fld))
19193, 190, 153, 4lmodvscl 20768 . . . . . . . . . . . 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 1368 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))) ∈ (Baseβ€˜(Poly1β€˜β„‚fld)))
193192fmpttd 7130 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))):β„•0⟢(Baseβ€˜(Poly1β€˜β„‚fld)))
194165mptex 7241 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))) ∈ V
195 funmpt 6596 . . . . . . . . . . . . 13 Fun (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))
196 fvex 6915 . . . . . . . . . . . . 13 (0gβ€˜(Poly1β€˜β„‚fld)) ∈ V
197194, 195, 1963pm3.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)
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 22139 . . . . . . . . . . . . 13 (π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) β†’ (coe1β€˜π‘Ž) finSupp 0)
200152, 199syl 17 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (coe1β€˜π‘Ž) finSupp 0)
201200fsuppimpd 9401 . . . . . . . . . . 11 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((coe1β€˜π‘Ž) supp 0) ∈ Fin)
202179feqmptd 6972 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (coe1β€˜π‘Ž) = (π‘˜ ∈ β„•0 ↦ ((coe1β€˜π‘Ž)β€˜π‘˜)))
203202oveq1d 7441 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((coe1β€˜π‘Ž) supp 0) = ((π‘˜ ∈ β„•0 ↦ ((coe1β€˜π‘Ž)β€˜π‘˜)) supp 0))
204 eqimss2 4041 . . . . . . . . . . . . 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 20785 . . . . . . . . . . . . 13 (((Poly1β€˜β„‚fld) ∈ LMod ∧ π‘₯ ∈ (Baseβ€˜(Poly1β€˜β„‚fld))) β†’ (0( ·𝑠 β€˜(Poly1β€˜β„‚fld))π‘₯) = (0gβ€˜(Poly1β€˜β„‚fld)))
208206, 207sylan 578 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘₯ ∈ (Baseβ€˜(Poly1β€˜β„‚fld))) β†’ (0( ·𝑠 β€˜(Poly1β€˜β„‚fld))π‘₯) = (0gβ€˜(Poly1β€˜β„‚fld)))
209 c0ex 11246 . . . . . . . . . . . . 13 0 ∈ V
210209a1i 11 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ 0 ∈ V)
211205, 208, 180, 188, 210suppssov1 8209 . . . . . . . . . . 11 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))) supp (0gβ€˜(Poly1β€˜β„‚fld))) βŠ† ((coe1β€˜π‘Ž) supp 0))
212 suppssfifsupp 9411 . . . . . . . . . . 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 19900 . . . . . . . . 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 7147 . . . . . . . . . . 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 7098 . . . . . . . . . . . . . . . 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 17478 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))):β„‚βŸΆβ„‚)
222221feqmptd 6972 . . . . . . . . . . . . 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 483 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) ∧ 𝑧 ∈ β„‚) β†’ 𝑧 ∈ β„‚)
22553, 114, 4, 54, 93, 223, 224evl1vard 22263 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) ∧ 𝑧 ∈ β„‚) β†’ ((var1β€˜β„‚fld) ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) ∧ ((πΈβ€˜(var1β€˜β„‚fld))β€˜π‘§) = 𝑧))
226185adantr 479 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) ∧ 𝑧 ∈ β„‚) β†’ π‘˜ ∈ β„•0)
22753, 54, 4, 93, 223, 224, 225, 116, 127, 226evl1expd 22271 . . . . . . . . . . . . . . . . 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 582 . . . . . . . . . . . . . . . . . . 19 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) ∧ 𝑧 ∈ β„‚) β†’ (π‘˜(.gβ€˜(mulGrpβ€˜β„‚fld))𝑧) = (π‘§β†‘π‘˜))
229228eqeq2d 2739 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) ∧ 𝑧 ∈ β„‚) β†’ (((πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))β€˜π‘§) = (π‘˜(.gβ€˜(mulGrpβ€˜β„‚fld))𝑧) ↔ ((πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))β€˜π‘§) = (π‘§β†‘π‘˜)))
230229anbi2d 628 . . . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) ∧ 𝑧 ∈ β„‚) β†’ ((coe1β€˜π‘Ž)β€˜π‘˜) ∈ β„‚)
23353, 54, 4, 93, 223, 224, 231, 232, 153, 80evl1vsd 22270 . . . . . . . . . . . . . . 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 494 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) ∧ 𝑧 ∈ β„‚) β†’ ((πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))β€˜π‘§) = (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))
235234mpteq2dva 5252 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (𝑧 ∈ β„‚ ↦ ((πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))β€˜π‘§)) = (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
236222, 235eqtrd 2768 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))) = (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
237236mpteq2dva 5252 . . . . . . . . . . 11 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (π‘˜ ∈ β„•0 ↦ (πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))) = (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))))
238216, 237eqtrd 2768 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (𝐸 ∘ (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))) = (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))))
239238oveq2d 7442 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((β„‚fld ↑s β„‚) Ξ£g (𝐸 ∘ (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))))) = ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))))
240157, 214, 2393eqtr2d 2774 . . . . . . . 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 11272 . . . . . . . . . 10 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ β„•0) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)) ∈ β„‚)
246245anasss 465 . . . . . . . . 9 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ (𝑧 ∈ β„‚ ∧ π‘˜ ∈ β„•0)) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)) ∈ β„‚)
247165mptex 7241 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) ∈ V
248 funmpt 6596 . . . . . . . . . . . 12 Fun (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
249247, 248, 393pm3.2i 1336 . . . . . . . . . . 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 13978 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)) ∈ Fin)
252 eldifn 4128 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))) β†’ Β¬ π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))
253252adantl 480 . . . . . . . . . . . . . . . . 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 4127 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))) β†’ π‘˜ ∈ β„•0)
256255adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ π‘˜ ∈ β„•0)
257 eqid 2728 . . . . . . . . . . . . . . . . . . . . . . . 24 ( deg1 β€˜β„‚fld) = ( deg1 β€˜β„‚fld)
258257, 54, 93, 17, 154deg1ge 26054 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) ∧ π‘˜ ∈ β„•0 ∧ ((coe1β€˜π‘Ž)β€˜π‘˜) β‰  0) β†’ π‘˜ ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž))
2592583expia 1118 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) ∧ π‘˜ ∈ β„•0) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) β‰  0 β†’ π‘˜ ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž)))
260254, 256, 259syl2anc 582 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) β‰  0 β†’ π‘˜ ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž)))
261 0xr 11299 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℝ*
262257, 54, 93deg1xrcl 26038 . . . . . . . . . . . . . . . . . . . . . . . . 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 13195 . . . . . . . . . . . . . . . . . . . . . . 23 ((0 ∈ ℝ* ∧ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ ℝ*) β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ≀ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))
266261, 264, 265sylancr 585 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ≀ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))
267256nn0red 12571 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ π‘˜ ∈ ℝ)
268267rexrd 11302 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ π‘˜ ∈ ℝ*)
269 ifcl 4577 . . . . . . . . . . . . . . . . . . . . . . . 24 (((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ ℝ* ∧ 0 ∈ ℝ*) β†’ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0) ∈ ℝ*)
270264, 261, 269sylancl 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0) ∈ ℝ*)
271 xrletr 13177 . . . . . . . . . . . . . . . . . . . . . . 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 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)))
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 524 . . . . . . . . . . . . . . . . . . 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 26039 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ (β„•0 βˆͺ {-∞}))
277152, 276syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ (β„•0 βˆͺ {-∞}))
278 elun 4149 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ (β„•0 βˆͺ {-∞}) ↔ ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ β„•0 ∨ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞}))
279277, 278sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ β„•0 ∨ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞}))
280 nn0ge0 12535 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ β„•0 β†’ 0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž))
281280iftrued 4540 . . . . . . . . . . . . . . . . . . . . . . . 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 2829 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ β„•0 β†’ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0) ∈ β„•0)
284 mnflt0 13145 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -∞ < 0
285 mnfxr 11309 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 -∞ ∈ ℝ*
286 xrltnle 11319 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*) β†’ (-∞ < 0 ↔ Β¬ 0 ≀ -∞))
287285, 261, 286mp2an 690 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (-∞ < 0 ↔ Β¬ 0 ≀ -∞)
288284, 287mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Β¬ 0 ≀ -∞
289 elsni 4649 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞} β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) = -∞)
290289breq2d 5164 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞} β†’ (0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ↔ 0 ≀ -∞))
291288, 290mtbiri 326 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞} β†’ Β¬ 0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž))
292291iffalsed 4543 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞} β†’ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0) = 0)
293 0nn0 12525 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ β„•0
294292, 293eqeltrdi 2837 . . . . . . . . . . . . . . . . . . . . . . 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 13633 . . . . . . . . . . . . . . . . . . . 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 2955 . . . . . . . . . . . . . . . . 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 7441 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)) = (0 Β· (π‘§β†‘π‘˜)))
304255, 244sylan2 591 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (π‘§β†‘π‘˜) ∈ β„‚)
305304mul02d 11450 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (0 Β· (π‘§β†‘π‘˜)) = 0)
306303, 305eqtrd 2768 . . . . . . . . . . . . . 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 5252 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) = (𝑧 ∈ β„‚ ↦ 0))
309 fconstmpt 5744 . . . . . . . . . . . . 13 (β„‚ Γ— {0}) = (𝑧 ∈ β„‚ ↦ 0)
310 ringmnd 20190 . . . . . . . . . . . . . . 15 (β„‚fld ∈ Ring β†’ β„‚fld ∈ Mnd)
3119, 310ax-mp 5 . . . . . . . . . . . . . 14 β„‚fld ∈ Mnd
3123, 17pws0g 18737 . . . . . . . . . . . . . 14 ((β„‚fld ∈ Mnd ∧ β„‚ ∈ V) β†’ (β„‚ Γ— {0}) = (0gβ€˜(β„‚fld ↑s β„‚)))
313311, 6, 312mp2an 690 . . . . . . . . . . . . 13 (β„‚ Γ— {0}) = (0gβ€˜(β„‚fld ↑s β„‚))
314309, 313eqtr3i 2758 . . . . . . . . . . . 12 (𝑧 ∈ β„‚ ↦ 0) = (0gβ€˜(β„‚fld ↑s β„‚))
315308, 314eqtrdi 2784 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) = (0gβ€˜(β„‚fld ↑s β„‚)))
316315, 166suppss2 8212 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) supp (0gβ€˜(β„‚fld ↑s β„‚))) βŠ† (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))
317 suppssfifsupp 9411 . . . . . . . . . 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 19944 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))) = (𝑧 ∈ β„‚ ↦ (β„‚fld Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))))
320 fz0ssnn0 13636 . . . . . . . . . . . 12 (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)) βŠ† β„•0
321 resmpt 6046 . . . . . . . . . . . 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 7437 . . . . . . . . . 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 7130 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))):β„•0βŸΆβ„‚)
327306, 325suppss2 8212 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ ((π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) supp 0) βŠ† (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))
328165mptex 7241 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ V
329 funmpt 6596 . . . . . . . . . . . . . 14 Fun (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))
330328, 329, 2093pm3.2i 1336 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ V ∧ Fun (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∧ 0 ∈ V)
331330a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ ((π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ V ∧ Fun (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∧ 0 ∈ V))
332 fzfid 13978 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)) ∈ Fin)
333 suppssfifsupp 9411 . . . . . . . . . . . 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 19875 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ (β„‚fld Ξ£g ((π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) β†Ύ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) = (β„‚fld Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))))
336 elfznn0 13634 . . . . . . . . . . . 12 (π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)) β†’ π‘˜ ∈ β„•0)
337336, 245sylan2 591 . . . . . . . . . . 11 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)) ∈ β„‚)
338332, 337gsumfsum 21374 . . . . . . . . . 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 2792 . . . . . . . . 9 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ (β„‚fld Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) = Ξ£π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))(((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))
340339mpteq2dva 5252 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (𝑧 ∈ β„‚ ↦ (β„‚fld Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))) = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))(((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
341240, 319, 3403eqtrd 2772 . . . . . . 7 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (πΈβ€˜π‘Ž) = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))(((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
34212adantr 479 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ 𝑆 βŠ† β„‚)
343 elplyr 26155 . . . . . . . 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 1368 . . . . . . 7 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))(((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ (Polyβ€˜π‘†))
345341, 344eqeltrd 2829 . . . . . 6 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (πΈβ€˜π‘Ž) ∈ (Polyβ€˜π‘†))
346 eleq1 2817 . . . . . 6 ((πΈβ€˜π‘Ž) = 𝑓 β†’ ((πΈβ€˜π‘Ž) ∈ (Polyβ€˜π‘†) ↔ 𝑓 ∈ (Polyβ€˜π‘†)))
347345, 346syl5ibcom 244 . . . . 5 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((πΈβ€˜π‘Ž) = 𝑓 β†’ 𝑓 ∈ (Polyβ€˜π‘†)))
348347rexlimdva 3152 . . . 4 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (βˆƒπ‘Ž ∈ 𝐴 (πΈβ€˜π‘Ž) = 𝑓 β†’ 𝑓 ∈ (Polyβ€˜π‘†)))
349151, 348syl5 34 . . 3 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (𝑓 ∈ (𝐸 β€œ 𝐴) β†’ 𝑓 ∈ (Polyβ€˜π‘†)))
350147, 349impbid 211 . 2 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (𝑓 ∈ (Polyβ€˜π‘†) ↔ 𝑓 ∈ (𝐸 β€œ 𝐴)))
351350eqrdv 2726 1 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (Polyβ€˜π‘†) = (𝐸 β€œ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2937  βˆƒwrex 3067  Vcvv 3473   βˆ– cdif 3946   βˆͺ cun 3947   βŠ† wss 3949  ifcif 4532  {csn 4632   class class class wbr 5152   ↦ cmpt 5235   Γ— cxp 5680   β†Ύ cres 5684   β€œ cima 5685   ∘ ccom 5686  Fun wfun 6547   Fn wfn 6548  βŸΆwf 6549  β€˜cfv 6553  (class class class)co 7426   ∘f cof 7689   supp csupp 8171   ↑m cmap 8851  Fincfn 8970   finSupp cfsupp 9393  β„‚cc 11144  0cc0 11146   Β· cmul 11151  -∞cmnf 11284  β„*cxr 11285   < clt 11286   ≀ cle 11287  β„•0cn0 12510  ...cfz 13524  β†‘cexp 14066  Ξ£csu 15672  Basecbs 17187   β†Ύs cress 17216  .rcmulr 17241  Scalarcsca 17243   ·𝑠 cvsca 17244  0gc0g 17428   Ξ£g cgsu 17429   ↑s cpws 17435  Mndcmnd 18701   MndHom cmhm 18745  SubMndcsubmnd 18746  .gcmg 19030  SubGrpcsubg 19082   GrpHom cghm 19174  CMndccmn 19742  mulGrpcmgp 20081  Ringcrg 20180  CRingccrg 20181   RingHom crh 20415  SubRingcsubrg 20513  LModclmod 20750  β„‚fldccnfld 21286  algSccascl 21793  var1cv1 22102  Poly1cpl1 22103  coe1cco1 22104  eval1ce1 22240   deg1 cdg1 26007  Polycply 26138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9672  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224  ax-addf 11225  ax-mulf 11226
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7691  df-ofr 7692  df-om 7877  df-1st 7999  df-2nd 8000  df-supp 8172  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-er 8731  df-map 8853  df-pm 8854  df-ixp 8923  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-fsupp 9394  df-sup 9473  df-oi 9541  df-card 9970  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12251  df-2 12313  df-3 12314  df-4 12315  df-5 12316  df-6 12317  df-7 12318  df-8 12319  df-9 12320  df-n0 12511  df-z 12597  df-dec 12716  df-uz 12861  df-rp 13015  df-fz 13525  df-fzo 13668  df-seq 14007  df-exp 14067  df-hash 14330  df-cj 15086  df-re 15087  df-im 15088  df-sqrt 15222  df-abs 15223  df-clim 15472  df-sum 15673  df-struct 17123  df-sets 17140  df-slot 17158  df-ndx 17170  df-base 17188  df-ress 17217  df-plusg 17253  df-mulr 17254  df-starv 17255  df-sca 17256  df-vsca 17257  df-ip 17258  df-tset 17259  df-ple 17260  df-ds 17262  df-unif 17263  df-hom 17264  df-cco 17265  df-0g 17430  df-gsum 17431  df-prds 17436  df-pws 17438  df-mre 17573  df-mrc 17574  df-acs 17576  df-mgm 18607  df-sgrp 18686  df-mnd 18702  df-mhm 18747  df-submnd 18748  df-grp 18900  df-minusg 18901  df-sbg 18902  df-mulg 19031  df-subg 19085  df-ghm 19175  df-cntz 19275  df-cmn 19744  df-abl 19745  df-mgp 20082  df-rng 20100  df-ur 20129  df-srg 20134  df-ring 20182  df-cring 20183  df-rhm 20418  df-subrng 20490  df-subrg 20515  df-lmod 20752  df-lss 20823  df-lsp 20863  df-cnfld 21287  df-assa 21794  df-asp 21795  df-ascl 21796  df-psr 21849  df-mvr 21850  df-mpl 21851  df-opsr 21853  df-evls 22025  df-evl 22026  df-psr1 22106  df-vr1 22107  df-ply1 22108  df-coe1 22109  df-evl1 22242  df-mdeg 26008  df-deg1 26009  df-ply 26142
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator