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 · ˙ = W
lmodvsghm.k K = Base F
Assertion lmodvsghm W LMod R K x V R · ˙ x W GrpHom W

Proof

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