| 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 2733 | . . 3 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅) | |
| 2 | 1 | psr1sca 22172 | . 2 ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘(PwSer1‘𝑅))) |
| 3 | fvex 6844 | . . 3 ⊢ (Base‘(1o mPoly 𝑅)) ∈ V | |
| 4 | ply1lmod.p | . . . . 5 ⊢ 𝑃 = (Poly1‘𝑅) | |
| 5 | 4, 1 | ply1val 22116 | . . . 4 ⊢ 𝑃 = ((PwSer1‘𝑅) ↾s (Base‘(1o mPoly 𝑅))) |
| 6 | eqid 2733 | . . . 4 ⊢ (Scalar‘(PwSer1‘𝑅)) = (Scalar‘(PwSer1‘𝑅)) | |
| 7 | 5, 6 | resssca 17257 | . . 3 ⊢ ((Base‘(1o mPoly 𝑅)) ∈ V → (Scalar‘(PwSer1‘𝑅)) = (Scalar‘𝑃)) |
| 8 | 3, 7 | ax-mp 5 | . 2 ⊢ (Scalar‘(PwSer1‘𝑅)) = (Scalar‘𝑃) |
| 9 | 2, 8 | eqtrdi 2784 | 1 ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘𝑃)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2113 Vcvv 3438 ‘cfv 6489 (class class class)co 7355 1oc1o 8387 Basecbs 17130 Scalarcsca 17174 mPoly cmpl 21853 PwSer1cps1 22097 Poly1cpl1 22099 |
| 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 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7677 ax-cnex 11072 ax-resscn 11073 ax-1cn 11074 ax-icn 11075 ax-addcl 11076 ax-addrcl 11077 ax-mulcl 11078 ax-mulrcl 11079 ax-mulcom 11080 ax-addass 11081 ax-mulass 11082 ax-distr 11083 ax-i2m1 11084 ax-1ne0 11085 ax-1rid 11086 ax-rnegex 11087 ax-rrecex 11088 ax-cnre 11089 ax-pre-lttri 11090 ax-pre-lttrn 11091 ax-pre-ltadd 11092 ax-pre-mulgt0 11093 |
| 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 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2883 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3059 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4861 df-iun 4945 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-riota 7312 df-ov 7358 df-oprab 7359 df-mpo 7360 df-of 7619 df-om 7806 df-1st 7930 df-2nd 7931 df-supp 8100 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-1o 8394 df-er 8631 df-map 8761 df-en 8879 df-dom 8880 df-sdom 8881 df-fin 8882 df-fsupp 9256 df-pnf 11158 df-mnf 11159 df-xr 11160 df-ltxr 11161 df-le 11162 df-sub 11356 df-neg 11357 df-nn 12136 df-2 12198 df-3 12199 df-4 12200 df-5 12201 df-6 12202 df-7 12203 df-8 12204 df-9 12205 df-n0 12392 df-z 12479 df-dec 12599 df-uz 12743 df-fz 13418 df-struct 17068 df-sets 17085 df-slot 17103 df-ndx 17115 df-base 17131 df-ress 17152 df-plusg 17184 df-mulr 17185 df-sca 17187 df-vsca 17188 df-tset 17190 df-ple 17191 df-psr 21856 df-opsr 21860 df-psr1 22102 df-ply1 22104 |
| This theorem is referenced by: ply1sca2 22176 ply1ascl0 22177 ply1ascl1 22178 ply10s0 22180 ply1ascl 22182 coe1pwmul 22203 ply1scl0 22214 ply1scl1 22217 ply1idvr1OLD 22220 ply1coefsupp 22222 ply1coe 22223 cply1coe0bi 22227 ply1chr 22231 gsumsmonply1 22232 gsummoncoe1 22233 lply1binomsc 22236 ply1fermltlchr 22237 evls1sca 22248 evl1vsd 22269 evl1scvarpw 22288 evl1gsummon 22290 evls1fpws 22294 evls1vsca 22298 asclply1subcl 22299 evls1maplmhm 22302 cpmatacl 22641 cpmatinvcl 22642 mat2pmatbas 22651 mat2pmatghm 22655 mat2pmatmul 22656 mat2pmatlin 22660 decpmatid 22695 pmatcollpw2lem 22702 monmatcollpw 22704 pmatcollpwlem 22705 pmatcollpwscmatlem1 22714 pm2mpcl 22722 idpm2idmp 22726 mply1topmatcllem 22728 mply1topmatcl 22730 mp2pm2mplem4 22734 mp2pm2mplem5 22735 pm2mpghmlem2 22737 pm2mpghm 22741 pm2mpmhmlem1 22743 pm2mpmhmlem2 22744 monmat2matmon 22749 chpscmat 22767 chpscmatgsumbin 22769 chpscmatgsummon 22770 deg1pwle 26062 deg1pw 26063 ply1remlem 26107 fta1blem 26113 plypf1 26154 ply1lvec 33533 ressasclcl 33545 ply1asclunit 33548 coe1mon 33560 deg1vr 33564 ply1degltlss 33568 gsummoncoe1fzo 33569 q1pvsca 33575 r1pvsca 33576 r1p0 33577 r1plmhm 33581 ply1degltdimlem 33646 irngnzply1lem 33714 extdgfialglem2 33717 algextdeglem8 33748 2sqr3minply 33804 cos9thpiminplylem6 33811 cos9thpiminply 33812 aks5lem2 42290 ply1asclzrhval 42291 ply1vr1smo 48497 ply1sclrmsm 48498 ply1mulgsumlem4 48504 ply1mulgsum 48505 |
| Copyright terms: Public domain | W3C validator |