Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ply1bas | Structured version Visualization version GIF version |
Description: The value of the base set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.) |
Ref | Expression |
---|---|
ply1val.1 | ⊢ 𝑃 = (Poly1‘𝑅) |
ply1val.2 | ⊢ 𝑆 = (PwSer1‘𝑅) |
ply1bas.u | ⊢ 𝑈 = (Base‘𝑃) |
Ref | Expression |
---|---|
ply1bas | ⊢ 𝑈 = (Base‘(1o mPoly 𝑅)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ply1bas.u | . 2 ⊢ 𝑈 = (Base‘𝑃) | |
2 | eqid 2738 | . . . 4 ⊢ (1o mPoly 𝑅) = (1o mPoly 𝑅) | |
3 | eqid 2738 | . . . 4 ⊢ (1o mPwSer 𝑅) = (1o mPwSer 𝑅) | |
4 | eqid 2738 | . . . 4 ⊢ (Base‘(1o mPoly 𝑅)) = (Base‘(1o mPoly 𝑅)) | |
5 | ply1val.2 | . . . . 5 ⊢ 𝑆 = (PwSer1‘𝑅) | |
6 | eqid 2738 | . . . . 5 ⊢ (Base‘𝑆) = (Base‘𝑆) | |
7 | 5, 6, 3 | psr1bas2 21135 | . . . 4 ⊢ (Base‘𝑆) = (Base‘(1o mPwSer 𝑅)) |
8 | 2, 3, 4, 7 | mplbasss 20983 | . . 3 ⊢ (Base‘(1o mPoly 𝑅)) ⊆ (Base‘𝑆) |
9 | ply1val.1 | . . . . 5 ⊢ 𝑃 = (Poly1‘𝑅) | |
10 | 9, 5 | ply1val 21139 | . . . 4 ⊢ 𝑃 = (𝑆 ↾s (Base‘(1o mPoly 𝑅))) |
11 | 10, 6 | ressbas2 16815 | . . 3 ⊢ ((Base‘(1o mPoly 𝑅)) ⊆ (Base‘𝑆) → (Base‘(1o mPoly 𝑅)) = (Base‘𝑃)) |
12 | 8, 11 | ax-mp 5 | . 2 ⊢ (Base‘(1o mPoly 𝑅)) = (Base‘𝑃) |
13 | 1, 12 | eqtr4i 2769 | 1 ⊢ 𝑈 = (Base‘(1o mPoly 𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 ⊆ wss 3880 ‘cfv 6397 (class class class)co 7231 1oc1o 8215 Basecbs 16784 mPwSer cmps 20887 mPoly cmpl 20889 PwSer1cps1 21120 Poly1cpl1 21122 |
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 5193 ax-sep 5206 ax-nul 5213 ax-pow 5272 ax-pr 5336 ax-un 7541 ax-cnex 10809 ax-resscn 10810 ax-1cn 10811 ax-icn 10812 ax-addcl 10813 ax-addrcl 10814 ax-mulcl 10815 ax-mulrcl 10816 ax-mulcom 10817 ax-addass 10818 ax-mulass 10819 ax-distr 10820 ax-i2m1 10821 ax-1ne0 10822 ax-1rid 10823 ax-rnegex 10824 ax-rrecex 10825 ax-cnre 10826 ax-pre-lttri 10827 ax-pre-lttrn 10828 ax-pre-ltadd 10829 ax-pre-mulgt0 10830 |
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 3422 df-sbc 3709 df-csb 3826 df-dif 3883 df-un 3885 df-in 3887 df-ss 3897 df-pss 3899 df-nul 4252 df-if 4454 df-pw 4529 df-sn 4556 df-pr 4558 df-tp 4560 df-op 4562 df-uni 4834 df-iun 4920 df-br 5068 df-opab 5130 df-mpt 5150 df-tr 5176 df-id 5469 df-eprel 5474 df-po 5482 df-so 5483 df-fr 5523 df-we 5525 df-xp 5571 df-rel 5572 df-cnv 5573 df-co 5574 df-dm 5575 df-rn 5576 df-res 5577 df-ima 5578 df-pred 6175 df-ord 6233 df-on 6234 df-lim 6235 df-suc 6236 df-iota 6355 df-fun 6399 df-fn 6400 df-f 6401 df-f1 6402 df-fo 6403 df-f1o 6404 df-fv 6405 df-riota 7188 df-ov 7234 df-oprab 7235 df-mpo 7236 df-om 7663 df-wrecs 8067 df-recs 8128 df-rdg 8166 df-er 8411 df-en 8647 df-dom 8648 df-sdom 8649 df-pnf 10893 df-mnf 10894 df-xr 10895 df-ltxr 10896 df-le 10897 df-sub 11088 df-neg 11089 df-nn 11855 df-2 11917 df-3 11918 df-4 11919 df-5 11920 df-6 11921 df-7 11922 df-8 11923 df-9 11924 df-dec 12318 df-sets 16741 df-slot 16759 df-ndx 16769 df-base 16785 df-ress 16809 df-ple 16846 df-psr 20892 df-mpl 20894 df-opsr 20896 df-psr1 21125 df-ply1 21127 |
This theorem is referenced by: ply1lss 21141 ply1subrg 21142 ply1crng 21143 ply1assa 21144 ply1basf 21147 ply1bascl2 21149 vr1cl 21162 ressply1bas2 21173 ressply1add 21175 ressply1mul 21176 ressply1vsca 21177 subrgply1 21178 ply1baspropd 21188 ply1ring 21193 ply1lmod 21197 ply1mpl0 21200 ply1mpl1 21202 subrg1asclcl 21205 subrgvr1cl 21207 coe1add 21209 coe1tm 21218 ply1coe 21241 evls1rhm 21262 evls1sca 21263 evl1rhm 21272 evl1sca 21274 evl1var 21276 evls1var 21278 mpfpf1 21291 pf1mpf 21292 deg1xrf 25003 deg1cl 25005 deg1nn0cl 25010 deg1ldg 25014 deg1leb 25017 deg1val 25018 deg1vscale 25026 deg1vsca 25027 deg1mulle2 25031 deg1le0 25033 fply1 31405 |
Copyright terms: Public domain | W3C validator |