Theorem ply1sca 22158

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 2727	. . 3 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅)
2	1	psr1sca 22155	. 2 ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘(PwSer1‘𝑅)))
3		fvex 6904	. . 3 ⊢ (Base‘(1o mPoly 𝑅)) ∈ V
4		ply1lmod.p	. . . . 5 ⊢ 𝑃 = (Poly1‘𝑅)
5	4, 1	ply1val 22100	. . . 4 ⊢ 𝑃 = ((PwSer1‘𝑅) ↾s (Base‘(1o mPoly 𝑅)))
6		eqid 2727	. . . 4 ⊢ (Scalar‘(PwSer1‘𝑅)) = (Scalar‘(PwSer1‘𝑅))
7	5, 6	resssca 17315	. . 3 ⊢ ((Base‘(1o mPoly 𝑅)) ∈ V → (Scalar‘(PwSer1‘𝑅)) = (Scalar‘𝑃))
8	3, 7	ax-mp 5	. 2 ⊢ (Scalar‘(PwSer1‘𝑅)) = (Scalar‘𝑃)
9	2, 8	eqtrdi 2783	1 ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘𝑃))

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  Vcvv 3469  ‘cfv 6542  (class class class)co 7414  1_oc1o 8473  Basecbs 17171  Scalarcsca 17227   mPoly cmpl 21826  PwSer₁cps1 22081  Poly₁cpl1 22083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-map 8838  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9378  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-z 12581  df-dec 12700  df-uz 12845  df-fz 13509  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-sca 17240  df-vsca 17241  df-tset 17243  df-ple 17244  df-psr 21829  df-opsr 21833  df-psr1 22086  df-ply1 22088

This theorem is referenced by:  ply1sca2  22159  ply1ascl0  22160  ply10s0  22162  ply1ascl  22164  coe1pwmul  22185  ply1scl0  22196  ply1scl1  22199  ply1idvr1  22201  ply1coefsupp  22203  ply1coe  22204  cply1coe0bi  22208  ply1chr  22212  gsumsmonply1  22213  gsummoncoe1  22214  lply1binomsc  22217  ply1fermltlchr  22218  evls1sca  22229  evl1vsd  22250  evl1scvarpw  22269  evl1gsummon  22271  cpmatacl  22605  cpmatinvcl  22606  mat2pmatbas  22615  mat2pmatghm  22619  mat2pmatmul  22620  mat2pmatlin  22624  decpmatid  22659  pmatcollpw2lem  22666  monmatcollpw  22668  pmatcollpwlem  22669  pmatcollpwscmatlem1  22678  pm2mpcl  22686  idpm2idmp  22690  mply1topmatcllem  22692  mply1topmatcl  22694  mp2pm2mplem4  22698  mp2pm2mplem5  22699  pm2mpghmlem2  22701  pm2mpghm  22705  pm2mpmhmlem1  22707  pm2mpmhmlem2  22708  monmat2matmon  22713  chpscmat  22731  chpscmatgsumbin  22733  chpscmatgsummon  22734  deg1pwle  26042  deg1pw  26043  ply1remlem  26086  fta1blem  26092  plypf1  26133  ply1lvec  33170  evls1fpws  33182  evls1vsca  33187  ply1ascl1  33188  ply1asclunit  33190  asclply1subcl  33193  coe1mon  33195  ply1degltlss  33199  gsummoncoe1fzo  33200  q1pvsca  33206  r1pvsca  33207  r1p0  33208  r1plmhm  33212  ply1degltdimlem  33252  irngnzply1lem  33300  evls1maplmhm  33306  algextdeglem8  33328  ply1vr1smo  47373  ply1sclrmsm  47374  ply1mulgsumlem4  47380  ply1mulgsum  47381