quslmod

Description: If G is a submodule in M , then N = M / G is a left module, called the quotient module of M by 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)$
Assertion	quslmod	$⊢ φ \to N \in LMod$

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	1	a1i	$⊢ φ \to N = M /_{𝑠} (M ~_{QG} G)$
6	2	a1i	$⊢ φ \to V = {Base}_{M}$
7		eqid	$⊢ (x \in V ⟼ [x] (M ~_{QG} G)) = (x \in V ⟼ [x] (M ~_{QG} G))$
8		ovexd	$⊢ φ \to M ~_{QG} G \in V$
9	5 6 7 8 3	qusval	$⊢ φ \to N = (x \in V ⟼ [x] (M ~_{QG} G)) “_{𝑠} M$
10		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
11		eqid	$⊢ +_{M} = +_{M}$
12		eqid	$⊢ \cdot_{M} = \cdot_{M}$
13		eqid	$⊢ 0_{M} = 0_{M}$
14	5 6 7 8 3	quslem	$⊢ φ \to (x \in V ⟼ [x] (M ~_{QG} G)) : V \underset{onto}{⟶} V / (M ~_{QG} G)$
15		eqid	$⊢ LSubSp (M) = LSubSp (M)$
16	15	lsssubg	$⊢ (M \in LMod \land G \in LSubSp (M)) \to G \in SubGrp (M)$
17	3 4 16	syl2anc	$⊢ φ \to G \in SubGrp (M)$
18		eqid	$⊢ M ~_{QG} G = M ~_{QG} G$
19	2 18	eqger	$⊢ G \in SubGrp (M) \to (M ~_{QG} G) Er V$
20	17 19	syl	$⊢ φ \to (M ~_{QG} G) Er V$
21	2	fvexi	$⊢ V \in V$
22	21	a1i	$⊢ φ \to V \in V$
23		lmodgrp	$⊢ M \in LMod \to M \in Grp$
24	3 23	syl	$⊢ φ \to M \in Grp$
25	24	adantr	$⊢ (φ \land (p \in V \land q \in V)) \to M \in Grp$
26		simprl	$⊢ (φ \land (p \in V \land q \in V)) \to p \in V$
27		simprr	$⊢ (φ \land (p \in V \land q \in V)) \to q \in V$
28	2 11	grpcl	$⊢ (M \in Grp \land p \in V \land q \in V) \to p +_{M} q \in V$
29	25 26 27 28	syl3anc	$⊢ (φ \land (p \in V \land q \in V)) \to p +_{M} q \in V$
30		lmodabl	$⊢ M \in LMod \to M \in Abel$
31		ablnsg	$⊢ M \in Abel \to NrmSGrp (M) = SubGrp (M)$
32	3 30 31	3syl	$⊢ φ \to NrmSGrp (M) = SubGrp (M)$
33	17 32	eleqtrrd	$⊢ φ \to G \in NrmSGrp (M)$
34	2 18 11	eqgcpbl	$⊢ G \in NrmSGrp (M) \to ((a (M ~_{QG} G) p \land b (M ~_{QG} G) q) \to (a +_{M} b) (M ~_{QG} G) (p +_{M} q))$
35	33 34	syl	$⊢ φ \to ((a (M ~_{QG} G) p \land b (M ~_{QG} G) q) \to (a +_{M} b) (M ~_{QG} G) (p +_{M} q))$
36	20 22 7 29 35	ercpbl	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to (((x \in V ⟼ [x] (M ~_{QG} G)) (a) = (x \in V ⟼ [x] (M ~_{QG} G)) (p) \land (x \in V ⟼ [x] (M ~_{QG} G)) (b) = (x \in V ⟼ [x] (M ~_{QG} G)) (q)) \to (x \in V ⟼ [x] (M ~_{QG} G)) (a +_{M} b) = (x \in V ⟼ [x] (M ~_{QG} G)) (p +_{M} q))$
37	3	adantr	$⊢ (φ \land (k \in {Base}_{Scalar (M)} \land a \in V \land b \in V)) \to M \in LMod$
38	4	adantr	$⊢ (φ \land (k \in {Base}_{Scalar (M)} \land a \in V \land b \in V)) \to G \in LSubSp (M)$
39		simpr1	$⊢ (φ \land (k \in {Base}_{Scalar (M)} \land a \in V \land b \in V)) \to k \in {Base}_{Scalar (M)}$
40		eqid	$⊢ \cdot_{N} = \cdot_{N}$
41		simpr2	$⊢ (φ \land (k \in {Base}_{Scalar (M)} \land a \in V \land b \in V)) \to a \in V$
42		simpr3	$⊢ (φ \land (k \in {Base}_{Scalar (M)} \land a \in V \land b \in V)) \to b \in V$
43	2 18 10 12 37 38 39 1 40 7 41 42	qusvscpbl	$⊢ (φ \land (k \in {Base}_{Scalar (M)} \land a \in V \land b \in V)) \to ((x \in V ⟼ [x] (M ~_{QG} G)) (a) = (x \in V ⟼ [x] (M ~_{QG} G)) (b) \to (x \in V ⟼ [x] (M ~_{QG} G)) (k \cdot_{M} a) = (x \in V ⟼ [x] (M ~_{QG} G)) (k \cdot_{M} b))$
44	9 2 10 11 12 13 14 36 43 3	imaslmod	$⊢ φ \to N \in LMod$

Metamath Proof Explorer

Theorem quslmod

Proof