Theorem ply1sca 22240

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 2741	. . 3 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅)
2	1	psr1sca 22237	. 2 ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘(PwSer1‘𝑅)))
3		fvex 6843	. . 3 ⊢ (Base‘(1o mPoly 𝑅)) ∈ V
4		ply1lmod.p	. . . . 5 ⊢ 𝑃 = (Poly1‘𝑅)
5	4, 1	ply1val 22182	. . . 4 ⊢ 𝑃 = ((PwSer1‘𝑅) ↾s (Base‘(1o mPoly 𝑅)))
6		eqid 2741	. . . 4 ⊢ (Scalar‘(PwSer1‘𝑅)) = (Scalar‘(PwSer1‘𝑅))
7	5, 6	resssca 17301	. . 3 ⊢ ((Base‘(1o mPoly 𝑅)) ∈ V → (Scalar‘(PwSer1‘𝑅)) = (Scalar‘𝑃))
8	3, 7	ax-mp 5	. 2 ⊢ (Scalar‘(PwSer1‘𝑅)) = (Scalar‘𝑃)
9	2, 8	eqtrdi 2792	1 ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘𝑃))

Syntax hints:   → wi 4   = wceq 1548   ∈ wcel 2121  Vcvv 3433  ‘cfv 6488  (class class class)co 7359  1_oc1o 8392  Basecbs 17174  Scalarcsca 17218   mPoly cmpl 21884  PwSer₁cps1 22163  Poly₁cpl1 22165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-rep 5201  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7681  ax-cnex 11090  ax-resscn 11091  ax-1cn 11092  ax-icn 11093  ax-addcl 11094  ax-addrcl 11095  ax-mulcl 11096  ax-mulrcl 11097  ax-mulcom 11098  ax-addass 11099  ax-mulass 11100  ax-distr 11101  ax-i2m1 11102  ax-1ne0 11103  ax-1rid 11104  ax-rnegex 11105  ax-rrecex 11106  ax-cnre 11107  ax-pre-lttri 11108  ax-pre-lttrn 11109  ax-pre-ltadd 11110  ax-pre-mulgt0 11111

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3725  df-csb 3833  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3904  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-tr 5182  df-id 5515  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6255  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-riota 7316  df-ov 7362  df-oprab 7363  df-mpo 7364  df-of 7623  df-om 7810  df-1st 7933  df-2nd 7934  df-supp 8103  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8343  df-1o 8399  df-er 8637  df-map 8769  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-fsupp 9269  df-pnf 11177  df-mnf 11178  df-xr 11179  df-ltxr 11180  df-le 11181  df-sub 11375  df-neg 11376  df-nn 12170  df-2 12239  df-3 12240  df-4 12241  df-5 12242  df-6 12243  df-7 12244  df-8 12245  df-9 12246  df-n0 12433  df-z 12520  df-dec 12640  df-uz 12784  df-fz 13457  df-struct 17112  df-sets 17129  df-slot 17147  df-ndx 17159  df-base 17175  df-ress 17196  df-plusg 17228  df-mulr 17229  df-sca 17231  df-vsca 17232  df-tset 17234  df-ple 17235  df-psr 21887  df-opsr 21891  df-psr1 22168  df-ply1 22170

This theorem is referenced by:  ply1sca2  22241  ply1ascl0  22242  ply1ascl1  22243  ply10s0  22245  ply1ascl  22247  coe1pwmul  22268  ply1scl0  22279  ply1scl1  22281  ply1idvr1OLD  22284  ply1coefsupp  22286  ply1coe  22287  cply1coe0bi  22291  ply1chr  22295  gsumsmonply1  22296  gsummoncoe1  22297  lply1binomsc  22300  ply1fermltlchr  22301  evls1sca  22312  evl1vsd  22333  evl1scvarpw  22352  evl1gsummon  22354  evls1fpws  22358  evls1vsca  22362  asclply1subcl  22363  evls1maplmhm  22366  cpmatacl  22702  cpmatinvcl  22703  mat2pmatbas  22712  mat2pmatghm  22716  mat2pmatmul  22717  mat2pmatlin  22721  decpmatid  22756  pmatcollpw2lem  22763  monmatcollpw  22765  pmatcollpwlem  22766  pmatcollpwscmatlem1  22775  pm2mpcl  22783  idpm2idmp  22787  mply1topmatcllem  22789  mply1topmatcl  22791  mp2pm2mplem4  22795  mp2pm2mplem5  22796  pm2mpghmlem2  22798  pm2mpghm  22802  pm2mpmhmlem1  22804  pm2mpmhmlem2  22805  monmat2matmon  22810  chpscmat  22828  chpscmatgsumbin  22830  chpscmatgsummon  22831  deg1pwle  26106  deg1pw  26107  ply1remlem  26151  fta1blem  26157  plypf1  26198  ply1lvec  33652  ressasclcl  33664  ply1asclunit  33667  coe1mon  33680  ply1coedeg  33682  deg1vr  33685  ply1degltlss  33689  gsummoncoe1fzo  33690  q1pvsca  33697  r1pvsca  33698  r1p0  33699  r1plmhm  33703  vietadeg1  33772  vietalem  33773  ply1degltdimlem  33816  irngnzply1lem  33884  extdgfialglem2  33887  algextdeglem8  33918  2sqr3minply  33974  cos9thpiminplylem6  33981  cos9thpiminply  33982  aks5lem2  42685  ply1asclzrhval  42686  ply1vr1smo  48886  ply1sclrmsm  48887  ply1mulgsumlem4  48892  ply1mulgsum  48893