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 ⊢ · ˙ = ⋅ W
lmodvslmhm.k ⊢ K = Base F
Assertion lmodvslmhm ⊢ W ∈ LMod ∧ Y ∈ V → x ∈ K ⟼ x · ˙ Y ∈ F GrpHom W

Proof

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