Theorem subrgvr1cl

Description: The variables in a polynomial algebra are contained in every subring algebra. (Contributed by Mario Carneiro, 5-Jul-2015)

	Ref	Expression
Hypotheses	subrgvr1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	subrgvr1.r	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
	subrgvr1.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
	subrgvr1cl.u	⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
	subrgvr1cl.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
Assertion	subrgvr1cl	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		subrgvr1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
2		subrgvr1.r	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
3		subrgvr1.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
4		subrgvr1cl.u	⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
5		subrgvr1cl.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
6	1	vr1val	⊢ 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )
7		eqid	⊢ ( 1o mVar 𝑅 ) = ( 1o mVar 𝑅 )
8		1on	⊢ 1o ∈ On
9	8	a1i	⊢ ( 𝜑 → 1o ∈ On )
10		eqid	⊢ ( 1o mPoly 𝐻 ) = ( 1o mPoly 𝐻 )
11		eqid	⊢ ( PwSer1 ‘ 𝐻 ) = ( PwSer1 ‘ 𝐻 )
12	4 11 5	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝐻 ) )
13	7 9 2 3 10 12	subrgmvrf	⊢ ( 𝜑 → ( 1o mVar 𝑅 ) : 1o ⟶ 𝐵 )
14		0lt1o	⊢ ∅ ∈ 1o
15		ffvelrn	⊢ ( ( ( 1o mVar 𝑅 ) : 1o ⟶ 𝐵 ∧ ∅ ∈ 1o ) → ( ( 1o mVar 𝑅 ) ‘ ∅ ) ∈ 𝐵 )
16	13 14 15	sylancl	⊢ ( 𝜑 → ( ( 1o mVar 𝑅 ) ‘ ∅ ) ∈ 𝐵 )
17	6 16	eqeltrid	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )