Metamath Proof Explorer

Theorem ressascl

Description: The injection of scalars is invariant between subalgebras and superalgebras. (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Hypotheses ressascl.a 
|- A = ( algSc ` W )
ressascl.x 
|- X = ( W |`s S )
Assertion ressascl 
|- ( S e. ( SubRing ` W ) -> A = ( algSc ` X ) )

Proof

Step Hyp Ref Expression
1 ressascl.a 
 |-  A = ( algSc ` W )
2 ressascl.x 
 |-  X = ( W |`s S )
3 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
4 2 3 resssca 
 |-  ( S e. ( SubRing ` W ) -> ( Scalar ` W ) = ( Scalar ` X ) )
5 4 fveq2d 
 |-  ( S e. ( SubRing ` W ) -> ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` X ) ) )
6 eqid 
 |-  ( .s ` W ) = ( .s ` W )
7 2 6 ressvsca 
 |-  ( S e. ( SubRing ` W ) -> ( .s ` W ) = ( .s ` X ) )
8 eqidd 
 |-  ( S e. ( SubRing ` W ) -> x = x )
9 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
10 2 9 subrg1 
 |-  ( S e. ( SubRing ` W ) -> ( 1r ` W ) = ( 1r ` X ) )
11 7 8 10 oveq123d 
 |-  ( S e. ( SubRing ` W ) -> ( x ( .s ` W ) ( 1r ` W ) ) = ( x ( .s ` X ) ( 1r ` X ) ) )
12 5 11 mpteq12dv 
 |-  ( S e. ( SubRing ` W ) -> ( x e. ( Base ` ( Scalar ` W ) ) |-> ( x ( .s ` W ) ( 1r ` W ) ) ) = ( x e. ( Base ` ( Scalar ` X ) ) |-> ( x ( .s ` X ) ( 1r ` X ) ) ) )
13 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
14 1 3 13 6 9 asclfval 
 |-  A = ( x e. ( Base ` ( Scalar ` W ) ) |-> ( x ( .s ` W ) ( 1r ` W ) ) )
15 eqid 
 |-  ( algSc ` X ) = ( algSc ` X )
16 eqid 
 |-  ( Scalar ` X ) = ( Scalar ` X )
17 eqid 
 |-  ( Base ` ( Scalar ` X ) ) = ( Base ` ( Scalar ` X ) )
18 eqid 
 |-  ( .s ` X ) = ( .s ` X )
19 eqid 
 |-  ( 1r ` X ) = ( 1r ` X )
20 15 16 17 18 19 asclfval 
 |-  ( algSc ` X ) = ( x e. ( Base ` ( Scalar ` X ) ) |-> ( x ( .s ` X ) ( 1r ` X ) ) )
21 12 14 20 3eqtr4g 
 |-  ( S e. ( SubRing ` W ) -> A = ( algSc ` X ) )