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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
lmodvslmhm.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lmodvslmhm.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
lmodvslmhm.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion lmodvslmhm ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) ∈ ( 𝐹 GrpHom 𝑊 ) )

Proof

Step Hyp Ref Expression
1 lmodvslmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lmodvslmhm.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 lmodvslmhm.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 lmodvslmhm.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 eqid ⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
6 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
7 2 lmodfgrp ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Grp )
8 7 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → 𝐹 ∈ Grp )
9 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
10 9 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → 𝑊 ∈ Grp )
11 1 2 3 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑥 · 𝑌 ) ∈ 𝑉 )
12 11 3expa ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ 𝐾 ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑥 · 𝑌 ) ∈ 𝑉 )
13 12 an32s ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝑥 · 𝑌 ) ∈ 𝑉 )
14 eqid ⊢ ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) )
15 13 14 fmptd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) : 𝐾 ⟶ 𝑉 )
16 simpll ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → 𝑊 ∈ LMod )
17 simprl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → 𝑖 ∈ 𝐾 )
18 simprr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → 𝑗 ∈ 𝐾 )
19 simplr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → 𝑌 ∈ 𝑉 )
20 1 6 2 3 4 5 lmodvsdir ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑖 ( +g ‘ 𝐹 ) 𝑗 ) · 𝑌 ) = ( ( 𝑖 · 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑗 · 𝑌 ) ) )
21 16 17 18 19 20 syl13anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → ( ( 𝑖 ( +g ‘ 𝐹 ) 𝑗 ) · 𝑌 ) = ( ( 𝑖 · 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑗 · 𝑌 ) ) )
22 14 a1i ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) )
23 simpr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) ∧ 𝑥 = ( 𝑖 ( +g ‘ 𝐹 ) 𝑗 ) ) → 𝑥 = ( 𝑖 ( +g ‘ 𝐹 ) 𝑗 ) )
24 23 oveq1d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) ∧ 𝑥 = ( 𝑖 ( +g ‘ 𝐹 ) 𝑗 ) ) → ( 𝑥 · 𝑌 ) = ( ( 𝑖 ( +g ‘ 𝐹 ) 𝑗 ) · 𝑌 ) )
25 2 4 5 lmodacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) → ( 𝑖 ( +g ‘ 𝐹 ) 𝑗 ) ∈ 𝐾 )
26 25 3expb ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → ( 𝑖 ( +g ‘ 𝐹 ) 𝑗 ) ∈ 𝐾 )
27 26 adantlr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → ( 𝑖 ( +g ‘ 𝐹 ) 𝑗 ) ∈ 𝐾 )
28 ovexd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → ( ( 𝑖 ( +g ‘ 𝐹 ) 𝑗 ) · 𝑌 ) ∈ V )
29 22 24 27 28 fvmptd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → ( ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) ‘ ( 𝑖 ( +g ‘ 𝐹 ) 𝑗 ) ) = ( ( 𝑖 ( +g ‘ 𝐹 ) 𝑗 ) · 𝑌 ) )
30 simpr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) ∧ 𝑥 = 𝑖 ) → 𝑥 = 𝑖 )
31 30 oveq1d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) ∧ 𝑥 = 𝑖 ) → ( 𝑥 · 𝑌 ) = ( 𝑖 · 𝑌 ) )
32 ovexd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → ( 𝑖 · 𝑌 ) ∈ V )
33 22 31 17 32 fvmptd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → ( ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) ‘ 𝑖 ) = ( 𝑖 · 𝑌 ) )
34 simpr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) ∧ 𝑥 = 𝑗 ) → 𝑥 = 𝑗 )
35 34 oveq1d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) ∧ 𝑥 = 𝑗 ) → ( 𝑥 · 𝑌 ) = ( 𝑗 · 𝑌 ) )
36 ovexd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → ( 𝑗 · 𝑌 ) ∈ V )
37 22 35 18 36 fvmptd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → ( ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) ‘ 𝑗 ) = ( 𝑗 · 𝑌 ) )
38 33 37 oveq12d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → ( ( ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) ‘ 𝑖 ) ( +g ‘ 𝑊 ) ( ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) ‘ 𝑗 ) ) = ( ( 𝑖 · 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑗 · 𝑌 ) ) )
39 21 29 38 3eqtr4d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑖 ∈ 𝐾 ∧ 𝑗 ∈ 𝐾 ) ) → ( ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) ‘ ( 𝑖 ( +g ‘ 𝐹 ) 𝑗 ) ) = ( ( ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) ‘ 𝑖 ) ( +g ‘ 𝑊 ) ( ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) ‘ 𝑗 ) ) )
40 4 1 5 6 8 10 15 39 isghmd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) ∈ ( 𝐹 GrpHom 𝑊 ) )