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	2 3	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
8		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
9	8	a1i	$$⊢R\in \mathrm{Ring}\to 1_{𝑜}\in \mathrm{\omega }$$
10		id	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Ring}$$
11		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
12	11	a1i	$$⊢R\in \mathrm{Ring}\to \varnothing \in 1_{𝑜}$$
13	5 6 7 9 10 12	mvrcl	$$⊢R\in \mathrm{Ring}\to \left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)\in B$$
14	4 13	eqeltrid	$$⊢R\in \mathrm{Ring}\to X\in B$$