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	|- X = ( var1 ` R )
	subrgvr1.r	|- ( ph -> T e. ( SubRing ` R ) )
	subrgvr1.h	|- H = ( R |`s T )
	subrgvr1cl.u	|- U = ( Poly1 ` H )
	subrgvr1cl.b	|- B = ( Base ` U )
Assertion	subrgvr1cl	|- ( ph -> X e. B )

Proof

Step	Hyp	Ref	Expression
1		subrgvr1.x	|- X = ( var1 ` R )
2		subrgvr1.r	|- ( ph -> T e. ( SubRing ` R ) )
3		subrgvr1.h	|- H = ( R |`s T )
4		subrgvr1cl.u	|- U = ( Poly1 ` H )
5		subrgvr1cl.b	|- B = ( Base ` U )
6	1	vr1val	|- X = ( ( 1o mVar R ) ` (/) )
7		eqid	|- ( 1o mVar R ) = ( 1o mVar R )
8		1on	|- 1o e. On
9	8	a1i	|- ( ph -> 1o e. On )
10		eqid	|- ( 1o mPoly H ) = ( 1o mPoly H )
11		eqid	|- ( PwSer1 ` H ) = ( PwSer1 ` H )
12	4 11 5	ply1bas	|- B = ( Base ` ( 1o mPoly H ) )
13	7 9 2 3 10 12	subrgmvrf	|- ( ph -> ( 1o mVar R ) : 1o --> B )
14		0lt1o	|- (/) e. 1o
15		ffvelrn	|- ( ( ( 1o mVar R ) : 1o --> B /\ (/) e. 1o ) -> ( ( 1o mVar R ) ` (/) ) e. B )
16	13 14 15	sylancl	|- ( ph -> ( ( 1o mVar R ) ` (/) ) e. B )
17	6 16	eqeltrid	|- ( ph -> X e. B )