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 𝑊 ) )