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	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	vr1cl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	vr1cl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		vr1cl.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
2		vr1cl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		vr1cl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4	1	vr1val	⊢ 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )
5		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
6		eqid	⊢ ( 1o mVar 𝑅 ) = ( 1o mVar 𝑅 )
7	2 3	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
8		1onn	⊢ 1o ∈ ω
9	8	a1i	⊢ ( 𝑅 ∈ Ring → 1o ∈ ω )
10		id	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Ring )
11		0lt1o	⊢ ∅ ∈ 1o
12	11	a1i	⊢ ( 𝑅 ∈ Ring → ∅ ∈ 1o )
13	5 6 7 9 10 12	mvrcl	⊢ ( 𝑅 ∈ Ring → ( ( 1o mVar 𝑅 ) ‘ ∅ ) ∈ 𝐵 )
14	4 13	eqeltrid	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )