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		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
8	2 7 3	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
9		1onn	⊢ 1o ∈ ω
10	9	a1i	⊢ ( 𝑅 ∈ Ring → 1o ∈ ω )
11		id	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Ring )
12		0lt1o	⊢ ∅ ∈ 1o
13	12	a1i	⊢ ( 𝑅 ∈ Ring → ∅ ∈ 1o )
14	5 6 8 10 11 13	mvrcl	⊢ ( 𝑅 ∈ Ring → ( ( 1o mVar 𝑅 ) ‘ ∅ ) ∈ 𝐵 )
15	4 14	eqeltrid	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )