MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vr1cl Structured version   Visualization version   GIF version

Theorem vr1cl 21170
Description: The generator of a univariate polynomial algebra is contained in the base set. (Contributed by Stefan O'Rear, 19-Mar-2015.)
Hypotheses
Ref Expression
vr1cl.x 𝑋 = (var1𝑅)
vr1cl.p 𝑃 = (Poly1𝑅)
vr1cl.b 𝐵 = (Base‘𝑃)
Assertion
Ref Expression
vr1cl (𝑅 ∈ Ring → 𝑋𝐵)

Proof of Theorem vr1cl
StepHypRef Expression
1 vr1cl.x . . 3 𝑋 = (var1𝑅)
21vr1val 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‘𝑃)
85, 6, 7ply1bas 21148 . . 3 𝐵 = (Base‘(1o mPoly 𝑅))
9 1onn 8391 . . . 4 1o ∈ ω
109a1i 11 . . 3 (𝑅 ∈ Ring → 1o ∈ ω)
11 id 22 . . 3 (𝑅 ∈ Ring → 𝑅 ∈ Ring)
12 0lt1o 8255 . . . 4 ∅ ∈ 1o
1312a1i 11 . . 3 (𝑅 ∈ Ring → ∅ ∈ 1o)
143, 4, 8, 10, 11, 13mvrcl 21009 . 2 (𝑅 ∈ Ring → ((1o mVar 𝑅)‘∅) ∈ 𝐵)
152, 14eqeltrid 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