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

Metamath Proof Explorer

Theorem asclrhm

Description: The algebra scalar lifting function is a ring homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015)

Ref Expression
Hypotheses asclrhm.a 
|- A = ( algSc ` W )
asclrhm.f 
|- F = ( Scalar ` W )
Assertion asclrhm 
|- ( W e. AssAlg -> A e. ( F RingHom W ) )

Proof

Step Hyp Ref Expression
1 asclrhm.a 
 |-  A = ( algSc ` W )
2 asclrhm.f 
 |-  F = ( Scalar ` W )
3 eqid 
 |-  ( Base ` F ) = ( Base ` F )
4 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
5 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
6 eqid 
 |-  ( .r ` F ) = ( .r ` F )
7 eqid 
 |-  ( .r ` W ) = ( .r ` W )
8 2 assasca 
 |-  ( W e. AssAlg -> F e. Ring )
9 assaring 
 |-  ( W e. AssAlg -> W e. Ring )
10 assalmod 
 |-  ( W e. AssAlg -> W e. LMod )
11 1 2 10 9 ascl1 
 |-  ( W e. AssAlg -> ( A ` ( 1r ` F ) ) = ( 1r ` W ) )
12 1 2 3 7 6 ascldimul 
 |-  ( ( W e. AssAlg /\ x e. ( Base ` F ) /\ y e. ( Base ` F ) ) -> ( A ` ( x ( .r ` F ) y ) ) = ( ( A ` x ) ( .r ` W ) ( A ` y ) ) )
13 12 3expb 
 |-  ( ( W e. AssAlg /\ ( x e. ( Base ` F ) /\ y e. ( Base ` F ) ) ) -> ( A ` ( x ( .r ` F ) y ) ) = ( ( A ` x ) ( .r ` W ) ( A ` y ) ) )
14 1 2 9 10 asclghm 
 |-  ( W e. AssAlg -> A e. ( F GrpHom W ) )
15 3 4 5 6 7 8 9 11 13 14 isrhm2d 
 |-  ( W e. AssAlg -> A e. ( F RingHom W ) )