vr1cl

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

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

Metamath Proof Explorer