This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 lmodvsghm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lmodvsghm.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 lmodvsghm.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 lmodvsghm.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
6 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
7 6 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ) → 𝑊 ∈ Grp )
8 1 2 3 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑅 · 𝑥 ) ∈ 𝑉 )
9 8 3expa ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑅 · 𝑥 ) ∈ 𝑉 )
10 9 fmpttd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑅 · 𝑥 ) ) : 𝑉 ⟶ 𝑉 )
11 1 5 2 3 4 lmodvsdi ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑅 · ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) = ( ( 𝑅 · 𝑦 ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑧 ) ) )
12 11 3exp2 ⊢ ( 𝑊 ∈ LMod → ( 𝑅 ∈ 𝐾 → ( 𝑦 ∈ 𝑉 → ( 𝑧 ∈ 𝑉 → ( 𝑅 · ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) = ( ( 𝑅 · 𝑦 ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑧 ) ) ) ) ) )
13 12 imp43 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑅 · ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) = ( ( 𝑅 · 𝑦 ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑧 ) ) )
14 1 5 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
15 14 3expb ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
16 15 adantlr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
17 oveq2 ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → ( 𝑅 · 𝑥 ) = ( 𝑅 · ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) )
18 eqid ⊢ ( 𝑥 ∈ 𝑉 ↦ ( 𝑅 · 𝑥 ) ) = ( 𝑥 ∈ 𝑉 ↦ ( 𝑅 · 𝑥 ) )
19 ovex ⊢ ( 𝑅 · ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∈ V
20 17 18 19 fvmpt ⊢ ( ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑅 · 𝑥 ) ) ‘ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) = ( 𝑅 · ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) )
21 16 20 syl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑅 · 𝑥 ) ) ‘ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) = ( 𝑅 · ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) )
22 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑅 · 𝑥 ) = ( 𝑅 · 𝑦 ) )
23 ovex ⊢ ( 𝑅 · 𝑦 ) ∈ V
24 22 18 23 fvmpt ⊢ ( 𝑦 ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑅 · 𝑥 ) ) ‘ 𝑦 ) = ( 𝑅 · 𝑦 ) )
25 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑅 · 𝑥 ) = ( 𝑅 · 𝑧 ) )
26 ovex ⊢ ( 𝑅 · 𝑧 ) ∈ V
27 25 18 26 fvmpt ⊢ ( 𝑧 ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑅 · 𝑥 ) ) ‘ 𝑧 ) = ( 𝑅 · 𝑧 ) )
28 24 27 oveqan12d ⊢ ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑅 · 𝑥 ) ) ‘ 𝑦 ) ( +g ‘ 𝑊 ) ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑅 · 𝑥 ) ) ‘ 𝑧 ) ) = ( ( 𝑅 · 𝑦 ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑧 ) ) )
29 28 adantl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑅 · 𝑥 ) ) ‘ 𝑦 ) ( +g ‘ 𝑊 ) ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑅 · 𝑥 ) ) ‘ 𝑧 ) ) = ( ( 𝑅 · 𝑦 ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑧 ) ) )
30 13 21 29 3eqtr4d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑅 · 𝑥 ) ) ‘ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) = ( ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑅 · 𝑥 ) ) ‘ 𝑦 ) ( +g ‘ 𝑊 ) ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑅 · 𝑥 ) ) ‘ 𝑧 ) ) )
31 1 1 5 5 7 7 10 30 isghmd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑅 · 𝑥 ) ) ∈ ( 𝑊 GrpHom 𝑊 ) )