Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > vr1cl | Structured version Visualization version GIF version |
Description: The generator of a univariate polynomial algebra is contained in the base set. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
Ref | Expression |
---|---|
vr1cl.x | ⊢ 𝑋 = (var1‘𝑅) |
vr1cl.p | ⊢ 𝑃 = (Poly1‘𝑅) |
vr1cl.b | ⊢ 𝐵 = (Base‘𝑃) |
Ref | Expression |
---|---|
vr1cl | ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vr1cl.x | . . 3 ⊢ 𝑋 = (var1‘𝑅) | |
2 | 1 | vr1val 21145 | . 2 ⊢ 𝑋 = ((1o mVar 𝑅)‘∅) |
3 | eqid 2739 | . . 3 ⊢ (1o mPoly 𝑅) = (1o mPoly 𝑅) | |
4 | eqid 2739 | . . 3 ⊢ (1o mVar 𝑅) = (1o mVar 𝑅) | |
5 | vr1cl.p | . . . 4 ⊢ 𝑃 = (Poly1‘𝑅) | |
6 | eqid 2739 | . . . 4 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅) | |
7 | vr1cl.b | . . . 4 ⊢ 𝐵 = (Base‘𝑃) | |
8 | 5, 6, 7 | ply1bas 21148 | . . 3 ⊢ 𝐵 = (Base‘(1o mPoly 𝑅)) |
9 | 1onn 8391 | . . . 4 ⊢ 1o ∈ ω | |
10 | 9 | a1i 11 | . . 3 ⊢ (𝑅 ∈ Ring → 1o ∈ ω) |
11 | id 22 | . . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Ring) | |
12 | 0lt1o 8255 | . . . 4 ⊢ ∅ ∈ 1o | |
13 | 12 | a1i 11 | . . 3 ⊢ (𝑅 ∈ Ring → ∅ ∈ 1o) |
14 | 3, 4, 8, 10, 11, 13 | mvrcl 21009 | . 2 ⊢ (𝑅 ∈ Ring → ((1o mVar 𝑅)‘∅) ∈ 𝐵) |
15 | 2, 14 | eqeltrid 2844 | 1 ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ∈ wcel 2112 ∅c0 4254 ‘cfv 6401 (class class class)co 7235 ωcom 7666 1oc1o 8219 Basecbs 16793 Ringcrg 19595 mVar cmvr 20896 mPoly cmpl 20897 PwSer1cps1 21128 var1cv1 21129 Poly1cpl1 21130 |
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 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-rep 5196 ax-sep 5209 ax-nul 5216 ax-pow 5275 ax-pr 5339 ax-un 7545 ax-cnex 10815 ax-resscn 10816 ax-1cn 10817 ax-icn 10818 ax-addcl 10819 ax-addrcl 10820 ax-mulcl 10821 ax-mulrcl 10822 ax-mulcom 10823 ax-addass 10824 ax-mulass 10825 ax-distr 10826 ax-i2m1 10827 ax-1ne0 10828 ax-1rid 10829 ax-rnegex 10830 ax-rrecex 10831 ax-cnre 10832 ax-pre-lttri 10833 ax-pre-lttrn 10834 ax-pre-ltadd 10835 ax-pre-mulgt0 10836 |
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 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3425 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4255 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5153 df-tr 5179 df-id 5472 df-eprel 5478 df-po 5486 df-so 5487 df-fr 5527 df-we 5529 df-xp 5575 df-rel 5576 df-cnv 5577 df-co 5578 df-dm 5579 df-rn 5580 df-res 5581 df-ima 5582 df-pred 6179 df-ord 6237 df-on 6238 df-lim 6239 df-suc 6240 df-iota 6359 df-fun 6403 df-fn 6404 df-f 6405 df-f1 6406 df-fo 6407 df-f1o 6408 df-fv 6409 df-riota 7192 df-ov 7238 df-oprab 7239 df-mpo 7240 df-of 7491 df-om 7667 df-1st 7783 df-2nd 7784 df-supp 7928 df-wrecs 8071 df-recs 8132 df-rdg 8170 df-1o 8226 df-er 8415 df-map 8534 df-en 8651 df-dom 8652 df-sdom 8653 df-fin 8654 df-fsupp 9016 df-pnf 10899 df-mnf 10900 df-xr 10901 df-ltxr 10902 df-le 10903 df-sub 11094 df-neg 11095 df-nn 11861 df-2 11923 df-3 11924 df-4 11925 df-5 11926 df-6 11927 df-7 11928 df-8 11929 df-9 11930 df-n0 12121 df-z 12207 df-dec 12324 df-uz 12469 df-fz 13126 df-struct 16733 df-sets 16750 df-slot 16768 df-ndx 16778 df-base 16794 df-ress 16818 df-plusg 16848 df-mulr 16849 df-sca 16851 df-vsca 16852 df-tset 16854 df-ple 16855 df-0g 16979 df-mgm 18147 df-sgrp 18196 df-mnd 18207 df-grp 18401 df-mgp 19538 df-ur 19550 df-ring 19597 df-psr 20900 df-mvr 20901 df-mpl 20902 df-opsr 20904 df-psr1 21133 df-vr1 21134 df-ply1 21135 |
This theorem is referenced by: ply1moncl 21224 coe1pwmul 21232 ply1scltm 21234 ply1coefsupp 21248 ply1coe 21249 gsummoncoe1 21257 lply1binom 21259 evls1varpw 21275 evl1var 21284 evl1vard 21285 evls1var 21286 pf1id 21295 evl1scvarpw 21311 evl1scvarpwval 21312 evl1gsummon 21313 pmatcollpwscmatlem1 21718 mply1topmatcllem 21732 mply1topmatcl 21734 pm2mpghm 21745 monmat2matmon 21753 pm2mp 21754 chmatcl 21757 chmatval 21758 chpmat0d 21763 chpmat1dlem 21764 chpmat1d 21765 chpdmatlem0 21766 chpdmatlem2 21768 chpdmatlem3 21769 chpscmat 21771 chpscmatgsumbin 21773 chpscmatgsummon 21774 chp0mat 21775 chpidmat 21776 chfacfscmulcl 21786 chfacfscmul0 21787 chfacfscmulgsum 21789 cpmadugsumlemB 21803 cpmadugsumlemC 21804 cpmadugsumlemF 21805 cpmadugsumfi 21806 cpmidgsum2 21808 deg1pw 25050 ply1remlem 25092 fta1blem 25098 plypf1 25138 lgsqrlem2 26260 lgsqrlem3 26261 lgsqrlem4 26262 ply1fermltl 31416 hbtlem4 40702 idomrootle 40771 ply1vr1smo 45441 ply1mulgsumlem4 45449 ply1mulgsum 45450 linply1 45453 |
Copyright terms: Public domain | W3C validator |