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

Proof

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

Metamath Proof Explorer

Theorem lmodvslmhm

Proof