Metamath Proof Explorer


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 )