Theorem ply1sca 22137

Description: Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015.)

Hypothesis

Ref	Expression
ply1lmod.p	⊢ 𝑃 = (Poly1‘𝑅)

Assertion

Ref	Expression
ply1sca	⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘𝑃))

Proof of Theorem ply1sca

Step	Hyp	Ref	Expression
1		eqid 2729	. . 3 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅)
2	1	psr1sca 22134	. 2 ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘(PwSer1‘𝑅)))
3		fvex 6871	. . 3 ⊢ (Base‘(1o mPoly 𝑅)) ∈ V
4		ply1lmod.p	. . . . 5 ⊢ 𝑃 = (Poly1‘𝑅)
5	4, 1	ply1val 22078	. . . 4 ⊢ 𝑃 = ((PwSer1‘𝑅) ↾s (Base‘(1o mPoly 𝑅)))
6		eqid 2729	. . . 4 ⊢ (Scalar‘(PwSer1‘𝑅)) = (Scalar‘(PwSer1‘𝑅))
7	5, 6	resssca 17306	. . 3 ⊢ ((Base‘(1o mPoly 𝑅)) ∈ V → (Scalar‘(PwSer1‘𝑅)) = (Scalar‘𝑃))
8	3, 7	ax-mp 5	. 2 ⊢ (Scalar‘(PwSer1‘𝑅)) = (Scalar‘𝑃)
9	2, 8	eqtrdi 2780	1 ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘𝑃))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3447  ‘cfv 6511  (class class class)co 7387  1_oc1o 8427  Basecbs 17179  Scalarcsca 17223   mPoly cmpl 21815  PwSer₁cps1 22059  Poly₁cpl1 22061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-of 7653  df-om 7843  df-1st 7968  df-2nd 7969  df-supp 8140  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-er 8671  df-map 8801  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-fsupp 9313  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-nn 12187  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253  df-7 12254  df-8 12255  df-9 12256  df-n0 12443  df-z 12530  df-dec 12650  df-uz 12794  df-fz 13469  df-struct 17117  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201  df-plusg 17233  df-mulr 17234  df-sca 17236  df-vsca 17237  df-tset 17239  df-ple 17240  df-psr 21818  df-opsr 21822  df-psr1 22064  df-ply1 22066

This theorem is referenced by:  ply1sca2  22138  ply1ascl0  22139  ply1ascl1  22140  ply10s0  22142  ply1ascl  22144  coe1pwmul  22165  ply1scl0  22176  ply1scl1  22179  ply1idvr1OLD  22182  ply1coefsupp  22184  ply1coe  22185  cply1coe0bi  22189  ply1chr  22193  gsumsmonply1  22194  gsummoncoe1  22195  lply1binomsc  22198  ply1fermltlchr  22199  evls1sca  22210  evl1vsd  22231  evl1scvarpw  22250  evl1gsummon  22252  evls1fpws  22256  evls1vsca  22260  asclply1subcl  22261  evls1maplmhm  22264  cpmatacl  22603  cpmatinvcl  22604  mat2pmatbas  22613  mat2pmatghm  22617  mat2pmatmul  22618  mat2pmatlin  22622  decpmatid  22657  pmatcollpw2lem  22664  monmatcollpw  22666  pmatcollpwlem  22667  pmatcollpwscmatlem1  22676  pm2mpcl  22684  idpm2idmp  22688  mply1topmatcllem  22690  mply1topmatcl  22692  mp2pm2mplem4  22696  mp2pm2mplem5  22697  pm2mpghmlem2  22699  pm2mpghm  22703  pm2mpmhmlem1  22705  pm2mpmhmlem2  22706  monmat2matmon  22711  chpscmat  22729  chpscmatgsumbin  22731  chpscmatgsummon  22732  deg1pwle  26025  deg1pw  26026  ply1remlem  26070  fta1blem  26076  plypf1  26117  ply1lvec  33528  ressasclcl  33540  ply1asclunit  33543  coe1mon  33554  deg1vr  33558  ply1degltlss  33562  gsummoncoe1fzo  33563  q1pvsca  33569  r1pvsca  33570  r1p0  33571  r1plmhm  33575  ply1degltdimlem  33618  irngnzply1lem  33685  algextdeglem8  33714  2sqr3minply  33770  cos9thpiminplylem6  33777  cos9thpiminply  33778  aks5lem2  42175  ply1asclzrhval  42176  ply1vr1smo  48371  ply1sclrmsm  48372  ply1mulgsumlem4  48378  ply1mulgsum  48379