This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑄 ) = 𝑁 )