Metamath Proof Explorer

Theorem asclghm

Description: The algebra scalar lifting function is a group homomorphism. (Contributed by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses asclf.a 
|- A = ( algSc ` W )
asclf.f 
|- F = ( Scalar ` W )
asclf.r 
|- ( ph -> W e. Ring )
asclf.l 
|- ( ph -> W e. LMod )
Assertion asclghm 
|- ( ph -> A e. ( F GrpHom W ) )

Proof

Step Hyp Ref Expression
1 asclf.a 
 |-  A = ( algSc ` W )
2 asclf.f 
 |-  F = ( Scalar ` W )
3 asclf.r 
 |-  ( ph -> W e. Ring )
4 asclf.l 
 |-  ( ph -> W e. LMod )
5 eqid 
 |-  ( Base ` F ) = ( Base ` F )
6 eqid 
 |-  ( Base ` W ) = ( Base ` W )
7 eqid 
 |-  ( +g ` F ) = ( +g ` F )
8 eqid 
 |-  ( +g ` W ) = ( +g ` W )
9 2 lmodring 
 |-  ( W e. LMod -> F e. Ring )
10 4 9 syl 
 |-  ( ph -> F e. Ring )
11 ringgrp 
 |-  ( F e. Ring -> F e. Grp )
12 10 11 syl 
 |-  ( ph -> F e. Grp )
13 ringgrp 
 |-  ( W e. Ring -> W e. Grp )
14 3 13 syl 
 |-  ( ph -> W e. Grp )
15 1 2 3 4 5 6 asclf 
 |-  ( ph -> A : ( Base ` F ) --> ( Base ` W ) )
16 4 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` F ) /\ y e. ( Base ` F ) ) ) -> W e. LMod )
17 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` F ) /\ y e. ( Base ` F ) ) ) -> x e. ( Base ` F ) )
18 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` F ) /\ y e. ( Base ` F ) ) ) -> y e. ( Base ` F ) )
19 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
20 6 19 ringidcl 
 |-  ( W e. Ring -> ( 1r ` W ) e. ( Base ` W ) )
21 3 20 syl 
 |-  ( ph -> ( 1r ` W ) e. ( Base ` W ) )
22 21 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` F ) /\ y e. ( Base ` F ) ) ) -> ( 1r ` W ) e. ( Base ` W ) )
23 eqid 
 |-  ( .s ` W ) = ( .s ` W )
24 6 8 2 23 5 7 lmodvsdir 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` F ) /\ y e. ( Base ` F ) /\ ( 1r ` W ) e. ( Base ` W ) ) ) -> ( ( x ( +g ` F ) y ) ( .s ` W ) ( 1r ` W ) ) = ( ( x ( .s ` W ) ( 1r ` W ) ) ( +g ` W ) ( y ( .s ` W ) ( 1r ` W ) ) ) )
25 16 17 18 22 24 syl13anc 
 |-  ( ( ph /\ ( x e. ( Base ` F ) /\ y e. ( Base ` F ) ) ) -> ( ( x ( +g ` F ) y ) ( .s ` W ) ( 1r ` W ) ) = ( ( x ( .s ` W ) ( 1r ` W ) ) ( +g ` W ) ( y ( .s ` W ) ( 1r ` W ) ) ) )
26 5 7 grpcl 
 |-  ( ( F e. Grp /\ x e. ( Base ` F ) /\ y e. ( Base ` F ) ) -> ( x ( +g ` F ) y ) e. ( Base ` F ) )
27 26 3expb 
 |-  ( ( F e. Grp /\ ( x e. ( Base ` F ) /\ y e. ( Base ` F ) ) ) -> ( x ( +g ` F ) y ) e. ( Base ` F ) )
28 12 27 sylan 
 |-  ( ( ph /\ ( x e. ( Base ` F ) /\ y e. ( Base ` F ) ) ) -> ( x ( +g ` F ) y ) e. ( Base ` F ) )
29 1 2 5 23 19 asclval 
 |-  ( ( x ( +g ` F ) y ) e. ( Base ` F ) -> ( A ` ( x ( +g ` F ) y ) ) = ( ( x ( +g ` F ) y ) ( .s ` W ) ( 1r ` W ) ) )
30 28 29 syl 
 |-  ( ( ph /\ ( x e. ( Base ` F ) /\ y e. ( Base ` F ) ) ) -> ( A ` ( x ( +g ` F ) y ) ) = ( ( x ( +g ` F ) y ) ( .s ` W ) ( 1r ` W ) ) )
31 1 2 5 23 19 asclval 
 |-  ( x e. ( Base ` F ) -> ( A ` x ) = ( x ( .s ` W ) ( 1r ` W ) ) )
32 1 2 5 23 19 asclval 
 |-  ( y e. ( Base ` F ) -> ( A ` y ) = ( y ( .s ` W ) ( 1r ` W ) ) )
33 31 32 oveqan12d 
 |-  ( ( x e. ( Base ` F ) /\ y e. ( Base ` F ) ) -> ( ( A ` x ) ( +g ` W ) ( A ` y ) ) = ( ( x ( .s ` W ) ( 1r ` W ) ) ( +g ` W ) ( y ( .s ` W ) ( 1r ` W ) ) ) )
34 33 adantl 
 |-  ( ( ph /\ ( x e. ( Base ` F ) /\ y e. ( Base ` F ) ) ) -> ( ( A ` x ) ( +g ` W ) ( A ` y ) ) = ( ( x ( .s ` W ) ( 1r ` W ) ) ( +g ` W ) ( y ( .s ` W ) ( 1r ` W ) ) ) )
35 25 30 34 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` F ) /\ y e. ( Base ` F ) ) ) -> ( A ` ( x ( +g ` F ) y ) ) = ( ( A ` x ) ( +g ` W ) ( A ` y ) ) )
36 5 6 7 8 12 14 15 35 isghmd 
 |-  ( ph -> A e. ( F GrpHom W ) )