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