Theorem vr1cl

Description: The generator of a univariate polynomial algebra is contained in the base set. (Contributed by Stefan O'Rear, 19-Mar-2015)

	Ref	Expression
Hypotheses	vr1cl.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	vr1cl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	vr1cl.b	$$⊢B={\mathrm{Base}}_P$$
Assertion	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in B$$

Proof

Step	Hyp	Ref	Expression
1		vr1cl.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
2		vr1cl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		vr1cl.b	$$⊢B={\mathrm{Base}}_P$$
4	1	vr1val	$$⊢X=\left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)$$
5		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
6		eqid	$$⊢1_{𝑜}\mathrm{mVar}R=1_{𝑜}\mathrm{mVar}R$$
7		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
8	2 7 3	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
9		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
10	9	a1i	$$⊢R\in \mathrm{Ring}\to 1_{𝑜}\in \mathrm{\omega }$$
11		id	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Ring}$$
12		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
13	12	a1i	$$⊢R\in \mathrm{Ring}\to \varnothing \in 1_{𝑜}$$
14	5 6 8 10 11 13	mvrcl	$$⊢R\in \mathrm{Ring}\to \left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)\in B$$
15	4 14	eqeltrid	$$⊢R\in \mathrm{Ring}\to X\in B$$