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 𝑁 ) )