![]() |
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 2826 | . . . 4 ⊢ (1o mPoly 𝑅) = (1o mPoly 𝑅) | |
3 | eqid 2826 | . . . 4 ⊢ (1o mPwSer 𝑅) = (1o mPwSer 𝑅) | |
4 | eqid 2826 | . . . 4 ⊢ (Base‘(1o mPoly 𝑅)) = (Base‘(1o mPoly 𝑅)) | |
5 | ply1val.2 | . . . . 5 ⊢ 𝑆 = (PwSer1‘𝑅) | |
6 | eqid 2826 | . . . . 5 ⊢ (Base‘𝑆) = (Base‘𝑆) | |
7 | 5, 6, 3 | psr1bas2 19921 | . . . 4 ⊢ (Base‘𝑆) = (Base‘(1o mPwSer 𝑅)) |
8 | 2, 3, 4, 7 | mplbasss 19794 | . . 3 ⊢ (Base‘(1o mPoly 𝑅)) ⊆ (Base‘𝑆) |
9 | ply1val.1 | . . . . 5 ⊢ 𝑃 = (Poly1‘𝑅) | |
10 | 9, 5 | ply1val 19925 | . . . 4 ⊢ 𝑃 = (𝑆 ↾s (Base‘(1o mPoly 𝑅))) |
11 | 10, 6 | ressbas2 16295 | . . 3 ⊢ ((Base‘(1o mPoly 𝑅)) ⊆ (Base‘𝑆) → (Base‘(1o mPoly 𝑅)) = (Base‘𝑃)) |
12 | 8, 11 | ax-mp 5 | . 2 ⊢ (Base‘(1o mPoly 𝑅)) = (Base‘𝑃) |
13 | 1, 12 | eqtr4i 2853 | 1 ⊢ 𝑈 = (Base‘(1o mPoly 𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 ⊆ wss 3799 ‘cfv 6124 (class class class)co 6906 1oc1o 7820 Basecbs 16223 mPwSer cmps 19713 mPoly cmpl 19715 PwSer1cps1 19906 Poly1cpl1 19908 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-rep 4995 ax-sep 5006 ax-nul 5014 ax-pow 5066 ax-pr 5128 ax-un 7210 ax-cnex 10309 ax-resscn 10310 ax-1cn 10311 ax-icn 10312 ax-addcl 10313 ax-addrcl 10314 ax-mulcl 10315 ax-mulrcl 10316 ax-mulcom 10317 ax-addass 10318 ax-mulass 10319 ax-distr 10320 ax-i2m1 10321 ax-1ne0 10322 ax-1rid 10323 ax-rnegex 10324 ax-rrecex 10325 ax-cnre 10326 ax-pre-lttri 10327 ax-pre-lttrn 10328 ax-pre-ltadd 10329 ax-pre-mulgt0 10330 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3or 1114 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ne 3001 df-nel 3104 df-ral 3123 df-rex 3124 df-reu 3125 df-rab 3127 df-v 3417 df-sbc 3664 df-csb 3759 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-pss 3815 df-nul 4146 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4660 df-iun 4743 df-br 4875 df-opab 4937 df-mpt 4954 df-tr 4977 df-id 5251 df-eprel 5256 df-po 5264 df-so 5265 df-fr 5302 df-we 5304 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-rn 5354 df-res 5355 df-ima 5356 df-pred 5921 df-ord 5967 df-on 5968 df-lim 5969 df-suc 5970 df-iota 6087 df-fun 6126 df-fn 6127 df-f 6128 df-f1 6129 df-fo 6130 df-f1o 6131 df-fv 6132 df-riota 6867 df-ov 6909 df-oprab 6910 df-mpt2 6911 df-om 7328 df-wrecs 7673 df-recs 7735 df-rdg 7773 df-er 8010 df-en 8224 df-dom 8225 df-sdom 8226 df-pnf 10394 df-mnf 10395 df-xr 10396 df-ltxr 10397 df-le 10398 df-sub 10588 df-neg 10589 df-nn 11352 df-2 11415 df-3 11416 df-4 11417 df-5 11418 df-6 11419 df-7 11420 df-8 11421 df-9 11422 df-dec 11823 df-ndx 16226 df-slot 16227 df-base 16229 df-sets 16230 df-ress 16231 df-ple 16326 df-psr 19718 df-mpl 19720 df-opsr 19722 df-psr1 19911 df-ply1 19913 |
This theorem is referenced by: ply1lss 19927 ply1subrg 19928 ply1crng 19929 ply1assa 19930 ply1basf 19933 ply1bascl2 19935 vr1cl 19948 ressply1bas2 19959 ressply1add 19961 ressply1mul 19962 ressply1vsca 19963 subrgply1 19964 ply1baspropd 19974 ply1ring 19979 ply1lmod 19983 ply1mpl0 19986 ply1mpl1 19988 subrg1asclcl 19991 subrgvr1cl 19993 coe1add 19995 coe1tm 20004 ply1coe 20027 evls1rhm 20048 evls1sca 20049 evl1rhm 20057 evl1sca 20059 evl1var 20061 evls1var 20063 mpfpf1 20076 pf1mpf 20077 deg1xrf 24241 deg1cl 24243 deg1nn0cl 24248 deg1ldg 24252 deg1leb 24255 deg1val 24256 deg1vscale 24264 deg1vsca 24265 deg1mulle2 24269 deg1le0 24271 |
Copyright terms: Public domain | W3C validator |