Theorem qus0g

Description: The identity element of a quotient group. (Contributed by Thierry Arnoux, 13-Mar-2025)

	Ref	Expression
Hypothesis	qus0g.1	|- Q = ( G /s ( G ~QG N ) )
Assertion	qus0g	|- ( N e. ( NrmSGrp ` G ) -> ( 0g ` Q ) = N )

Proof

Step	Hyp	Ref	Expression
1		qus0g.1	|- Q = ( G /s ( G ~QG N ) )
2		eqid	|- ( Base ` G ) = ( Base ` G )
3		eqid	|- ( LSSum ` G ) = ( LSSum ` G )
4		nsgsubg	|- ( N e. ( NrmSGrp ` G ) -> N e. ( SubGrp ` G ) )
5		subgrcl	|- ( N e. ( SubGrp ` G ) -> G e. Grp )
6		eqid	|- ( 0g ` G ) = ( 0g ` G )
7	2 6	grpidcl	|- ( G e. Grp -> ( 0g ` G ) e. ( Base ` G ) )
8	4 5 7	3syl	|- ( N e. ( NrmSGrp ` G ) -> ( 0g ` G ) e. ( Base ` G ) )
9	2 3 4 8	quslsm	|- ( N e. ( NrmSGrp ` G ) -> [ ( 0g ` G ) ] ( G ~QG N ) = ( { ( 0g ` G ) } ( LSSum ` G ) N ) )
10	1 6	qus0	|- ( N e. ( NrmSGrp ` G ) -> [ ( 0g ` G ) ] ( G ~QG N ) = ( 0g ` Q ) )
11	6 3	lsm02	|- ( N e. ( SubGrp ` G ) -> ( { ( 0g ` G ) } ( LSSum ` G ) N ) = N )
12	4 11	syl	|- ( N e. ( NrmSGrp ` G ) -> ( { ( 0g ` G ) } ( LSSum ` G ) N ) = N )
13	9 10 12	3eqtr3d	|- ( N e. ( NrmSGrp ` G ) -> ( 0g ` Q ) = N )