Metamath Proof Explorer

Theorem subrgmvr

Description: The variables in a subring polynomial algebra are the same as the original ring. (Contributed by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses subrgmvr.v 
|- V = ( I mVar R )
subrgmvr.i 
|- ( ph -> I e. W )
subrgmvr.r 
|- ( ph -> T e. ( SubRing ` R ) )
subrgmvr.h 
|- H = ( R |`s T )
Assertion subrgmvr 
|- ( ph -> V = ( I mVar H ) )

Proof

Step Hyp Ref Expression
1 subrgmvr.v 
 |-  V = ( I mVar R )
2 subrgmvr.i 
 |-  ( ph -> I e. W )
3 subrgmvr.r 
 |-  ( ph -> T e. ( SubRing ` R ) )
4 subrgmvr.h 
 |-  H = ( R |`s T )
5 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
6 4 5 subrg1 
 |-  ( T e. ( SubRing ` R ) -> ( 1r ` R ) = ( 1r ` H ) )
7 3 6 syl 
 |-  ( ph -> ( 1r ` R ) = ( 1r ` H ) )
8 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
9 4 8 subrg0 
 |-  ( T e. ( SubRing ` R ) -> ( 0g ` R ) = ( 0g ` H ) )
10 3 9 syl 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` H ) )
11 7 10 ifeq12d 
 |-  ( ph -> if ( y = ( z e. I |-> if ( z = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( y = ( z e. I |-> if ( z = x , 1 , 0 ) ) , ( 1r ` H ) , ( 0g ` H ) ) )
12 11 mpteq2dv 
 |-  ( ph -> ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = ( z e. I |-> if ( z = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = ( z e. I |-> if ( z = x , 1 , 0 ) ) , ( 1r ` H ) , ( 0g ` H ) ) ) )
13 12 mpteq2dv 
 |-  ( ph -> ( x e. I |-> ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = ( z e. I |-> if ( z = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( x e. I |-> ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = ( z e. I |-> if ( z = x , 1 , 0 ) ) , ( 1r ` H ) , ( 0g ` H ) ) ) ) )
14 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
15 subrgrcl 
 |-  ( T e. ( SubRing ` R ) -> R e. Ring )
16 3 15 syl 
 |-  ( ph -> R e. Ring )
17 1 14 8 5 2 16 mvrfval 
 |-  ( ph -> V = ( x e. I |-> ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = ( z e. I |-> if ( z = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
18 eqid 
 |-  ( I mVar H ) = ( I mVar H )
19 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
20 eqid 
 |-  ( 1r ` H ) = ( 1r ` H )
21 4 ovexi 
 |-  H e. _V
22 21 a1i 
 |-  ( ph -> H e. _V )
23 18 14 19 20 2 22 mvrfval 
 |-  ( ph -> ( I mVar H ) = ( x e. I |-> ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = ( z e. I |-> if ( z = x , 1 , 0 ) ) , ( 1r ` H ) , ( 0g ` H ) ) ) ) )
24 13 17 23 3eqtr4d 
 |-  ( ph -> V = ( I mVar H ) )