Theorem 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	⊢ 𝑁 = ( 𝑀 /s ( 𝑀 ~QG 𝐺 ) )
	quslmod.v	⊢ 𝑉 = ( Base ‘ 𝑀 )
	quslmod.1	⊢ ( 𝜑 → 𝑀 ∈ LMod )
	quslmod.2	⊢ ( 𝜑 → 𝐺 ∈ ( LSubSp ‘ 𝑀 ) )
Assertion	quslmod	⊢ ( 𝜑 → 𝑁 ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		quslmod.n	⊢ 𝑁 = ( 𝑀 /s ( 𝑀 ~QG 𝐺 ) )
2		quslmod.v	⊢ 𝑉 = ( Base ‘ 𝑀 )
3		quslmod.1	⊢ ( 𝜑 → 𝑀 ∈ LMod )
4		quslmod.2	⊢ ( 𝜑 → 𝐺 ∈ ( LSubSp ‘ 𝑀 ) )
5	1	a1i	⊢ ( 𝜑 → 𝑁 = ( 𝑀 /s ( 𝑀 ~QG 𝐺 ) ) )
6	2	a1i	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑀 ) )
7		eqid	⊢ ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) )
8		ovexd	⊢ ( 𝜑 → ( 𝑀 ~QG 𝐺 ) ∈ V )
9	5 6 7 8 3	qusval	⊢ ( 𝜑 → 𝑁 = ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) “s 𝑀 ) )
10		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
11		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
12		eqid	⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
13		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
14	5 6 7 8 3	quslem	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) : 𝑉 –onto→ ( 𝑉 / ( 𝑀 ~QG 𝐺 ) ) )
15		eqid	⊢ ( LSubSp ‘ 𝑀 ) = ( LSubSp ‘ 𝑀 )
16	15	lsssubg	⊢ ( ( 𝑀 ∈ LMod ∧ 𝐺 ∈ ( LSubSp ‘ 𝑀 ) ) → 𝐺 ∈ ( SubGrp ‘ 𝑀 ) )
17	3 4 16	syl2anc	⊢ ( 𝜑 → 𝐺 ∈ ( SubGrp ‘ 𝑀 ) )
18		eqid	⊢ ( 𝑀 ~QG 𝐺 ) = ( 𝑀 ~QG 𝐺 )
19	2 18	eqger	⊢ ( 𝐺 ∈ ( SubGrp ‘ 𝑀 ) → ( 𝑀 ~QG 𝐺 ) Er 𝑉 )
20	17 19	syl	⊢ ( 𝜑 → ( 𝑀 ~QG 𝐺 ) Er 𝑉 )
21	2	fvexi	⊢ 𝑉 ∈ V
22	21	a1i	⊢ ( 𝜑 → 𝑉 ∈ V )
23		lmodgrp	⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Grp )
24	3 23	syl	⊢ ( 𝜑 → 𝑀 ∈ Grp )
25	24	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → 𝑀 ∈ Grp )
26		simprl	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → 𝑝 ∈ 𝑉 )
27		simprr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → 𝑞 ∈ 𝑉 )
28	2 11	grpcl	⊢ ( ( 𝑀 ∈ Grp ∧ 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) → ( 𝑝 ( +g ‘ 𝑀 ) 𝑞 ) ∈ 𝑉 )
29	25 26 27 28	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 ( +g ‘ 𝑀 ) 𝑞 ) ∈ 𝑉 )
30		lmodabl	⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Abel )
31		ablnsg	⊢ ( 𝑀 ∈ Abel → ( NrmSGrp ‘ 𝑀 ) = ( SubGrp ‘ 𝑀 ) )
32	3 30 31	3syl	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝑀 ) = ( SubGrp ‘ 𝑀 ) )
33	17 32	eleqtrrd	⊢ ( 𝜑 → 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) )
34	2 18 11	eqgcpbl	⊢ ( 𝐺 ∈ ( NrmSGrp ‘ 𝑀 ) → ( ( 𝑎 ( 𝑀 ~QG 𝐺 ) 𝑝 ∧ 𝑏 ( 𝑀 ~QG 𝐺 ) 𝑞 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( 𝑀 ~QG 𝐺 ) ( 𝑝 ( +g ‘ 𝑀 ) 𝑞 ) ) )
35	33 34	syl	⊢ ( 𝜑 → ( ( 𝑎 ( 𝑀 ~QG 𝐺 ) 𝑝 ∧ 𝑏 ( 𝑀 ~QG 𝐺 ) 𝑞 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( 𝑀 ~QG 𝐺 ) ( 𝑝 ( +g ‘ 𝑀 ) 𝑞 ) ) )
36	20 22 7 29 35	ercpbl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑎 ) = ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑝 ) ∧ ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑏 ) = ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑞 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ ( 𝑝 ( +g ‘ 𝑀 ) 𝑞 ) ) ) )
37	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑀 ∈ LMod )
38	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝐺 ∈ ( LSubSp ‘ 𝑀 ) )
39		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
40		eqid	⊢ ( ·𝑠 ‘ 𝑁 ) = ( ·𝑠 ‘ 𝑁 )
41		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑎 ∈ 𝑉 )
42		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑏 ∈ 𝑉 )
43	2 18 10 12 37 38 39 1 40 7 41 42	qusvscpbl	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑎 ) = ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑏 ) → ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ ( 𝑘 ( ·𝑠 ‘ 𝑀 ) 𝑎 ) ) = ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ ( 𝑘 ( ·𝑠 ‘ 𝑀 ) 𝑏 ) ) ) )
44	9 2 10 11 12 13 14 36 43 3	imaslmod	⊢ ( 𝜑 → 𝑁 ∈ LMod )