Metamath Proof Explorer

Theorem lmodvsghm

Description: Scalar multiplication of the vector space by a fixed scalar is an endomorphism of the additive group of vectors. (Contributed by Mario Carneiro, 5-May-2015)

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

Proof

Step Hyp Ref Expression
1 lmodvsghm.v 
 |-  V = ( Base ` W )
2 lmodvsghm.f 
 |-  F = ( Scalar ` W )
3 lmodvsghm.s 
 |-  .x. = ( .s ` W )
4 lmodvsghm.k 
 |-  K = ( Base ` F )
5 eqid 
 |-  ( +g ` W ) = ( +g ` W )
6 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
7 6 adantr 
 |-  ( ( W e. LMod /\ R e. K ) -> W e. Grp )
8 1 2 3 4 lmodvscl 
 |-  ( ( W e. LMod /\ R e. K /\ x e. V ) -> ( R .x. x ) e. V )
9 8 3expa 
 |-  ( ( ( W e. LMod /\ R e. K ) /\ x e. V ) -> ( R .x. x ) e. V )
10 9 fmpttd 
 |-  ( ( W e. LMod /\ R e. K ) -> ( x e. V |-> ( R .x. x ) ) : V --> V )
11 1 5 2 3 4 lmodvsdi 
 |-  ( ( W e. LMod /\ ( R e. K /\ y e. V /\ z e. V ) ) -> ( R .x. ( y ( +g ` W ) z ) ) = ( ( R .x. y ) ( +g ` W ) ( R .x. z ) ) )
12 11 3exp2 
 |-  ( W e. LMod -> ( R e. K -> ( y e. V -> ( z e. V -> ( R .x. ( y ( +g ` W ) z ) ) = ( ( R .x. y ) ( +g ` W ) ( R .x. z ) ) ) ) ) )
13 12 imp43 
 |-  ( ( ( W e. LMod /\ R e. K ) /\ ( y e. V /\ z e. V ) ) -> ( R .x. ( y ( +g ` W ) z ) ) = ( ( R .x. y ) ( +g ` W ) ( R .x. z ) ) )
14 1 5 lmodvacl 
 |-  ( ( W e. LMod /\ y e. V /\ z e. V ) -> ( y ( +g ` W ) z ) e. V )
15 14 3expb 
 |-  ( ( W e. LMod /\ ( y e. V /\ z e. V ) ) -> ( y ( +g ` W ) z ) e. V )
16 15 adantlr 
 |-  ( ( ( W e. LMod /\ R e. K ) /\ ( y e. V /\ z e. V ) ) -> ( y ( +g ` W ) z ) e. V )
17 oveq2 
 |-  ( x = ( y ( +g ` W ) z ) -> ( R .x. x ) = ( R .x. ( y ( +g ` W ) z ) ) )
18 eqid 
 |-  ( x e. V |-> ( R .x. x ) ) = ( x e. V |-> ( R .x. x ) )
19 ovex 
 |-  ( R .x. ( y ( +g ` W ) z ) ) e. _V
20 17 18 19 fvmpt 
 |-  ( ( y ( +g ` W ) z ) e. V -> ( ( x e. V |-> ( R .x. x ) ) ` ( y ( +g ` W ) z ) ) = ( R .x. ( y ( +g ` W ) z ) ) )
21 16 20 syl 
 |-  ( ( ( W e. LMod /\ R e. K ) /\ ( y e. V /\ z e. V ) ) -> ( ( x e. V |-> ( R .x. x ) ) ` ( y ( +g ` W ) z ) ) = ( R .x. ( y ( +g ` W ) z ) ) )
22 oveq2 
 |-  ( x = y -> ( R .x. x ) = ( R .x. y ) )
23 ovex 
 |-  ( R .x. y ) e. _V
24 22 18 23 fvmpt 
 |-  ( y e. V -> ( ( x e. V |-> ( R .x. x ) ) ` y ) = ( R .x. y ) )
25 oveq2 
 |-  ( x = z -> ( R .x. x ) = ( R .x. z ) )
26 ovex 
 |-  ( R .x. z ) e. _V
27 25 18 26 fvmpt 
 |-  ( z e. V -> ( ( x e. V |-> ( R .x. x ) ) ` z ) = ( R .x. z ) )
28 24 27 oveqan12d 
 |-  ( ( y e. V /\ z e. V ) -> ( ( ( x e. V |-> ( R .x. x ) ) ` y ) ( +g ` W ) ( ( x e. V |-> ( R .x. x ) ) ` z ) ) = ( ( R .x. y ) ( +g ` W ) ( R .x. z ) ) )
29 28 adantl 
 |-  ( ( ( W e. LMod /\ R e. K ) /\ ( y e. V /\ z e. V ) ) -> ( ( ( x e. V |-> ( R .x. x ) ) ` y ) ( +g ` W ) ( ( x e. V |-> ( R .x. x ) ) ` z ) ) = ( ( R .x. y ) ( +g ` W ) ( R .x. z ) ) )
30 13 21 29 3eqtr4d 
 |-  ( ( ( W e. LMod /\ R e. K ) /\ ( y e. V /\ z e. V ) ) -> ( ( x e. V |-> ( R .x. x ) ) ` ( y ( +g ` W ) z ) ) = ( ( ( x e. V |-> ( R .x. x ) ) ` y ) ( +g ` W ) ( ( x e. V |-> ( R .x. x ) ) ` z ) ) )
31 1 1 5 5 7 7 10 30 isghmd 
 |-  ( ( W e. LMod /\ R e. K ) -> ( x e. V |-> ( R .x. x ) ) e. ( W GrpHom W ) )