Metamath Proof Explorer


Theorem asclrhm

Description: The scalar injection 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 ) )