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	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	subrgvr1.r	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
	subrgvr1.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
Assertion	subrgvr1	⊢ ( 𝜑 → 𝑋 = ( var1 ‘ 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		subrgvr1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
2		subrgvr1.r	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
3		subrgvr1.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
4		eqid	⊢ ( 1o mVar 𝑅 ) = ( 1o mVar 𝑅 )
5		1on	⊢ 1o ∈ On
6	5	a1i	⊢ ( 𝜑 → 1o ∈ On )
7	4 6 2 3	subrgmvr	⊢ ( 𝜑 → ( 1o mVar 𝑅 ) = ( 1o mVar 𝐻 ) )
8	7	fveq1d	⊢ ( 𝜑 → ( ( 1o mVar 𝑅 ) ‘ ∅ ) = ( ( 1o mVar 𝐻 ) ‘ ∅ ) )
9	1	vr1val	⊢ 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )
10		eqid	⊢ ( var1 ‘ 𝐻 ) = ( var1 ‘ 𝐻 )
11	10	vr1val	⊢ ( var1 ‘ 𝐻 ) = ( ( 1o mVar 𝐻 ) ‘ ∅ )
12	8 9 11	3eqtr4g	⊢ ( 𝜑 → 𝑋 = ( var1 ‘ 𝐻 ) )