Theorem qus0g

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

	Ref	Expression
Hypothesis	qus0g.1	⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
Assertion	qus0g	⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → ( 0g ‘ 𝑄 ) = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		qus0g.1	⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
2		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3		eqid	⊢ ( LSSum ‘ 𝐺 ) = ( LSSum ‘ 𝐺 )
4		nsgsubg	⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
5		subgrcl	⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
6		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
7	2 6	grpidcl	⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
8	4 5 7	3syl	⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
9	2 3 4 8	quslsm	⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑁 ) = ( { ( 0g ‘ 𝐺 ) } ( LSSum ‘ 𝐺 ) 𝑁 ) )
10	1 6	qus0	⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑁 ) = ( 0g ‘ 𝑄 ) )
11	6 3	lsm02	⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → ( { ( 0g ‘ 𝐺 ) } ( LSSum ‘ 𝐺 ) 𝑁 ) = 𝑁 )
12	4 11	syl	⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → ( { ( 0g ‘ 𝐺 ) } ( LSSum ‘ 𝐺 ) 𝑁 ) = 𝑁 )
13	9 10 12	3eqtr3d	⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → ( 0g ‘ 𝑄 ) = 𝑁 )