ply1sca - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ply1sca		Structured version Visualization version GIF version

Theorem ply1sca 22171

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

**Hypothesis**
Ref	Expression
ply1lmod.p	⊢ 𝑃 = (Poly₁‘𝑅)

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

**Proof of Theorem ply1sca**
Step	Hyp	Ref	Expression
1		eqid 2731	. . 3 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
2	1	psr1sca 22168	. 2 ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘(PwSer₁‘𝑅)))
3		fvex 6841	. . 3 ⊢ (Base‘(1_o mPoly 𝑅)) ∈ V
4		ply1lmod.p	. . . . 5 ⊢ 𝑃 = (Poly₁‘𝑅)
5	4, 1	ply1val 22112	. . . 4 ⊢ 𝑃 = ((PwSer₁‘𝑅) ↾_s (Base‘(1_o mPoly 𝑅)))
6		eqid 2731	. . . 4 ⊢ (Scalar‘(PwSer₁‘𝑅)) = (Scalar‘(PwSer₁‘𝑅))
7	5, 6	resssca 17253	. . 3 ⊢ ((Base‘(1_o mPoly 𝑅)) ∈ V → (Scalar‘(PwSer₁‘𝑅)) = (Scalar‘𝑃))
8	3, 7	ax-mp 5	. 2 ⊢ (Scalar‘(PwSer₁‘𝑅)) = (Scalar‘𝑃)
9	2, 8	eqtrdi 2782	1 ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘𝑃))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2111 Vcvv 3436 ‘cfv 6487 (class class class)co 7352 1_oc1o 8384 Basecbs 17126 Scalarcsca 17170 mPoly cmpl 21849 PwSer₁cps1 22093 Poly₁cpl1 22095

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5219 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-cnex 11068 ax-resscn 11069 ax-1cn 11070 ax-icn 11071 ax-addcl 11072 ax-addrcl 11073 ax-mulcl 11074 ax-mulrcl 11075 ax-mulcom 11076 ax-addass 11077 ax-mulass 11078 ax-distr 11079 ax-i2m1 11080 ax-1ne0 11081 ax-1rid 11082 ax-rnegex 11083 ax-rrecex 11084 ax-cnre 11085 ax-pre-lttri 11086 ax-pre-lttrn 11087 ax-pre-ltadd 11088 ax-pre-mulgt0 11089

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-tp 4580 df-op 4582 df-uni 4859 df-iun 4943 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6254 df-ord 6315 df-on 6316 df-lim 6317 df-suc 6318 df-iota 6443 df-fun 6489 df-fn 6490 df-f 6491 df-f1 6492 df-fo 6493 df-f1o 6494 df-fv 6495 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-of 7616 df-om 7803 df-1st 7927 df-2nd 7928 df-supp 8097 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-1o 8391 df-er 8628 df-map 8758 df-en 8876 df-dom 8877 df-sdom 8878 df-fin 8879 df-fsupp 9252 df-pnf 11154 df-mnf 11155 df-xr 11156 df-ltxr 11157 df-le 11158 df-sub 11352 df-neg 11353 df-nn 12132 df-2 12194 df-3 12195 df-4 12196 df-5 12197 df-6 12198 df-7 12199 df-8 12200 df-9 12201 df-n0 12388 df-z 12475 df-dec 12595 df-uz 12739 df-fz 13414 df-struct 17064 df-sets 17081 df-slot 17099 df-ndx 17111 df-base 17127 df-ress 17148 df-plusg 17180 df-mulr 17181 df-sca 17183 df-vsca 17184 df-tset 17186 df-ple 17187 df-psr 21852 df-opsr 21856 df-psr1 22098 df-ply1 22100

This theorem is referenced by: ply1sca2 22172 ply1ascl0 22173 ply1ascl1 22174 ply10s0 22176 ply1ascl 22178 coe1pwmul 22199 ply1scl0 22210 ply1scl1 22213 ply1idvr1OLD 22216 ply1coefsupp 22218 ply1coe 22219 cply1coe0bi 22223 ply1chr 22227 gsumsmonply1 22228 gsummoncoe1 22229 lply1binomsc 22232 ply1fermltlchr 22233 evls1sca 22244 evl1vsd 22265 evl1scvarpw 22284 evl1gsummon 22286 evls1fpws 22290 evls1vsca 22294 asclply1subcl 22295 evls1maplmhm 22298 cpmatacl 22637 cpmatinvcl 22638 mat2pmatbas 22647 mat2pmatghm 22651 mat2pmatmul 22652 mat2pmatlin 22656 decpmatid 22691 pmatcollpw2lem 22698 monmatcollpw 22700 pmatcollpwlem 22701 pmatcollpwscmatlem1 22710 pm2mpcl 22718 idpm2idmp 22722 mply1topmatcllem 22724 mply1topmatcl 22726 mp2pm2mplem4 22730 mp2pm2mplem5 22731 pm2mpghmlem2 22733 pm2mpghm 22737 pm2mpmhmlem1 22739 pm2mpmhmlem2 22740 monmat2matmon 22745 chpscmat 22763 chpscmatgsumbin 22765 chpscmatgsummon 22766 deg1pwle 26058 deg1pw 26059 ply1remlem 26103 fta1blem 26109 plypf1 26150 ply1lvec 33529 ressasclcl 33541 ply1asclunit 33544 coe1mon 33556 deg1vr 33560 ply1degltlss 33564 gsummoncoe1fzo 33565 q1pvsca 33571 r1pvsca 33572 r1p0 33573 r1plmhm 33577 ply1degltdimlem 33642 irngnzply1lem 33710 extdgfialglem2 33713 algextdeglem8 33744 2sqr3minply 33800 cos9thpiminplylem6 33807 cos9thpiminply 33808 aks5lem2 42286 ply1asclzrhval 42287 ply1vr1smo 48488 ply1sclrmsm 48489 ply1mulgsumlem4 48495 ply1mulgsum 48496

W3C validator