Theorem vr1cl 19906

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

Step	Hyp	Ref	Expression
1		vr1cl.x	. . 3 ⊢ 𝑋 = (var1‘𝑅)
2	1	vr1val 19881	. 2 ⊢ 𝑋 = ((1𝑜 mVar 𝑅)‘∅)
3		eqid 2798	. . 3 ⊢ (1𝑜 mPoly 𝑅) = (1𝑜 mPoly 𝑅)
4		eqid 2798	. . 3 ⊢ (1𝑜 mVar 𝑅) = (1𝑜 mVar 𝑅)
5		vr1cl.p	. . . 4 ⊢ 𝑃 = (Poly1‘𝑅)
6		eqid 2798	. . . 4 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅)
7		vr1cl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑃)
8	5, 6, 7	ply1bas 19884	. . 3 ⊢ 𝐵 = (Base‘(1𝑜 mPoly 𝑅))
9		1onn 7958	. . . 4 ⊢ 1𝑜 ∈ ω
10	9	a1i 11	. . 3 ⊢ (𝑅 ∈ Ring → 1𝑜 ∈ ω)
11		id 22	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Ring)
12		0lt1o 7823	. . . 4 ⊢ ∅ ∈ 1𝑜
13	12	a1i 11	. . 3 ⊢ (𝑅 ∈ Ring → ∅ ∈ 1𝑜)
14	3, 4, 8, 10, 11, 13	mvrcl 19769	. 2 ⊢ (𝑅 ∈ Ring → ((1𝑜 mVar 𝑅)‘∅) ∈ 𝐵)
15	2, 14	syl5eqel 2881	1 ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1653   ∈ wcel 2157  ∅c0 4114  ‘cfv 6100  (class class class)co 6877  ωcom 7298  1_𝑜c1o 7791  Basecbs 16181  Ringcrg 18860   mVar cmvr 19672   mPoly cmpl 19673  PwSer₁cps1 19864  var₁cv1 19865  Poly₁cpl1 19866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-rep 4963  ax-sep 4974  ax-nul 4982  ax-pow 5034  ax-pr 5096  ax-un 7182  ax-cnex 10279  ax-resscn 10280  ax-1cn 10281  ax-icn 10282  ax-addcl 10283  ax-addrcl 10284  ax-mulcl 10285  ax-mulrcl 10286  ax-mulcom 10287  ax-addass 10288  ax-mulass 10289  ax-distr 10290  ax-i2m1 10291  ax-1ne0 10292  ax-1rid 10293  ax-rnegex 10294  ax-rrecex 10295  ax-cnre 10296  ax-pre-lttri 10297  ax-pre-lttrn 10298  ax-pre-ltadd 10299  ax-pre-mulgt0 10300

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ne 2971  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3386  df-sbc 3633  df-csb 3728  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-pss 3784  df-nul 4115  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4628  df-int 4667  df-iun 4711  df-br 4843  df-opab 4905  df-mpt 4922  df-tr 4945  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5897  df-ord 5943  df-on 5944  df-lim 5945  df-suc 5946  df-iota 6063  df-fun 6102  df-fn 6103  df-f 6104  df-f1 6105  df-fo 6106  df-f1o 6107  df-fv 6108  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-of 7130  df-om 7299  df-1st 7400  df-2nd 7401  df-supp 7532  df-wrecs 7644  df-recs 7706  df-rdg 7744  df-1o 7798  df-oadd 7802  df-er 7981  df-map 8096  df-en 8195  df-dom 8196  df-sdom 8197  df-fin 8198  df-fsupp 8517  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10557  df-neg 10558  df-nn 11312  df-2 11373  df-3 11374  df-4 11375  df-5 11376  df-6 11377  df-7 11378  df-8 11379  df-9 11380  df-n0 11578  df-z 11664  df-dec 11781  df-uz 11928  df-fz 12578  df-struct 16183  df-ndx 16184  df-slot 16185  df-base 16187  df-sets 16188  df-ress 16189  df-plusg 16277  df-mulr 16278  df-sca 16280  df-vsca 16281  df-tset 16283  df-ple 16284  df-0g 16414  df-mgm 17554  df-sgrp 17596  df-mnd 17607  df-grp 17738  df-mgp 18803  df-ur 18815  df-ring 18862  df-psr 19676  df-mvr 19677  df-mpl 19678  df-opsr 19680  df-psr1 19869  df-vr1 19870  df-ply1 19871

This theorem is referenced by:  ply1moncl  19960  coe1pwmul  19968  ply1scltm  19970  ply1coefsupp  19984  ply1coe  19985  gsummoncoe1  19993  lply1binom  19995  evls1varpw  20010  evl1var  20019  evl1vard  20020  evls1var  20021  pf1id  20030  evl1scvarpw  20046  evl1scvarpwval  20047  evl1gsummon  20048  pmatcollpwscmatlem1  20919  mply1topmatcllem  20933  mply1topmatcl  20935  pm2mpghm  20946  monmat2matmon  20954  pm2mp  20955  chmatcl  20958  chmatval  20959  chpmat0d  20964  chpmat1dlem  20965  chpmat1d  20966  chpdmatlem0  20967  chpdmatlem2  20969  chpdmatlem3  20970  chpscmat  20972  chpscmatgsumbin  20974  chpscmatgsummon  20975  chp0mat  20976  chpidmat  20977  chfacfscmulcl  20987  chfacfscmul0  20988  chfacfscmulgsum  20990  cpmadugsumlemB  21004  cpmadugsumlemC  21005  cpmadugsumlemF  21006  cpmadugsumfi  21007  cpmidgsum2  21009  deg1pw  24218  ply1remlem  24260  fta1blem  24266  plypf1  24306  lgsqrlem2  25421  lgsqrlem3  25422  lgsqrlem4  25423  hbtlem4  38470  idomrootle  38547  ply1vr1smo  42957  ply1mulgsumlem4  42965  ply1mulgsum  42966  linply1  42969