Metamath Proof Explorer

Theorem lmodvslmhm

Description: Scalar multiplication in a left module by a fixed element is a group homomorphism. (Contributed by Thierry Arnoux, 12-Jun-2023)

Ref Expression
Hypotheses lmodvslmhm.v 
|- V = ( Base ` W )
lmodvslmhm.f 
|- F = ( Scalar ` W )
lmodvslmhm.s 
|- .x. = ( .s ` W )
lmodvslmhm.k 
|- K = ( Base ` F )
Assertion lmodvslmhm 
|- ( ( W e. LMod /\ Y e. V ) -> ( x e. K |-> ( x .x. Y ) ) e. ( F GrpHom W ) )

Proof

Step Hyp Ref Expression
1 lmodvslmhm.v 
 |-  V = ( Base ` W )
2 lmodvslmhm.f 
 |-  F = ( Scalar ` W )
3 lmodvslmhm.s 
 |-  .x. = ( .s ` W )
4 lmodvslmhm.k 
 |-  K = ( Base ` F )
5 eqid 
 |-  ( +g ` F ) = ( +g ` F )
6 eqid 
 |-  ( +g ` W ) = ( +g ` W )
7 2 lmodfgrp 
 |-  ( W e. LMod -> F e. Grp )
8 7 adantr 
 |-  ( ( W e. LMod /\ Y e. V ) -> F e. Grp )
9 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
10 9 adantr 
 |-  ( ( W e. LMod /\ Y e. V ) -> W e. Grp )
11 1 2 3 4 lmodvscl 
 |-  ( ( W e. LMod /\ x e. K /\ Y e. V ) -> ( x .x. Y ) e. V )
12 11 3expa 
 |-  ( ( ( W e. LMod /\ x e. K ) /\ Y e. V ) -> ( x .x. Y ) e. V )
13 12 an32s 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ x e. K ) -> ( x .x. Y ) e. V )
14 eqid 
 |-  ( x e. K |-> ( x .x. Y ) ) = ( x e. K |-> ( x .x. Y ) )
15 13 14 fmptd 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( x e. K |-> ( x .x. Y ) ) : K --> V )
16 simpll 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) -> W e. LMod )
17 simprl 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) -> i e. K )
18 simprr 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) -> j e. K )
19 simplr 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) -> Y e. V )
20 1 6 2 3 4 5 lmodvsdir 
 |-  ( ( W e. LMod /\ ( i e. K /\ j e. K /\ Y e. V ) ) -> ( ( i ( +g ` F ) j ) .x. Y ) = ( ( i .x. Y ) ( +g ` W ) ( j .x. Y ) ) )
21 16 17 18 19 20 syl13anc 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) -> ( ( i ( +g ` F ) j ) .x. Y ) = ( ( i .x. Y ) ( +g ` W ) ( j .x. Y ) ) )
22 14 a1i 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) -> ( x e. K |-> ( x .x. Y ) ) = ( x e. K |-> ( x .x. Y ) ) )
23 simpr 
 |-  ( ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) /\ x = ( i ( +g ` F ) j ) ) -> x = ( i ( +g ` F ) j ) )
24 23 oveq1d 
 |-  ( ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) /\ x = ( i ( +g ` F ) j ) ) -> ( x .x. Y ) = ( ( i ( +g ` F ) j ) .x. Y ) )
25 2 4 5 lmodacl 
 |-  ( ( W e. LMod /\ i e. K /\ j e. K ) -> ( i ( +g ` F ) j ) e. K )
26 25 3expb 
 |-  ( ( W e. LMod /\ ( i e. K /\ j e. K ) ) -> ( i ( +g ` F ) j ) e. K )
27 26 adantlr 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) -> ( i ( +g ` F ) j ) e. K )
28 ovexd 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) -> ( ( i ( +g ` F ) j ) .x. Y ) e. _V )
29 22 24 27 28 fvmptd 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) -> ( ( x e. K |-> ( x .x. Y ) ) ` ( i ( +g ` F ) j ) ) = ( ( i ( +g ` F ) j ) .x. Y ) )
30 simpr 
 |-  ( ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) /\ x = i ) -> x = i )
31 30 oveq1d 
 |-  ( ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) /\ x = i ) -> ( x .x. Y ) = ( i .x. Y ) )
32 ovexd 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) -> ( i .x. Y ) e. _V )
33 22 31 17 32 fvmptd 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) -> ( ( x e. K |-> ( x .x. Y ) ) ` i ) = ( i .x. Y ) )
34 simpr 
 |-  ( ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) /\ x = j ) -> x = j )
35 34 oveq1d 
 |-  ( ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) /\ x = j ) -> ( x .x. Y ) = ( j .x. Y ) )
36 ovexd 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) -> ( j .x. Y ) e. _V )
37 22 35 18 36 fvmptd 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) -> ( ( x e. K |-> ( x .x. Y ) ) ` j ) = ( j .x. Y ) )
38 33 37 oveq12d 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) -> ( ( ( x e. K |-> ( x .x. Y ) ) ` i ) ( +g ` W ) ( ( x e. K |-> ( x .x. Y ) ) ` j ) ) = ( ( i .x. Y ) ( +g ` W ) ( j .x. Y ) ) )
39 21 29 38 3eqtr4d 
 |-  ( ( ( W e. LMod /\ Y e. V ) /\ ( i e. K /\ j e. K ) ) -> ( ( x e. K |-> ( x .x. Y ) ) ` ( i ( +g ` F ) j ) ) = ( ( ( x e. K |-> ( x .x. Y ) ) ` i ) ( +g ` W ) ( ( x e. K |-> ( x .x. Y ) ) ` j ) ) )
40 4 1 5 6 8 10 15 39 isghmd 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( x e. K |-> ( x .x. Y ) ) e. ( F GrpHom W ) )