quslmhm

Description: If G is a submodule of M , then the "natural map" from elements to their cosets is a left module homomorphism from M to M / G . (Contributed by Thierry Arnoux, 18-May-2023)

	Ref	Expression
Hypotheses	quslmod.n	$⊢ N = M /_{𝑠} (M ~_{QG} G)$
	quslmod.v	$⊢ V = {Base}_{M}$
	quslmod.1	$⊢ φ \to M \in LMod$
	quslmod.2	$⊢ φ \to G \in LSubSp (M)$
	quslmhm.f	$⊢ F = (x \in V ⟼ [x] (M ~_{QG} G))$
Assertion	quslmhm	$⊢ φ \to F \in (M LMHom N)$

Proof

Step	Hyp	Ref	Expression
1		quslmod.n	$⊢ N = M /_{𝑠} (M ~_{QG} G)$
2		quslmod.v	$⊢ V = {Base}_{M}$
3		quslmod.1	$⊢ φ \to M \in LMod$
4		quslmod.2	$⊢ φ \to G \in LSubSp (M)$
5		quslmhm.f	$⊢ F = (x \in V ⟼ [x] (M ~_{QG} G))$
6		eqid	$⊢ \cdot_{M} = \cdot_{M}$
7		eqid	$⊢ \cdot_{N} = \cdot_{N}$
8		eqid	$⊢ Scalar (M) = Scalar (M)$
9		eqid	$⊢ Scalar (N) = Scalar (N)$
10		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
11	1 2 3 4	quslmod	$⊢ φ \to N \in LMod$
12	1	a1i	$⊢ φ \to N = M /_{𝑠} (M ~_{QG} G)$
13	2	a1i	$⊢ φ \to V = {Base}_{M}$
14		ovexd	$⊢ φ \to M ~_{QG} G \in V$
15	12 13 14 3 8	quss	$⊢ φ \to Scalar (M) = Scalar (N)$
16	15	eqcomd	$⊢ φ \to Scalar (N) = Scalar (M)$
17		eqid	$⊢ LSubSp (M) = LSubSp (M)$
18	17	lsssubg	$⊢ (M \in LMod \land G \in LSubSp (M)) \to G \in SubGrp (M)$
19	3 4 18	syl2anc	$⊢ φ \to G \in SubGrp (M)$
20		lmodabl	$⊢ M \in LMod \to M \in Abel$
21		ablnsg	$⊢ M \in Abel \to NrmSGrp (M) = SubGrp (M)$
22	3 20 21	3syl	$⊢ φ \to NrmSGrp (M) = SubGrp (M)$
23	19 22	eleqtrrd	$⊢ φ \to G \in NrmSGrp (M)$
24	2 1 5	qusghm	$⊢ G \in NrmSGrp (M) \to F \in (M GrpHom N)$
25	23 24	syl	$⊢ φ \to F \in (M GrpHom N)$
26	12 13 5 14 3	qusval	$⊢ φ \to N = F “_{𝑠} M$
27	12 13 5 14 3	quslem	$⊢ φ \to F : V \underset{onto}{⟶} V / (M ~_{QG} G)$
28		eqid	$⊢ M ~_{QG} G = M ~_{QG} G$
29	3	adantr	$⊢ (φ \land (k \in {Base}_{Scalar (M)} \land u \in V \land v \in V)) \to M \in LMod$
30	4	adantr	$⊢ (φ \land (k \in {Base}_{Scalar (M)} \land u \in V \land v \in V)) \to G \in LSubSp (M)$
31		simpr1	$⊢ (φ \land (k \in {Base}_{Scalar (M)} \land u \in V \land v \in V)) \to k \in {Base}_{Scalar (M)}$
32		simpr2	$⊢ (φ \land (k \in {Base}_{Scalar (M)} \land u \in V \land v \in V)) \to u \in V$
33		simpr3	$⊢ (φ \land (k \in {Base}_{Scalar (M)} \land u \in V \land v \in V)) \to v \in V$
34	2 28 10 6 29 30 31 1 7 5 32 33	qusvscpbl	$⊢ (φ \land (k \in {Base}_{Scalar (M)} \land u \in V \land v \in V)) \to (F (u) = F (v) \to F (k \cdot_{M} u) = F (k \cdot_{M} v))$
35	26 13 27 3 8 10 6 7 34	imasvscaval	$⊢ (φ \land y \in {Base}_{Scalar (M)} \land z \in V) \to y \cdot_{N} F (z) = F (y \cdot_{M} z)$
36	35	3expb	$⊢ (φ \land (y \in {Base}_{Scalar (M)} \land z \in V)) \to y \cdot_{N} F (z) = F (y \cdot_{M} z)$
37	36	eqcomd	$⊢ (φ \land (y \in {Base}_{Scalar (M)} \land z \in V)) \to F (y \cdot_{M} z) = y \cdot_{N} F (z)$
38	2 6 7 8 9 10 3 11 16 25 37	islmhmd	$⊢ φ \to F \in (M LMHom N)$

Metamath Proof Explorer

Theorem quslmhm

Proof