Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ply1sca | Structured version Visualization version GIF version |
Description: Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
Ref | Expression |
---|---|
ply1lmod.p | ⊢ 𝑃 = (Poly1‘𝑅) |
Ref | Expression |
---|---|
ply1sca | ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘𝑃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2738 | . . 3 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅) | |
2 | 1 | psr1sca 21198 | . 2 ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘(PwSer1‘𝑅))) |
3 | fvex 6749 | . . 3 ⊢ (Base‘(1o mPoly 𝑅)) ∈ V | |
4 | ply1lmod.p | . . . . 5 ⊢ 𝑃 = (Poly1‘𝑅) | |
5 | 4, 1 | ply1val 21142 | . . . 4 ⊢ 𝑃 = ((PwSer1‘𝑅) ↾s (Base‘(1o mPoly 𝑅))) |
6 | eqid 2738 | . . . 4 ⊢ (Scalar‘(PwSer1‘𝑅)) = (Scalar‘(PwSer1‘𝑅)) | |
7 | 5, 6 | resssca 16904 | . . 3 ⊢ ((Base‘(1o mPoly 𝑅)) ∈ V → (Scalar‘(PwSer1‘𝑅)) = (Scalar‘𝑃)) |
8 | 3, 7 | ax-mp 5 | . 2 ⊢ (Scalar‘(PwSer1‘𝑅)) = (Scalar‘𝑃) |
9 | 2, 8 | eqtrdi 2795 | 1 ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘𝑃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ∈ wcel 2111 Vcvv 3421 ‘cfv 6398 (class class class)co 7232 1oc1o 8216 Basecbs 16788 Scalarcsca 16833 mPoly cmpl 20892 PwSer1cps1 21123 Poly1cpl1 21125 |
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 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-rep 5194 ax-sep 5207 ax-nul 5214 ax-pow 5273 ax-pr 5337 ax-un 7542 ax-cnex 10810 ax-resscn 10811 ax-1cn 10812 ax-icn 10813 ax-addcl 10814 ax-addrcl 10815 ax-mulcl 10816 ax-mulrcl 10817 ax-mulcom 10818 ax-addass 10819 ax-mulass 10820 ax-distr 10821 ax-i2m1 10822 ax-1ne0 10823 ax-1rid 10824 ax-rnegex 10825 ax-rrecex 10826 ax-cnre 10827 ax-pre-lttri 10828 ax-pre-lttrn 10829 ax-pre-ltadd 10830 ax-pre-mulgt0 10831 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2072 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3067 df-rex 3068 df-reu 3069 df-rab 3071 df-v 3423 df-sbc 3710 df-csb 3827 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4253 df-if 4455 df-pw 4530 df-sn 4557 df-pr 4559 df-tp 4561 df-op 4563 df-uni 4835 df-iun 4921 df-br 5069 df-opab 5131 df-mpt 5151 df-tr 5177 df-id 5470 df-eprel 5475 df-po 5483 df-so 5484 df-fr 5524 df-we 5526 df-xp 5572 df-rel 5573 df-cnv 5574 df-co 5575 df-dm 5576 df-rn 5577 df-res 5578 df-ima 5579 df-pred 6176 df-ord 6234 df-on 6235 df-lim 6236 df-suc 6237 df-iota 6356 df-fun 6400 df-fn 6401 df-f 6402 df-f1 6403 df-fo 6404 df-f1o 6405 df-fv 6406 df-riota 7189 df-ov 7235 df-oprab 7236 df-mpo 7237 df-of 7488 df-om 7664 df-1st 7780 df-2nd 7781 df-supp 7925 df-wrecs 8068 df-recs 8129 df-rdg 8167 df-1o 8223 df-er 8412 df-map 8531 df-en 8648 df-dom 8649 df-sdom 8650 df-fin 8651 df-fsupp 9011 df-pnf 10894 df-mnf 10895 df-xr 10896 df-ltxr 10897 df-le 10898 df-sub 11089 df-neg 11090 df-nn 11856 df-2 11918 df-3 11919 df-4 11920 df-5 11921 df-6 11922 df-7 11923 df-8 11924 df-9 11925 df-n0 12116 df-z 12202 df-dec 12319 df-uz 12464 df-fz 13121 df-struct 16728 df-sets 16745 df-slot 16763 df-ndx 16773 df-base 16789 df-ress 16813 df-plusg 16843 df-mulr 16844 df-sca 16846 df-vsca 16847 df-tset 16849 df-ple 16850 df-psr 20895 df-opsr 20899 df-psr1 21128 df-ply1 21130 |
This theorem is referenced by: ply1sca2 21202 ply10s0 21204 ply1ascl 21206 coe1pwmul 21227 ply1idvr1 21241 ply1coefsupp 21243 ply1coe 21244 cply1coe0bi 21248 gsumsmonply1 21251 gsummoncoe1 21252 lply1binomsc 21255 evls1sca 21266 evl1vsd 21287 evl1scvarpw 21306 evl1gsummon 21308 cpmatacl 21640 cpmatinvcl 21641 mat2pmatbas 21650 mat2pmatghm 21654 mat2pmatmul 21655 mat2pmatlin 21659 decpmatid 21694 pmatcollpw2lem 21701 monmatcollpw 21703 pmatcollpwlem 21704 pmatcollpwscmatlem1 21713 pm2mpcl 21721 idpm2idmp 21725 mply1topmatcllem 21727 mply1topmatcl 21729 mp2pm2mplem4 21733 mp2pm2mplem5 21734 pm2mpghmlem2 21736 pm2mpghm 21740 pm2mpmhmlem1 21742 pm2mpmhmlem2 21743 monmat2matmon 21748 chpscmat 21766 chpscmatgsumbin 21768 chpscmatgsummon 21769 deg1pwle 25044 deg1pw 25045 ply1remlem 25087 fta1blem 25093 plypf1 25133 ply1chr 31410 ply1fermltl 31411 ply1vr1smo 45426 ply1sclrmsm 45428 ply1mulgsumlem4 45434 ply1mulgsum 45435 |
Copyright terms: Public domain | W3C validator |