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

Metamath Proof Explorer

Theorem quslmhm

Proof