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	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lmodvsghm.k	$⊢ K = {Base}_{F}$
Assertion	lmodvsghm	$⊢ (W \in LMod \land R \in K) \to (x \in V ⟼ R \underset{˙}{\cdot} x) \in (W GrpHom W)$

Proof

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

Metamath Proof Explorer

Theorem lmodvsghm

Proof