Theorem subrgvr1

Description: The variables in a subring polynomial algebra are the same as the original ring. (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 )
Assertion	subrgvr1	|- ( ph -> X = ( var1 ` H ) )

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		eqid	|- ( 1o mVar R ) = ( 1o mVar R )
5		1on	|- 1o e. On
6	5	a1i	|- ( ph -> 1o e. On )
7	4 6 2 3	subrgmvr	|- ( ph -> ( 1o mVar R ) = ( 1o mVar H ) )
8	7	fveq1d	|- ( ph -> ( ( 1o mVar R ) ` (/) ) = ( ( 1o mVar H ) ` (/) ) )
9	1	vr1val	|- X = ( ( 1o mVar R ) ` (/) )
10		eqid	|- ( var1 ` H ) = ( var1 ` H )
11	10	vr1val	|- ( var1 ` H ) = ( ( 1o mVar H ) ` (/) )
12	8 9 11	3eqtr4g	|- ( ph -> X = ( var1 ` H ) )