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

Metamath Proof Explorer

Theorem quslmhm

Proof