This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )