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 2729	. . 3 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
2	1	psr1sca 22168	. 2 ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘(PwSer₁‘𝑅)))
3		fvex 6853	. . 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 2729	. . . 4 ⊢ (Scalar‘(PwSer₁‘𝑅)) = (Scalar‘(PwSer₁‘𝑅))
7	5, 6	resssca 17283	. . 3 ⊢ ((Base‘(1_o mPoly 𝑅)) ∈ V → (Scalar‘(PwSer₁‘𝑅)) = (Scalar‘𝑃))
8	3, 7	ax-mp 5	. 2 ⊢ (Scalar‘(PwSer₁‘𝑅)) = (Scalar‘𝑃)
9	2, 8	eqtrdi 2780	1 ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘𝑃))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2109 Vcvv 3444 ‘cfv 6499 (class class class)co 7369 1_oc1o 8404 Basecbs 17156 Scalarcsca 17200 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 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 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11102 ax-resscn 11103 ax-1cn 11104 ax-icn 11105 ax-addcl 11106 ax-addrcl 11107 ax-mulcl 11108 ax-mulrcl 11109 ax-mulcom 11110 ax-addass 11111 ax-mulass 11112 ax-distr 11113 ax-i2m1 11114 ax-1ne0 11115 ax-1rid 11116 ax-rnegex 11117 ax-rrecex 11118 ax-cnre 11119 ax-pre-lttri 11120 ax-pre-lttrn 11121 ax-pre-ltadd 11122 ax-pre-mulgt0 11123

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 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-of 7633 df-om 7823 df-1st 7947 df-2nd 7948 df-supp 8117 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-er 8648 df-map 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9289 df-pnf 11188 df-mnf 11189 df-xr 11190 df-ltxr 11191 df-le 11192 df-sub 11385 df-neg 11386 df-nn 12165 df-2 12227 df-3 12228 df-4 12229 df-5 12230 df-6 12231 df-7 12232 df-8 12233 df-9 12234 df-n0 12421 df-z 12508 df-dec 12628 df-uz 12772 df-fz 13447 df-struct 17094 df-sets 17111 df-slot 17129 df-ndx 17141 df-base 17157 df-ress 17178 df-plusg 17210 df-mulr 17211 df-sca 17213 df-vsca 17214 df-tset 17216 df-ple 17217 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 26059 deg1pw 26060 ply1remlem 26104 fta1blem 26110 plypf1 26151 ply1lvec 33522 ressasclcl 33534 ply1asclunit 33537 coe1mon 33548 deg1vr 33552 ply1degltlss 33556 gsummoncoe1fzo 33557 q1pvsca 33563 r1pvsca 33564 r1p0 33565 r1plmhm 33569 ply1degltdimlem 33612 irngnzply1lem 33679 algextdeglem8 33708 2sqr3minply 33764 cos9thpiminplylem6 33771 cos9thpiminply 33772 aks5lem2 42169 ply1asclzrhval 42170 ply1vr1smo 48365 ply1sclrmsm 48366 ply1mulgsumlem4 48372 ply1mulgsum 48373

W3C validator