MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  plypf1 Structured version   Visualization version   GIF version
Theorem plypf1 26097
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 26080 . . . . 5 (𝑓 ∈ (Polyβ€˜π‘†) ↔ (𝑆 βŠ† β„‚ ∧ βˆƒπ‘› ∈ β„•0 βˆƒπ‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0)𝑓 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))))
21simprbi 496 . . . 4 (𝑓 ∈ (Polyβ€˜π‘†) β†’ βˆƒπ‘› ∈ β„•0 βˆƒπ‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0)𝑓 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
3 eqid 2726 . . . . . . . . 9 (β„‚fld ↑s β„‚) = (β„‚fld ↑s β„‚)
4 cnfldbas 21240 . . . . . . . . 9 β„‚ = (Baseβ€˜β„‚fld)
5 eqid 2726 . . . . . . . . 9 (0gβ€˜(β„‚fld ↑s β„‚)) = (0gβ€˜(β„‚fld ↑s β„‚))
6 cnex 11190 . . . . . . . . . 10 β„‚ ∈ V
76a1i 11 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ β„‚ ∈ V)
8 fzfid 13941 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (0...𝑛) ∈ Fin)
9 cnring 21275 . . . . . . . . . 10 β„‚fld ∈ Ring
10 ringcmn 20179 . . . . . . . . . 10 (β„‚fld ∈ Ring β†’ β„‚fld ∈ CMnd)
119, 10mp1i 13 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ β„‚fld ∈ CMnd)
124subrgss 20472 . . . . . . . . . . . . 13 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 𝑆 βŠ† β„‚)
1312ad2antrr 723 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ 𝑆 βŠ† β„‚)
14 elmapi 8842 . . . . . . . . . . . . . . 15 (π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0) β†’ π‘Ž:β„•0⟢(𝑆 βˆͺ {0}))
1514ad2antll 726 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ π‘Ž:β„•0⟢(𝑆 βˆͺ {0}))
16 subrgsubg 20477 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 𝑆 ∈ (SubGrpβ€˜β„‚fld))
17 cnfld0 21277 . . . . . . . . . . . . . . . . . . . 20 0 = (0gβ€˜β„‚fld)
1817subg0cl 19059 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ (SubGrpβ€˜β„‚fld) β†’ 0 ∈ 𝑆)
1916, 18syl 17 . . . . . . . . . . . . . . . . . 18 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 0 ∈ 𝑆)
2019adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ 0 ∈ 𝑆)
2120snssd 4807 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ {0} βŠ† 𝑆)
22 ssequn2 4178 . . . . . . . . . . . . . . . 16 ({0} βŠ† 𝑆 ↔ (𝑆 βˆͺ {0}) = 𝑆)
2321, 22sylib 217 . . . . . . . . . . . . . . 15 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝑆 βˆͺ {0}) = 𝑆)
2423feq3d 6697 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (π‘Ž:β„•0⟢(𝑆 βˆͺ {0}) ↔ π‘Ž:β„•0βŸΆπ‘†))
2515, 24mpbid 231 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ π‘Ž:β„•0βŸΆπ‘†)
26 elfznn0 13597 . . . . . . . . . . . . 13 (π‘˜ ∈ (0...𝑛) β†’ π‘˜ ∈ β„•0)
27 ffvelcdm 7076 . . . . . . . . . . . . 13 ((π‘Ž:β„•0βŸΆπ‘† ∧ π‘˜ ∈ β„•0) β†’ (π‘Žβ€˜π‘˜) ∈ 𝑆)
2825, 26, 27syl2an 595 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (π‘Žβ€˜π‘˜) ∈ 𝑆)
2913, 28sseldd 3978 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (π‘Žβ€˜π‘˜) ∈ β„‚)
3029adantrl 713 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ (𝑧 ∈ β„‚ ∧ π‘˜ ∈ (0...𝑛))) β†’ (π‘Žβ€˜π‘˜) ∈ β„‚)
31 simprl 768 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ (𝑧 ∈ β„‚ ∧ π‘˜ ∈ (0...𝑛))) β†’ 𝑧 ∈ β„‚)
3226ad2antll 726 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ (𝑧 ∈ β„‚ ∧ π‘˜ ∈ (0...𝑛))) β†’ π‘˜ ∈ β„•0)
33 expcl 14048 . . . . . . . . . . 11 ((𝑧 ∈ β„‚ ∧ π‘˜ ∈ β„•0) β†’ (π‘§β†‘π‘˜) ∈ β„‚)
3431, 32, 33syl2anc 583 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ (𝑧 ∈ β„‚ ∧ π‘˜ ∈ (0...𝑛))) β†’ (π‘§β†‘π‘˜) ∈ β„‚)
3530, 34mulcld 11235 . . . . . . . . 9 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ (𝑧 ∈ β„‚ ∧ π‘˜ ∈ (0...𝑛))) β†’ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)) ∈ β„‚)
36 eqid 2726 . . . . . . . . . 10 (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))) = (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
376mptex 7219 . . . . . . . . . . 11 (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ V
3837a1i 11 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ V)
39 fvex 6897 . . . . . . . . . . 11 (0gβ€˜(β„‚fld ↑s β„‚)) ∈ V
4039a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (0gβ€˜(β„‚fld ↑s β„‚)) ∈ V)
4136, 8, 38, 40fsuppmptdm 9373 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))) finSupp (0gβ€˜(β„‚fld ↑s β„‚)))
423, 4, 5, 7, 8, 11, 35, 41pwsgsum 19900 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))) = (𝑧 ∈ β„‚ ↦ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑛) ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))))
43 fzfid 13941 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ 𝑧 ∈ β„‚) β†’ (0...𝑛) ∈ Fin)
4435anassrs 467 . . . . . . . . . 10 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (0...𝑛)) β†’ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)) ∈ β„‚)
4543, 44gsumfsum 21324 . . . . . . . . 9 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ 𝑧 ∈ β„‚) β†’ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑛) ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))) = Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))
4645mpteq2dva 5241 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝑧 ∈ β„‚ ↦ (β„‚fld Ξ£g (π‘˜ ∈ (0...𝑛) ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))) = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
4742, 46eqtrd 2766 . . . . . . 7 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))) = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
483pwsring 20221 . . . . . . . . . 10 ((β„‚fld ∈ Ring ∧ β„‚ ∈ V) β†’ (β„‚fld ↑s β„‚) ∈ Ring)
499, 6, 48mp2an 689 . . . . . . . . 9 (β„‚fld ↑s β„‚) ∈ Ring
50 ringcmn 20179 . . . . . . . . 9 ((β„‚fld ↑s β„‚) ∈ Ring β†’ (β„‚fld ↑s β„‚) ∈ CMnd)
5149, 50mp1i 13 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (β„‚fld ↑s β„‚) ∈ CMnd)
52 cncrng 21273 . . . . . . . . . . 11 β„‚fld ∈ CRing
53 plypf1.e . . . . . . . . . . . 12 𝐸 = (eval1β€˜β„‚fld)
54 eqid 2726 . . . . . . . . . . . 12 (Poly1β€˜β„‚fld) = (Poly1β€˜β„‚fld)
5553, 54, 3, 4evl1rhm 22202 . . . . . . . . . . 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 22102 . . . . . . . . . . 11 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld)))
6160adantr 480 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ 𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld)))
62 rhmima 20504 . . . . . . . . . 10 ((𝐸 ∈ ((Poly1β€˜β„‚fld) RingHom (β„‚fld ↑s β„‚)) ∧ 𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld))) β†’ (𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)))
6356, 61, 62sylancr 586 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)))
64 subrgsubg 20477 . . . . . . . . 9 ((𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)) β†’ (𝐸 β€œ 𝐴) ∈ (SubGrpβ€˜(β„‚fld ↑s β„‚)))
65 subgsubm 19073 . . . . . . . . 9 ((𝐸 β€œ 𝐴) ∈ (SubGrpβ€˜(β„‚fld ↑s β„‚)) β†’ (𝐸 β€œ 𝐴) ∈ (SubMndβ€˜(β„‚fld ↑s β„‚)))
6663, 64, 653syl 18 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝐸 β€œ 𝐴) ∈ (SubMndβ€˜(β„‚fld ↑s β„‚)))
67 eqid 2726 . . . . . . . . . . . 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 6773 . . . . . . . . . . . . . 14 ((π‘Žβ€˜π‘˜) ∈ β„‚ β†’ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}):β„‚βŸΆβ„‚)
7129, 70syl 17 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}):β„‚βŸΆβ„‚)
723, 4, 67pwselbasb 17441 . . . . . . . . . . . . . 14 ((β„‚fld ∈ Ring ∧ β„‚ ∈ V) β†’ ((β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)) ↔ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}):β„‚βŸΆβ„‚))
739, 6, 72mp2an 689 . . . . . . . . . . . . 13 ((β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)) ↔ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}):β„‚βŸΆβ„‚)
7471, 73sylibr 233 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)))
7534anass1rs 652 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ (π‘§β†‘π‘˜) ∈ β„‚)
7675fmpttd 7109 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)):β„‚βŸΆβ„‚)
773, 4, 67pwselbasb 17441 . . . . . . . . . . . . . 14 ((β„‚fld ∈ Ring ∧ β„‚ ∈ V) β†’ ((𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)) ↔ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)):β„‚βŸΆβ„‚))
789, 6, 77mp2an 689 . . . . . . . . . . . . 13 ((𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)) ↔ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)):β„‚βŸΆβ„‚)
7976, 78sylibr 233 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)))
80 cnfldmul 21244 . . . . . . . . . . . 12 Β· = (.rβ€˜β„‚fld)
81 eqid 2726 . . . . . . . . . . . 12 (.rβ€˜(β„‚fld ↑s β„‚)) = (.rβ€˜(β„‚fld ↑s β„‚))
823, 67, 68, 69, 74, 79, 80, 81pwsmulrval 17444 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ ((β„‚ Γ— {(π‘Žβ€˜π‘˜)})(.rβ€˜(β„‚fld ↑s β„‚))(𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜))) = ((β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∘f Β· (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜))))
8329adantr 480 . . . . . . . . . . . 12 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ (π‘Žβ€˜π‘˜) ∈ β„‚)
84 fconstmpt 5731 . . . . . . . . . . . . 13 (β„‚ Γ— {(π‘Žβ€˜π‘˜)}) = (𝑧 ∈ β„‚ ↦ (π‘Žβ€˜π‘˜))
8584a1i 11 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}) = (𝑧 ∈ β„‚ ↦ (π‘Žβ€˜π‘˜)))
86 eqidd 2727 . . . . . . . . . . . 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 2766 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ ((β„‚ Γ— {(π‘Žβ€˜π‘˜)})(.rβ€˜(β„‚fld ↑s β„‚))(𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜))) = (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))
8963adantr 480 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)))
90 eqid 2726 . . . . . . . . . . . . . 14 (algScβ€˜(Poly1β€˜β„‚fld)) = (algScβ€˜(Poly1β€˜β„‚fld))
9153, 54, 4, 90evl1sca 22204 . . . . . . . . . . . . 13 ((β„‚fld ∈ CRing ∧ (π‘Žβ€˜π‘˜) ∈ β„‚) β†’ (πΈβ€˜((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜))) = (β„‚ Γ— {(π‘Žβ€˜π‘˜)}))
9252, 29, 91sylancr 586 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜))) = (β„‚ Γ— {(π‘Žβ€˜π‘˜)}))
93 eqid 2726 . . . . . . . . . . . . . . . 16 (Baseβ€˜(Poly1β€˜β„‚fld)) = (Baseβ€˜(Poly1β€˜β„‚fld))
9493, 67rhmf 20385 . . . . . . . . . . . . . . 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 6710 . . . . . . . . . . . . . 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 20472 . . . . . . . . . . . . . . 15 (𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld)) β†’ 𝐴 βŠ† (Baseβ€˜(Poly1β€˜β„‚fld)))
9960, 98syl 17 . . . . . . . . . . . . . 14 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 𝐴 βŠ† (Baseβ€˜(Poly1β€˜β„‚fld)))
10099ad2antrr 723 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ 𝐴 βŠ† (Baseβ€˜(Poly1β€˜β„‚fld)))
101 simpll 764 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ 𝑆 ∈ (SubRingβ€˜β„‚fld))
10254, 90, 57, 58, 101, 59, 4, 29subrg1asclcl 22130 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜)) ∈ 𝐴 ↔ (π‘Žβ€˜π‘˜) ∈ 𝑆))
10328, 102mpbird 257 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ ((algScβ€˜(Poly1β€˜β„‚fld))β€˜(π‘Žβ€˜π‘˜)) ∈ 𝐴)
104 fnfvima 7229 . . . . . . . . . . . . 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 2828 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (β„‚ Γ— {(π‘Žβ€˜π‘˜)}) ∈ (𝐸 β€œ 𝐴))
10767subrgss 20472 . . . . . . . . . . . . . . . . 17 ((𝐸 β€œ 𝐴) ∈ (SubRingβ€˜(β„‚fld ↑s β„‚)) β†’ (𝐸 β€œ 𝐴) βŠ† (Baseβ€˜(β„‚fld ↑s β„‚)))
10889, 107syl 17 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝐸 β€œ 𝐴) βŠ† (Baseβ€˜(β„‚fld ↑s β„‚)))
10960ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ 𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld)))
110 eqid 2726 . . . . . . . . . . . . . . . . . . . 20 (mulGrpβ€˜(Poly1β€˜β„‚fld)) = (mulGrpβ€˜(Poly1β€˜β„‚fld))
111110subrgsubm 20485 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ (SubRingβ€˜(Poly1β€˜β„‚fld)) β†’ 𝐴 ∈ (SubMndβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld))))
112109, 111syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ 𝐴 ∈ (SubMndβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld))))
11326adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ π‘˜ ∈ β„•0)
114 eqid 2726 . . . . . . . . . . . . . . . . . . 19 (var1β€˜β„‚fld) = (var1β€˜β„‚fld)
115114, 101, 57, 58, 59subrgvr1cl 22132 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (var1β€˜β„‚fld) ∈ 𝐴)
116 eqid 2726 . . . . . . . . . . . . . . . . . . 19 (.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld))) = (.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))
117116submmulgcl 19042 . . . . . . . . . . . . . . . . . 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 7229 . . . . . . . . . . . . . . . . 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 3978 . . . . . . . . . . . . . . 15 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))) ∈ (Baseβ€˜(β„‚fld ↑s β„‚)))
1223, 4, 67, 68, 69, 121pwselbas 17442 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))):β„‚βŸΆβ„‚)
123122feqmptd 6953 . . . . . . . . . . . . 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 484 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ 𝑧 ∈ β„‚)
12653, 114, 4, 54, 93, 124, 125evl1vard 22207 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ ((var1β€˜β„‚fld) ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) ∧ ((πΈβ€˜(var1β€˜β„‚fld))β€˜π‘§) = 𝑧))
127 eqid 2726 . . . . . . . . . . . . . . . . 17 (.gβ€˜(mulGrpβ€˜β„‚fld)) = (.gβ€˜(mulGrpβ€˜β„‚fld))
128113adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ π‘˜ ∈ β„•0)
12953, 54, 4, 93, 124, 125, 126, 116, 127, 128evl1expd 22215 . . . . . . . . . . . . . . . 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 495 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ ((πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))β€˜π‘§) = (π‘˜(.gβ€˜(mulGrpβ€˜β„‚fld))𝑧))
131 cnfldexp 21289 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ β„‚ ∧ π‘˜ ∈ β„•0) β†’ (π‘˜(.gβ€˜(mulGrpβ€˜β„‚fld))𝑧) = (π‘§β†‘π‘˜))
132125, 128, 131syl2anc 583 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ (π‘˜(.gβ€˜(mulGrpβ€˜β„‚fld))𝑧) = (π‘§β†‘π‘˜))
133130, 132eqtrd 2766 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) ∧ 𝑧 ∈ β„‚) β†’ ((πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))β€˜π‘§) = (π‘§β†‘π‘˜))
134133mpteq2dva 5241 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ ((πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))β€˜π‘§)) = (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)))
135123, 134eqtrd 2766 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (πΈβ€˜(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))) = (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)))
136135, 120eqeltrrd 2828 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ (π‘§β†‘π‘˜)) ∈ (𝐸 β€œ 𝐴))
13781subrgmcl 20484 . . . . . . . . . . 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 2828 . . . . . . . . 9 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) ∧ π‘˜ ∈ (0...𝑛)) β†’ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ (𝐸 β€œ 𝐴))
140139fmpttd 7109 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))):(0...𝑛)⟢(𝐸 β€œ 𝐴))
14136, 8, 139, 40fsuppmptdm 9373 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜)))) finSupp (0gβ€˜(β„‚fld ↑s β„‚)))
1425, 51, 8, 66, 140, 141gsumsubmcl 19837 . . . . . . 7 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ (0...𝑛) ↦ (𝑧 ∈ β„‚ ↦ ((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))))) ∈ (𝐸 β€œ 𝐴))
14347, 142eqeltrrd 2828 . . . . . 6 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ (𝐸 β€œ 𝐴))
144 eleq1 2815 . . . . . 6 (𝑓 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) β†’ (𝑓 ∈ (𝐸 β€œ 𝐴) ↔ (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ (𝐸 β€œ 𝐴)))
145143, 144syl5ibrcom 246 . . . . 5 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ (𝑛 ∈ β„•0 ∧ π‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))) β†’ (𝑓 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) β†’ 𝑓 ∈ (𝐸 β€œ 𝐴)))
146145rexlimdvva 3205 . . . 4 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (βˆƒπ‘› ∈ β„•0 βˆƒπ‘Ž ∈ ((𝑆 βˆͺ {0}) ↑m β„•0)𝑓 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑛)((π‘Žβ€˜π‘˜) Β· (π‘§β†‘π‘˜))) β†’ 𝑓 ∈ (𝐸 β€œ 𝐴)))
1472, 146syl5 34 . . 3 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (𝑓 ∈ (Polyβ€˜π‘†) β†’ 𝑓 ∈ (𝐸 β€œ 𝐴)))
148 ffun 6713 . . . . . 6 (𝐸:(Baseβ€˜(Poly1β€˜β„‚fld))⟢(Baseβ€˜(β„‚fld ↑s β„‚)) β†’ Fun 𝐸)
14995, 148ax-mp 5 . . . . 5 Fun 𝐸
150 fvelima 6950 . . . . 5 ((Fun 𝐸 ∧ 𝑓 ∈ (𝐸 β€œ 𝐴)) β†’ βˆƒπ‘Ž ∈ 𝐴 (πΈβ€˜π‘Ž) = 𝑓)
151149, 150mpan 687 . . . 4 (𝑓 ∈ (𝐸 β€œ 𝐴) β†’ βˆƒπ‘Ž ∈ 𝐴 (πΈβ€˜π‘Ž) = 𝑓)
15299sselda 3977 . . . . . . . . . . 11 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld)))
153 eqid 2726 . . . . . . . . . . . 12 ( ·𝑠 β€˜(Poly1β€˜β„‚fld)) = ( ·𝑠 β€˜(Poly1β€˜β„‚fld))
154 eqid 2726 . . . . . . . . . . . 12 (coe1β€˜π‘Ž) = (coe1β€˜π‘Ž)
15554, 114, 93, 153, 110, 116, 154ply1coe 22168 . . . . . . . . . . 11 ((β„‚fld ∈ Ring ∧ π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld))) β†’ π‘Ž = ((Poly1β€˜β„‚fld) Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))))
1569, 152, 155sylancr 586 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ π‘Ž = ((Poly1β€˜β„‚fld) Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))))
157156fveq2d 6888 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (πΈβ€˜π‘Ž) = (πΈβ€˜((Poly1β€˜β„‚fld) Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))))))
158 eqid 2726 . . . . . . . . . 10 (0gβ€˜(Poly1β€˜β„‚fld)) = (0gβ€˜(Poly1β€˜β„‚fld))
15954ply1ring 22117 . . . . . . . . . . . 12 (β„‚fld ∈ Ring β†’ (Poly1β€˜β„‚fld) ∈ Ring)
1609, 159ax-mp 5 . . . . . . . . . . 11 (Poly1β€˜β„‚fld) ∈ Ring
161 ringcmn 20179 . . . . . . . . . . 11 ((Poly1β€˜β„‚fld) ∈ Ring β†’ (Poly1β€˜β„‚fld) ∈ CMnd)
162160, 161mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (Poly1β€˜β„‚fld) ∈ CMnd)
163 ringmnd 20146 . . . . . . . . . . 11 ((β„‚fld ↑s β„‚) ∈ Ring β†’ (β„‚fld ↑s β„‚) ∈ Mnd)
16449, 163mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (β„‚fld ↑s β„‚) ∈ Mnd)
165 nn0ex 12479 . . . . . . . . . . 11 β„•0 ∈ V
166165a1i 11 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ β„•0 ∈ V)
167 rhmghm 20384 . . . . . . . . . . . 12 (𝐸 ∈ ((Poly1β€˜β„‚fld) RingHom (β„‚fld ↑s β„‚)) β†’ 𝐸 ∈ ((Poly1β€˜β„‚fld) GrpHom (β„‚fld ↑s β„‚)))
16856, 167ax-mp 5 . . . . . . . . . . 11 𝐸 ∈ ((Poly1β€˜β„‚fld) GrpHom (β„‚fld ↑s β„‚))
169 ghmmhm 19149 . . . . . . . . . . 11 (𝐸 ∈ ((Poly1β€˜β„‚fld) GrpHom (β„‚fld ↑s β„‚)) β†’ 𝐸 ∈ ((Poly1β€˜β„‚fld) MndHom (β„‚fld ↑s β„‚)))
170168, 169mp1i 13 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ 𝐸 ∈ ((Poly1β€˜β„‚fld) MndHom (β„‚fld ↑s β„‚)))
17154ply1lmod 22121 . . . . . . . . . . . . 13 (β„‚fld ∈ Ring β†’ (Poly1β€˜β„‚fld) ∈ LMod)
1729, 171mp1i 13 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (Poly1β€˜β„‚fld) ∈ LMod)
17312ad2antrr 723 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ 𝑆 βŠ† β„‚)
174 eqid 2726 . . . . . . . . . . . . . . . . 17 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
175154, 59, 58, 174coe1f 22081 . . . . . . . . . . . . . . . 16 (π‘Ž ∈ 𝐴 β†’ (coe1β€˜π‘Ž):β„•0⟢(Baseβ€˜π‘…))
17657subrgbas 20481 . . . . . . . . . . . . . . . . 17 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ 𝑆 = (Baseβ€˜π‘…))
177176feq3d 6697 . . . . . . . . . . . . . . . 16 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ ((coe1β€˜π‘Ž):β„•0βŸΆπ‘† ↔ (coe1β€˜π‘Ž):β„•0⟢(Baseβ€˜π‘…)))
178175, 177imbitrrid 245 . . . . . . . . . . . . . . 15 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (π‘Ž ∈ 𝐴 β†’ (coe1β€˜π‘Ž):β„•0βŸΆπ‘†))
179178imp 406 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (coe1β€˜π‘Ž):β„•0βŸΆπ‘†)
180179ffvelcdmda 7079 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ ((coe1β€˜π‘Ž)β€˜π‘˜) ∈ 𝑆)
181173, 180sseldd 3978 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ ((coe1β€˜π‘Ž)β€˜π‘˜) ∈ β„‚)
182110, 93mgpbas 20043 . . . . . . . . . . . . 13 (Baseβ€˜(Poly1β€˜β„‚fld)) = (Baseβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))
183110ringmgp 20142 . . . . . . . . . . . . . 14 ((Poly1β€˜β„‚fld) ∈ Ring β†’ (mulGrpβ€˜(Poly1β€˜β„‚fld)) ∈ Mnd)
184160, 183mp1i 13 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (mulGrpβ€˜(Poly1β€˜β„‚fld)) ∈ Mnd)
185 simpr 484 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„•0)
186114, 54, 93vr1cl 22087 . . . . . . . . . . . . . 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 19020 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)) ∈ (Baseβ€˜(Poly1β€˜β„‚fld)))
18954ply1sca 22122 . . . . . . . . . . . . . 14 (β„‚fld ∈ Ring β†’ β„‚fld = (Scalarβ€˜(Poly1β€˜β„‚fld)))
1909, 189ax-mp 5 . . . . . . . . . . . . 13 β„‚fld = (Scalarβ€˜(Poly1β€˜β„‚fld))
19193, 190, 153, 4lmodvscl 20722 . . . . . . . . . . . 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 7109 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))):β„•0⟢(Baseβ€˜(Poly1β€˜β„‚fld)))
194165mptex 7219 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))) ∈ V
195 funmpt 6579 . . . . . . . . . . . . 13 Fun (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))
196 fvex 6897 . . . . . . . . . . . . 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 22083 . . . . . . . . . . . . 13 (π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) β†’ (coe1β€˜π‘Ž) finSupp 0)
200152, 199syl 17 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (coe1β€˜π‘Ž) finSupp 0)
201200fsuppimpd 9368 . . . . . . . . . . 11 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((coe1β€˜π‘Ž) supp 0) ∈ Fin)
202179feqmptd 6953 . . . . . . . . . . . . . 14 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (coe1β€˜π‘Ž) = (π‘˜ ∈ β„•0 ↦ ((coe1β€˜π‘Ž)β€˜π‘˜)))
203202oveq1d 7419 . . . . . . . . . . . . 13 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((coe1β€˜π‘Ž) supp 0) = ((π‘˜ ∈ β„•0 ↦ ((coe1β€˜π‘Ž)β€˜π‘˜)) supp 0))
204 eqimss2 4036 . . . . . . . . . . . . 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 20739 . . . . . . . . . . . . 13 (((Poly1β€˜β„‚fld) ∈ LMod ∧ π‘₯ ∈ (Baseβ€˜(Poly1β€˜β„‚fld))) β†’ (0( ·𝑠 β€˜(Poly1β€˜β„‚fld))π‘₯) = (0gβ€˜(Poly1β€˜β„‚fld)))
208206, 207sylan 579 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘₯ ∈ (Baseβ€˜(Poly1β€˜β„‚fld))) β†’ (0( ·𝑠 β€˜(Poly1β€˜β„‚fld))π‘₯) = (0gβ€˜(Poly1β€˜β„‚fld)))
209 c0ex 11209 . . . . . . . . . . . . 13 0 ∈ V
210209a1i 11 . . . . . . . . . . . 12 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ 0 ∈ V)
211205, 208, 180, 188, 210suppssov1 8180 . . . . . . . . . . 11 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))) supp (0gβ€˜(Poly1β€˜β„‚fld))) βŠ† ((coe1β€˜π‘Ž) supp 0))
212 suppssfifsupp 9377 . . . . . . . . . . 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 834 . . . . . . . . . 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 19856 . . . . . . . . 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 7125 . . . . . . . . . . 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 7078 . . . . . . . . . . . . . . . 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 17442 . . . . . . . . . . . . . 14 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))):β„‚βŸΆβ„‚)
222221feqmptd 6953 . . . . . . . . . . . . 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 484 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) ∧ 𝑧 ∈ β„‚) β†’ 𝑧 ∈ β„‚)
22553, 114, 4, 54, 93, 223, 224evl1vard 22207 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) ∧ 𝑧 ∈ β„‚) β†’ ((var1β€˜β„‚fld) ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) ∧ ((πΈβ€˜(var1β€˜β„‚fld))β€˜π‘§) = 𝑧))
226185adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) ∧ 𝑧 ∈ β„‚) β†’ π‘˜ ∈ β„•0)
22753, 54, 4, 93, 223, 224, 225, 116, 127, 226evl1expd 22215 . . . . . . . . . . . . . . . . 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 583 . . . . . . . . . . . . . . . . . . 19 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) ∧ 𝑧 ∈ β„‚) β†’ (π‘˜(.gβ€˜(mulGrpβ€˜β„‚fld))𝑧) = (π‘§β†‘π‘˜))
229228eqeq2d 2737 . . . . . . . . . . . . . . . . . 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 480 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) ∧ 𝑧 ∈ β„‚) β†’ ((coe1β€˜π‘Ž)β€˜π‘˜) ∈ β„‚)
23353, 54, 4, 93, 223, 224, 231, 232, 153, 80evl1vsd 22214 . . . . . . . . . . . . . . 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 495 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) ∧ 𝑧 ∈ β„‚) β†’ ((πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))β€˜π‘§) = (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))
235234mpteq2dva 5241 . . . . . . . . . . . . 13 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (𝑧 ∈ β„‚ ↦ ((πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))β€˜π‘§)) = (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
236222, 235eqtrd 2766 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ β„•0) β†’ (πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))) = (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
237236mpteq2dva 5241 . . . . . . . . . . 11 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (π‘˜ ∈ β„•0 ↦ (πΈβ€˜(((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))) = (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))))
238216, 237eqtrd 2766 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (𝐸 ∘ (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld))))) = (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))))
239238oveq2d 7420 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((β„‚fld ↑s β„‚) Ξ£g (𝐸 ∘ (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜)( ·𝑠 β€˜(Poly1β€˜β„‚fld))(π‘˜(.gβ€˜(mulGrpβ€˜(Poly1β€˜β„‚fld)))(var1β€˜β„‚fld)))))) = ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))))
240157, 214, 2393eqtr2d 2772 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (πΈβ€˜π‘Ž) = ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))))
2416a1i 11 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ β„‚ ∈ V)
2429, 10mp1i 13 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ β„‚fld ∈ CMnd)
243181adantlr 712 . . . . . . . . . . 11 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ β„•0) β†’ ((coe1β€˜π‘Ž)β€˜π‘˜) ∈ β„‚)
24433adantll 711 . . . . . . . . . . 11 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ β„•0) β†’ (π‘§β†‘π‘˜) ∈ β„‚)
245243, 244mulcld 11235 . . . . . . . . . 10 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ β„•0) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)) ∈ β„‚)
246245anasss 466 . . . . . . . . 9 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ (𝑧 ∈ β„‚ ∧ π‘˜ ∈ β„•0)) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)) ∈ β„‚)
247165mptex 7219 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) ∈ V
248 funmpt 6579 . . . . . . . . . . . 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 13941 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)) ∈ Fin)
252 eldifn 4122 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))) β†’ Β¬ π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))
253252adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ Β¬ π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))
254152ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld)))
255 eldifi 4121 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))) β†’ π‘˜ ∈ β„•0)
256255adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ π‘˜ ∈ β„•0)
257 eqid 2726 . . . . . . . . . . . . . . . . . . . . . . . 24 ( deg1 β€˜β„‚fld) = ( deg1 β€˜β„‚fld)
258257, 54, 93, 17, 154deg1ge 25985 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) ∧ π‘˜ ∈ β„•0 ∧ ((coe1β€˜π‘Ž)β€˜π‘˜) β‰  0) β†’ π‘˜ ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž))
2592583expia 1118 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) ∧ π‘˜ ∈ β„•0) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) β‰  0 β†’ π‘˜ ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž)))
260254, 256, 259syl2anc 583 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) β‰  0 β†’ π‘˜ ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž)))
261 0xr 11262 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℝ*
262257, 54, 93deg1xrcl 25969 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ ℝ*)
263152, 262syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ ℝ*)
264263ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ ℝ*)
265 xrmax2 13158 . . . . . . . . . . . . . . . . . . . . . . 23 ((0 ∈ ℝ* ∧ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ ℝ*) β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ≀ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))
266261, 264, 265sylancr 586 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ≀ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))
267256nn0red 12534 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ π‘˜ ∈ ℝ)
268267rexrd 11265 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ π‘˜ ∈ ℝ*)
269 ifcl 4568 . . . . . . . . . . . . . . . . . . . . . . . 24 (((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ ℝ* ∧ 0 ∈ ℝ*) β†’ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0) ∈ ℝ*)
270264, 261, 269sylancl 585 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0) ∈ ℝ*)
271 xrletr 13140 . . . . . . . . . . . . . . . . . . . . . . 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 691 . . . . . . . . . . . . . . . . . . . . 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 525 . . . . . . . . . . . . . . . . . . 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 25970 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž ∈ (Baseβ€˜(Poly1β€˜β„‚fld)) β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ (β„•0 βˆͺ {-∞}))
277152, 276syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ (β„•0 βˆͺ {-∞}))
278 elun 4143 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ (β„•0 βˆͺ {-∞}) ↔ ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ β„•0 ∨ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞}))
279277, 278sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ β„•0 ∨ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞}))
280 nn0ge0 12498 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ β„•0 β†’ 0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž))
281280iftrued 4531 . . . . . . . . . . . . . . . . . . . . . . . 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 2827 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ β„•0 β†’ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0) ∈ β„•0)
284 mnflt0 13108 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -∞ < 0
285 mnfxr 11272 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 -∞ ∈ ℝ*
286 xrltnle 11282 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*) β†’ (-∞ < 0 ↔ Β¬ 0 ≀ -∞))
287285, 261, 286mp2an 689 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (-∞ < 0 ↔ Β¬ 0 ≀ -∞)
288284, 287mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Β¬ 0 ≀ -∞
289 elsni 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞} β†’ (( deg1 β€˜β„‚fld)β€˜π‘Ž) = -∞)
290289breq2d 5153 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞} β†’ (0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž) ↔ 0 ≀ -∞))
291288, 290mtbiri 327 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞} β†’ Β¬ 0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž))
292291iffalsed 4534 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞} β†’ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0) = 0)
293 0nn0 12488 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ β„•0
294292, 293eqeltrdi 2835 . . . . . . . . . . . . . . . . . . . . . . 23 ((( deg1 β€˜β„‚fld)β€˜π‘Ž) ∈ {-∞} β†’ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0) ∈ β„•0)
295283, 294jaoi 854 . . . . . . . . . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . . . . . 20 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0) ∈ β„•0)
298 fznn0 13596 . . . . . . . . . . . . . . . . . . . 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 259 . . . . . . . . . . . . . . . . . 18 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) β‰  0 β†’ π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))))
301300necon1bd 2952 . . . . . . . . . . . . . . . . 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 7419 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)) = (0 Β· (π‘§β†‘π‘˜)))
304255, 244sylan2 592 . . . . . . . . . . . . . . . 16 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (π‘§β†‘π‘˜) ∈ β„‚)
305304mul02d 11413 . . . . . . . . . . . . . . 15 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (0 Β· (π‘§β†‘π‘˜)) = 0)
306303, 305eqtrd 2766 . . . . . . . . . . . . . 14 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)) = 0)
307306an32s 649 . . . . . . . . . . . . 13 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) ∧ 𝑧 ∈ β„‚) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)) = 0)
308307mpteq2dva 5241 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) = (𝑧 ∈ β„‚ ↦ 0))
309 fconstmpt 5731 . . . . . . . . . . . . 13 (β„‚ Γ— {0}) = (𝑧 ∈ β„‚ ↦ 0)
310 ringmnd 20146 . . . . . . . . . . . . . . 15 (β„‚fld ∈ Ring β†’ β„‚fld ∈ Mnd)
3119, 310ax-mp 5 . . . . . . . . . . . . . 14 β„‚fld ∈ Mnd
3123, 17pws0g 18701 . . . . . . . . . . . . . 14 ((β„‚fld ∈ Mnd ∧ β„‚ ∈ V) β†’ (β„‚ Γ— {0}) = (0gβ€˜(β„‚fld ↑s β„‚)))
313311, 6, 312mp2an 689 . . . . . . . . . . . . 13 (β„‚ Γ— {0}) = (0gβ€˜(β„‚fld ↑s β„‚))
314309, 313eqtr3i 2756 . . . . . . . . . . . 12 (𝑧 ∈ β„‚ ↦ 0) = (0gβ€˜(β„‚fld ↑s β„‚))
315308, 314eqtrdi 2782 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ π‘˜ ∈ (β„•0 βˆ– (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) β†’ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) = (0gβ€˜(β„‚fld ↑s β„‚)))
316315, 166suppss2 8183 . . . . . . . . . 10 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) supp (0gβ€˜(β„‚fld ↑s β„‚))) βŠ† (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))
317 suppssfifsupp 9377 . . . . . . . . . 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 834 . . . . . . . . 9 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) finSupp (0gβ€˜(β„‚fld ↑s β„‚)))
3193, 4, 5, 241, 166, 242, 246, 318pwsgsum 19900 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((β„‚fld ↑s β„‚) Ξ£g (π‘˜ ∈ β„•0 ↦ (𝑧 ∈ β„‚ ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))) = (𝑧 ∈ β„‚ ↦ (β„‚fld Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))))
320 fz0ssnn0 13599 . . . . . . . . . . . 12 (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)) βŠ† β„•0
321 resmpt 6030 . . . . . . . . . . . 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 7415 . . . . . . . . . 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 7109 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))):β„•0βŸΆβ„‚)
327306, 325suppss2 8183 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ ((π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) supp 0) βŠ† (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))
328165mptex 7219 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) ∈ V
329 funmpt 6579 . . . . . . . . . . . . . 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 13941 . . . . . . . . . . . 12 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)) ∈ Fin)
333 suppssfifsupp 9377 . . . . . . . . . . . 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 834 . . . . . . . . . . 11 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) finSupp 0)
3354, 17, 324, 325, 326, 327, 334gsumres 19831 . . . . . . . . . 10 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ (β„‚fld Ξ£g ((π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))) β†Ύ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)))) = (β„‚fld Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))))
336 elfznn0 13597 . . . . . . . . . . . 12 (π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0)) β†’ π‘˜ ∈ β„•0)
337336, 245sylan2 592 . . . . . . . . . . 11 ((((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) ∧ π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))) β†’ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)) ∈ β„‚)
338332, 337gsumfsum 21324 . . . . . . . . . 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 2790 . . . . . . . . 9 (((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) ∧ 𝑧 ∈ β„‚) β†’ (β„‚fld Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))) = Ξ£π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))(((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜)))
340339mpteq2dva 5241 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (𝑧 ∈ β„‚ ↦ (β„‚fld Ξ£g (π‘˜ ∈ β„•0 ↦ (((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))) = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))(((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
341240, 319, 3403eqtrd 2770 . . . . . . 7 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (πΈβ€˜π‘Ž) = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...if(0 ≀ (( deg1 β€˜β„‚fld)β€˜π‘Ž), (( deg1 β€˜β„‚fld)β€˜π‘Ž), 0))(((coe1β€˜π‘Ž)β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
34212adantr 480 . . . . . . . 8 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ 𝑆 βŠ† β„‚)
343 elplyr 26086 . . . . . . . 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 2827 . . . . . 6 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ (πΈβ€˜π‘Ž) ∈ (Polyβ€˜π‘†))
346 eleq1 2815 . . . . . 6 ((πΈβ€˜π‘Ž) = 𝑓 β†’ ((πΈβ€˜π‘Ž) ∈ (Polyβ€˜π‘†) ↔ 𝑓 ∈ (Polyβ€˜π‘†)))
347345, 346syl5ibcom 244 . . . . 5 ((𝑆 ∈ (SubRingβ€˜β„‚fld) ∧ π‘Ž ∈ 𝐴) β†’ ((πΈβ€˜π‘Ž) = 𝑓 β†’ 𝑓 ∈ (Polyβ€˜π‘†)))
348347rexlimdva 3149 . . . 4 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (βˆƒπ‘Ž ∈ 𝐴 (πΈβ€˜π‘Ž) = 𝑓 β†’ 𝑓 ∈ (Polyβ€˜π‘†)))
349151, 348syl5 34 . . 3 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (𝑓 ∈ (𝐸 β€œ 𝐴) β†’ 𝑓 ∈ (Polyβ€˜π‘†)))
350147, 349impbid 211 . 2 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (𝑓 ∈ (Polyβ€˜π‘†) ↔ 𝑓 ∈ (𝐸 β€œ 𝐴)))
351350eqrdv 2724 1 (𝑆 ∈ (SubRingβ€˜β„‚fld) β†’ (Polyβ€˜π‘†) = (𝐸 β€œ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2934  βˆƒwrex 3064  Vcvv 3468   βˆ– cdif 3940   βˆͺ cun 3941   βŠ† wss 3943  ifcif 4523  {csn 4623   class class class wbr 5141   ↦ cmpt 5224   Γ— cxp 5667   β†Ύ cres 5671   β€œ cima 5672   ∘ ccom 5673  Fun wfun 6530   Fn wfn 6531  βŸΆwf 6532  β€˜cfv 6536  (class class class)co 7404   ∘f cof 7664   supp csupp 8143   ↑m cmap 8819  Fincfn 8938   finSupp cfsupp 9360  β„‚cc 11107  0cc0 11109   Β· cmul 11114  -∞cmnf 11247  β„*cxr 11248   < clt 11249   ≀ cle 11250  β„•0cn0 12473  ...cfz 13487  β†‘cexp 14030  Ξ£csu 15636  Basecbs 17151   β†Ύs cress 17180  .rcmulr 17205  Scalarcsca 17207   ·𝑠 cvsca 17208  0gc0g 17392   Ξ£g cgsu 17393   ↑s cpws 17399  Mndcmnd 18665   MndHom cmhm 18709  SubMndcsubmnd 18710  .gcmg 18993  SubGrpcsubg 19045   GrpHom cghm 19136  CMndccmn 19698  mulGrpcmgp 20037  Ringcrg 20136  CRingccrg 20137   RingHom crh 20369  SubRingcsubrg 20467  LModclmod 20704  β„‚fldccnfld 21236  algSccascl 21743  var1cv1 22046  Poly1cpl1 22047  coe1cco1 22048  eval1ce1 22184   deg1 cdg1 25938  Polycply 26069
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 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  ax-inf2 9635  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-pre-sup 11187  ax-addf 11188  ax-mulf 11189
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6293  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-of 7666  df-ofr 7667  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8144  df-frecs 8264  df-wrecs 8295  df-recs 8369  df-rdg 8408  df-1o 8464  df-er 8702  df-map 8821  df-pm 8822  df-ixp 8891  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-fsupp 9361  df-sup 9436  df-oi 9504  df-card 9933  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11447  df-neg 11448  df-div 11873  df-nn 12214  df-2 12276  df-3 12277  df-4 12278  df-5 12279  df-6 12280  df-7 12281  df-8 12282  df-9 12283  df-n0 12474  df-z 12560  df-dec 12679  df-uz 12824  df-rp 12978  df-fz 13488  df-fzo 13631  df-seq 13970  df-exp 14031  df-hash 14294  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-clim 15436  df-sum 15637  df-struct 17087  df-sets 17104  df-slot 17122  df-ndx 17134  df-base 17152  df-ress 17181  df-plusg 17217  df-mulr 17218  df-starv 17219  df-sca 17220  df-vsca 17221  df-ip 17222  df-tset 17223  df-ple 17224  df-ds 17226  df-unif 17227  df-hom 17228  df-cco 17229  df-0g 17394  df-gsum 17395  df-prds 17400  df-pws 17402  df-mre 17537  df-mrc 17538  df-acs 17540  df-mgm 18571  df-sgrp 18650  df-mnd 18666  df-mhm 18711  df-submnd 18712  df-grp 18864  df-minusg 18865  df-sbg 18866  df-mulg 18994  df-subg 19048  df-ghm 19137  df-cntz 19231  df-cmn 19700  df-abl 19701  df-mgp 20038  df-rng 20056  df-ur 20085  df-srg 20090  df-ring 20138  df-cring 20139  df-rhm 20372  df-subrng 20444  df-subrg 20469  df-lmod 20706  df-lss 20777  df-lsp 20817  df-cnfld 21237  df-assa 21744  df-asp 21745  df-ascl 21746  df-psr 21799  df-mvr 21800  df-mpl 21801  df-opsr 21803  df-evls 21973  df-evl 21974  df-psr1 22050  df-vr1 22051  df-ply1 22052  df-coe1 22053  df-evl1 22186  df-mdeg 25939  df-deg1 25940  df-ply 26073
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator