This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem quslmhm

Description: If G is a submodule of M , then the "natural map" from elements to their cosets is a left module homomorphism from M to M / 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 ) )
quslmhm.f 
|- F = ( x e. V |-> [ x ] ( M ~QG G ) )
Assertion quslmhm 
|- ( ph -> F e. ( M LMHom N ) )

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 quslmhm.f 
 |-  F = ( x e. V |-> [ x ] ( M ~QG G ) )
6 eqid 
 |-  ( .s ` M ) = ( .s ` M )
7 eqid 
 |-  ( .s ` N ) = ( .s ` N )
8 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
9 eqid 
 |-  ( Scalar ` N ) = ( Scalar ` N )
10 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
11 1 2 3 4 quslmod 
 |-  ( ph -> N e. LMod )
12 1 a1i 
 |-  ( ph -> N = ( M /s ( M ~QG G ) ) )
13 2 a1i 
 |-  ( ph -> V = ( Base ` M ) )
14 ovexd 
 |-  ( ph -> ( M ~QG G ) e. _V )
15 12 13 14 3 8 quss 
 |-  ( ph -> ( Scalar ` M ) = ( Scalar ` N ) )
16 15 eqcomd 
 |-  ( ph -> ( Scalar ` N ) = ( Scalar ` M ) )
17 eqid 
 |-  ( LSubSp ` M ) = ( LSubSp ` M )
18 17 lsssubg 
 |-  ( ( M e. LMod /\ G e. ( LSubSp ` M ) ) -> G e. ( SubGrp ` M ) )
19 3 4 18 syl2anc 
 |-  ( ph -> G e. ( SubGrp ` M ) )
20 lmodabl 
 |-  ( M e. LMod -> M e. Abel )
21 ablnsg 
 |-  ( M e. Abel -> ( NrmSGrp ` M ) = ( SubGrp ` M ) )
22 3 20 21 3syl 
 |-  ( ph -> ( NrmSGrp ` M ) = ( SubGrp ` M ) )
23 19 22 eleqtrrd 
 |-  ( ph -> G e. ( NrmSGrp ` M ) )
24 2 1 5 qusghm 
 |-  ( G e. ( NrmSGrp ` M ) -> F e. ( M GrpHom N ) )
25 23 24 syl 
 |-  ( ph -> F e. ( M GrpHom N ) )
26 12 13 5 14 3 qusval 
 |-  ( ph -> N = ( F "s M ) )
27 12 13 5 14 3 quslem 
 |-  ( ph -> F : V -onto-> ( V /. ( M ~QG G ) ) )
28 eqid 
 |-  ( M ~QG G ) = ( M ~QG G )
29 3 adantr 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` M ) ) /\ u e. V /\ v e. V ) ) -> M e. LMod )
30 4 adantr 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` M ) ) /\ u e. V /\ v e. V ) ) -> G e. ( LSubSp ` M ) )
31 simpr1 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` M ) ) /\ u e. V /\ v e. V ) ) -> k e. ( Base ` ( Scalar ` M ) ) )
32 simpr2 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` M ) ) /\ u e. V /\ v e. V ) ) -> u e. V )
33 simpr3 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` M ) ) /\ u e. V /\ v e. V ) ) -> v e. V )
34 2 28 10 6 29 30 31 1 7 5 32 33 qusvscpbl 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` M ) ) /\ u e. V /\ v e. V ) ) -> ( ( F ` u ) = ( F ` v ) -> ( F ` ( k ( .s ` M ) u ) ) = ( F ` ( k ( .s ` M ) v ) ) ) )
35 26 13 27 3 8 10 6 7 34 imasvscaval 
 |-  ( ( ph /\ y e. ( Base ` ( Scalar ` M ) ) /\ z e. V ) -> ( y ( .s ` N ) ( F ` z ) ) = ( F ` ( y ( .s ` M ) z ) ) )
36 35 3expb 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` M ) ) /\ z e. V ) ) -> ( y ( .s ` N ) ( F ` z ) ) = ( F ` ( y ( .s ` M ) z ) ) )
37 36 eqcomd 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` M ) ) /\ z e. V ) ) -> ( F ` ( y ( .s ` M ) z ) ) = ( y ( .s ` N ) ( F ` z ) ) )
38 2 6 7 8 9 10 3 11 16 25 37 islmhmd 
 |-  ( ph -> F e. ( M LMHom N ) )