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

Metamath Proof Explorer

Theorem nsgqus0

Description: A normal subgroup N is a member of all subgroups F of the quotient group by N . In fact, it is the identity element of the quotient group. (Contributed by Thierry Arnoux, 27-Jul-2024)

Ref Expression
Hypothesis nsgqus0.q 
|- Q = ( G /s ( G ~QG N ) )
Assertion nsgqus0 
|- ( ( N e. ( NrmSGrp ` G ) /\ F e. ( SubGrp ` Q ) ) -> N e. F )

Proof

Step Hyp Ref Expression
1 nsgqus0.q 
 |-  Q = ( G /s ( G ~QG N ) )
2 simpl 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ F e. ( SubGrp ` Q ) ) -> N e. ( NrmSGrp ` G ) )
3 nsgsubg 
 |-  ( N e. ( NrmSGrp ` G ) -> N e. ( SubGrp ` G ) )
4 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
5 eqid 
 |-  ( LSSum ` G ) = ( LSSum ` G )
6 4 5 lsm02 
 |-  ( N e. ( SubGrp ` G ) -> ( { ( 0g ` G ) } ( LSSum ` G ) N ) = N )
7 2 3 6 3syl 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ F e. ( SubGrp ` Q ) ) -> ( { ( 0g ` G ) } ( LSSum ` G ) N ) = N )
8 1 4 qus0 
 |-  ( N e. ( NrmSGrp ` G ) -> [ ( 0g ` G ) ] ( G ~QG N ) = ( 0g ` Q ) )
9 8 adantr 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ F e. ( SubGrp ` Q ) ) -> [ ( 0g ` G ) ] ( G ~QG N ) = ( 0g ` Q ) )
10 eqid 
 |-  ( Base ` G ) = ( Base ` G )
11 3 adantr 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ F e. ( SubGrp ` Q ) ) -> N e. ( SubGrp ` G ) )
12 subgrcl 
 |-  ( N e. ( SubGrp ` G ) -> G e. Grp )
13 3 12 syl 
 |-  ( N e. ( NrmSGrp ` G ) -> G e. Grp )
14 13 adantr 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ F e. ( SubGrp ` Q ) ) -> G e. Grp )
15 10 4 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. ( Base ` G ) )
16 14 15 syl 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ F e. ( SubGrp ` Q ) ) -> ( 0g ` G ) e. ( Base ` G ) )
17 10 5 11 16 quslsm 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ F e. ( SubGrp ` Q ) ) -> [ ( 0g ` G ) ] ( G ~QG N ) = ( { ( 0g ` G ) } ( LSSum ` G ) N ) )
18 9 17 eqtr3d 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ F e. ( SubGrp ` Q ) ) -> ( 0g ` Q ) = ( { ( 0g ` G ) } ( LSSum ` G ) N ) )
19 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
20 19 subg0cl 
 |-  ( F e. ( SubGrp ` Q ) -> ( 0g ` Q ) e. F )
21 20 adantl 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ F e. ( SubGrp ` Q ) ) -> ( 0g ` Q ) e. F )
22 18 21 eqeltrrd 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ F e. ( SubGrp ` Q ) ) -> ( { ( 0g ` G ) } ( LSSum ` G ) N ) e. F )
23 7 22 eqeltrrd 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ F e. ( SubGrp ` Q ) ) -> N e. F )