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 /s ( M ~QG G ) )
quslmod.v 
|- V = ( Base ` M )
quslmod.1 
|- ( ph -> M e. LMod )
quslmod.2 
|- ( ph -> G e. ( LSubSp ` M ) )
Assertion quslmod 
|- ( ph -> N e. LMod )

Proof

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