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 N = M / 𝑠 M ~ QG G
quslmod.v V = Base M
quslmod.1 φ M LMod
quslmod.2 φ G LSubSp M
Assertion quslmod φ N LMod

Proof

Step Hyp Ref Expression
1 quslmod.n N = M / 𝑠 M ~ QG G
2 quslmod.v V = Base M
3 quslmod.1 φ M LMod
4 quslmod.2 φ G LSubSp M
5 1 a1i φ N = M / 𝑠 M ~ QG G
6 2 a1i φ V = Base M
7 eqid x V x M ~ QG G = x V x M ~ QG G
8 ovexd φ M ~ QG G V
9 5 6 7 8 3 qusval φ N = x V x M ~ QG G 𝑠 M
10 eqid Base Scalar M = Base Scalar M
11 eqid + M = + M
12 eqid M = M
13 eqid 0 M = 0 M
14 5 6 7 8 3 quslem φ x V x M ~ QG G : V onto V / M ~ QG G
15 eqid LSubSp M = LSubSp M
16 15 lsssubg M LMod G LSubSp M G SubGrp M
17 3 4 16 syl2anc φ G SubGrp M
18 eqid M ~ QG G = M ~ QG G
19 2 18 eqger G SubGrp M M ~ QG G Er V
20 17 19 syl φ M ~ QG G Er V
21 2 fvexi V V
22 21 a1i φ V V
23 lmodgrp M LMod M Grp
24 3 23 syl φ M Grp
25 24 adantr φ p V q V M Grp
26 simprl φ p V q V p V
27 simprr φ p V q V q V
28 2 11 grpcl M Grp p V q V p + M q V
29 25 26 27 28 syl3anc φ p V q V p + M q V
30 lmodabl M LMod M Abel
31 ablnsg M Abel NrmSGrp M = SubGrp M
32 3 30 31 3syl φ NrmSGrp M = SubGrp M
33 17 32 eleqtrrd φ G NrmSGrp M
34 2 18 11 eqgcpbl G NrmSGrp M a M ~ QG G p b M ~ QG G q a + M b M ~ QG G p + M q
35 33 34 syl φ a M ~ QG G p b M ~ QG G q a + M b M ~ QG G p + M q
36 20 22 7 29 35 ercpbl φ a V b V p V q V x V x M ~ QG G a = x V x M ~ QG G p x V x M ~ QG G b = x V x M ~ QG G q x V x M ~ QG G a + M b = x V x M ~ QG G p + M q
37 3 adantr φ k Base Scalar M a V b V M LMod
38 4 adantr φ k Base Scalar M a V b V G LSubSp M
39 simpr1 φ k Base Scalar M a V b V k Base Scalar M
40 eqid N = N
41 simpr2 φ k Base Scalar M a V b V a V
42 simpr3 φ k Base Scalar M a V b V b V
43 2 18 10 12 37 38 39 1 40 7 41 42 qusvscpbl φ k Base Scalar M a V b V x V x M ~ QG G a = x V x M ~ QG G b x V x M ~ QG G k M a = x V x M ~ QG G k M b
44 9 2 10 11 12 13 14 36 43 3 imaslmod φ N LMod