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 โŠข ๐‘ = ( ๐‘€ /s ( ๐‘€ ~QG ๐บ ) )
quslmod.v โŠข ๐‘‰ = ( Base โ€˜ ๐‘€ )
quslmod.1 โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ LMod )
quslmod.2 โŠข ( ๐œ‘ โ†’ ๐บ โˆˆ ( LSubSp โ€˜ ๐‘€ ) )
quslmhm.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐‘‰ โ†ฆ [ ๐‘ฅ ] ( ๐‘€ ~QG ๐บ ) )
Assertion quslmhm ( ๐œ‘ โ†’ ๐น โˆˆ ( ๐‘€ LMHom ๐‘ ) )

Proof

Step Hyp Ref Expression
1 quslmod.n โŠข ๐‘ = ( ๐‘€ /s ( ๐‘€ ~QG ๐บ ) )
2 quslmod.v โŠข ๐‘‰ = ( Base โ€˜ ๐‘€ )
3 quslmod.1 โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ LMod )
4 quslmod.2 โŠข ( ๐œ‘ โ†’ ๐บ โˆˆ ( LSubSp โ€˜ ๐‘€ ) )
5 quslmhm.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐‘‰ โ†ฆ [ ๐‘ฅ ] ( ๐‘€ ~QG ๐บ ) )
6 eqid โŠข ( ยท๐‘  โ€˜ ๐‘€ ) = ( ยท๐‘  โ€˜ ๐‘€ )
7 eqid โŠข ( ยท๐‘  โ€˜ ๐‘ ) = ( ยท๐‘  โ€˜ ๐‘ )
8 eqid โŠข ( Scalar โ€˜ ๐‘€ ) = ( Scalar โ€˜ ๐‘€ )
9 eqid โŠข ( Scalar โ€˜ ๐‘ ) = ( Scalar โ€˜ ๐‘ )
10 eqid โŠข ( Base โ€˜ ( Scalar โ€˜ ๐‘€ ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘€ ) )
11 1 2 3 4 quslmod โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ LMod )
12 1 a1i โŠข ( ๐œ‘ โ†’ ๐‘ = ( ๐‘€ /s ( ๐‘€ ~QG ๐บ ) ) )
13 2 a1i โŠข ( ๐œ‘ โ†’ ๐‘‰ = ( Base โ€˜ ๐‘€ ) )
14 ovexd โŠข ( ๐œ‘ โ†’ ( ๐‘€ ~QG ๐บ ) โˆˆ V )
15 12 13 14 3 8 quss โŠข ( ๐œ‘ โ†’ ( Scalar โ€˜ ๐‘€ ) = ( Scalar โ€˜ ๐‘ ) )
16 15 eqcomd โŠข ( ๐œ‘ โ†’ ( Scalar โ€˜ ๐‘ ) = ( Scalar โ€˜ ๐‘€ ) )
17 eqid โŠข ( LSubSp โ€˜ ๐‘€ ) = ( LSubSp โ€˜ ๐‘€ )
18 17 lsssubg โŠข ( ( ๐‘€ โˆˆ LMod โˆง ๐บ โˆˆ ( LSubSp โ€˜ ๐‘€ ) ) โ†’ ๐บ โˆˆ ( SubGrp โ€˜ ๐‘€ ) )
19 3 4 18 syl2anc โŠข ( ๐œ‘ โ†’ ๐บ โˆˆ ( SubGrp โ€˜ ๐‘€ ) )
20 lmodabl โŠข ( ๐‘€ โˆˆ LMod โ†’ ๐‘€ โˆˆ Abel )
21 ablnsg โŠข ( ๐‘€ โˆˆ Abel โ†’ ( NrmSGrp โ€˜ ๐‘€ ) = ( SubGrp โ€˜ ๐‘€ ) )
22 3 20 21 3syl โŠข ( ๐œ‘ โ†’ ( NrmSGrp โ€˜ ๐‘€ ) = ( SubGrp โ€˜ ๐‘€ ) )
23 19 22 eleqtrrd โŠข ( ๐œ‘ โ†’ ๐บ โˆˆ ( NrmSGrp โ€˜ ๐‘€ ) )
24 2 1 5 qusghm โŠข ( ๐บ โˆˆ ( NrmSGrp โ€˜ ๐‘€ ) โ†’ ๐น โˆˆ ( ๐‘€ GrpHom ๐‘ ) )
25 23 24 syl โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ( ๐‘€ GrpHom ๐‘ ) )
26 12 13 5 14 3 qusval โŠข ( ๐œ‘ โ†’ ๐‘ = ( ๐น โ€œs ๐‘€ ) )
27 12 13 5 14 3 quslem โŠข ( ๐œ‘ โ†’ ๐น : ๐‘‰ โ€“ontoโ†’ ( ๐‘‰ / ( ๐‘€ ~QG ๐บ ) ) )
28 eqid โŠข ( ๐‘€ ~QG ๐บ ) = ( ๐‘€ ~QG ๐บ )
29 3 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘˜ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘€ ) ) โˆง ๐‘ข โˆˆ ๐‘‰ โˆง ๐‘ฃ โˆˆ ๐‘‰ ) ) โ†’ ๐‘€ โˆˆ LMod )
30 4 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘˜ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘€ ) ) โˆง ๐‘ข โˆˆ ๐‘‰ โˆง ๐‘ฃ โˆˆ ๐‘‰ ) ) โ†’ ๐บ โˆˆ ( LSubSp โ€˜ ๐‘€ ) )
31 simpr1 โŠข ( ( ๐œ‘ โˆง ( ๐‘˜ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘€ ) ) โˆง ๐‘ข โˆˆ ๐‘‰ โˆง ๐‘ฃ โˆˆ ๐‘‰ ) ) โ†’ ๐‘˜ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘€ ) ) )
32 simpr2 โŠข ( ( ๐œ‘ โˆง ( ๐‘˜ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘€ ) ) โˆง ๐‘ข โˆˆ ๐‘‰ โˆง ๐‘ฃ โˆˆ ๐‘‰ ) ) โ†’ ๐‘ข โˆˆ ๐‘‰ )
33 simpr3 โŠข ( ( ๐œ‘ โˆง ( ๐‘˜ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘€ ) ) โˆง ๐‘ข โˆˆ ๐‘‰ โˆง ๐‘ฃ โˆˆ ๐‘‰ ) ) โ†’ ๐‘ฃ โˆˆ ๐‘‰ )
34 2 28 10 6 29 30 31 1 7 5 32 33 qusvscpbl โŠข ( ( ๐œ‘ โˆง ( ๐‘˜ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘€ ) ) โˆง ๐‘ข โˆˆ ๐‘‰ โˆง ๐‘ฃ โˆˆ ๐‘‰ ) ) โ†’ ( ( ๐น โ€˜ ๐‘ข ) = ( ๐น โ€˜ ๐‘ฃ ) โ†’ ( ๐น โ€˜ ( ๐‘˜ ( ยท๐‘  โ€˜ ๐‘€ ) ๐‘ข ) ) = ( ๐น โ€˜ ( ๐‘˜ ( ยท๐‘  โ€˜ ๐‘€ ) ๐‘ฃ ) ) ) )
35 26 13 27 3 8 10 6 7 34 imasvscaval โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘€ ) ) โˆง ๐‘ง โˆˆ ๐‘‰ ) โ†’ ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘ ) ( ๐น โ€˜ ๐‘ง ) ) = ( ๐น โ€˜ ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘€ ) ๐‘ง ) ) )
36 35 3expb โŠข ( ( ๐œ‘ โˆง ( ๐‘ฆ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘€ ) ) โˆง ๐‘ง โˆˆ ๐‘‰ ) ) โ†’ ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘ ) ( ๐น โ€˜ ๐‘ง ) ) = ( ๐น โ€˜ ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘€ ) ๐‘ง ) ) )
37 36 eqcomd โŠข ( ( ๐œ‘ โˆง ( ๐‘ฆ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘€ ) ) โˆง ๐‘ง โˆˆ ๐‘‰ ) ) โ†’ ( ๐น โ€˜ ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘€ ) ๐‘ง ) ) = ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘ ) ( ๐น โ€˜ ๐‘ง ) ) )
38 2 6 7 8 9 10 3 11 16 25 37 islmhmd โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ( ๐‘€ LMHom ๐‘ ) )