Metamath Proof Explorer

Theorem qus0

Description: Value of the group identity operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses qusgrp.h 
|- H = ( G /s ( G ~QG S ) )
qus0.p 
|- .0. = ( 0g ` G )
Assertion qus0 
|- ( S e. ( NrmSGrp ` G ) -> [ .0. ] ( G ~QG S ) = ( 0g ` H ) )

Proof

Step Hyp Ref Expression
1 qusgrp.h 
 |-  H = ( G /s ( G ~QG S ) )
2 qus0.p 
 |-  .0. = ( 0g ` G )
3 nsgsubg 
 |-  ( S e. ( NrmSGrp ` G ) -> S e. ( SubGrp ` G ) )
4 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
5 3 4 syl 
 |-  ( S e. ( NrmSGrp ` G ) -> G e. Grp )
6 eqid 
 |-  ( Base ` G ) = ( Base ` G )
7 6 2 grpidcl 
 |-  ( G e. Grp -> .0. e. ( Base ` G ) )
8 5 7 syl 
 |-  ( S e. ( NrmSGrp ` G ) -> .0. e. ( Base ` G ) )
9 eqid 
 |-  ( +g ` G ) = ( +g ` G )
10 eqid 
 |-  ( +g ` H ) = ( +g ` H )
11 1 6 9 10 qusadd 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ .0. e. ( Base ` G ) /\ .0. e. ( Base ` G ) ) -> ( [ .0. ] ( G ~QG S ) ( +g ` H ) [ .0. ] ( G ~QG S ) ) = [ ( .0. ( +g ` G ) .0. ) ] ( G ~QG S ) )
12 8 8 11 mpd3an23 
 |-  ( S e. ( NrmSGrp ` G ) -> ( [ .0. ] ( G ~QG S ) ( +g ` H ) [ .0. ] ( G ~QG S ) ) = [ ( .0. ( +g ` G ) .0. ) ] ( G ~QG S ) )
13 6 9 2 grplid 
 |-  ( ( G e. Grp /\ .0. e. ( Base ` G ) ) -> ( .0. ( +g ` G ) .0. ) = .0. )
14 5 8 13 syl2anc 
 |-  ( S e. ( NrmSGrp ` G ) -> ( .0. ( +g ` G ) .0. ) = .0. )
15 14 eceq1d 
 |-  ( S e. ( NrmSGrp ` G ) -> [ ( .0. ( +g ` G ) .0. ) ] ( G ~QG S ) = [ .0. ] ( G ~QG S ) )
16 12 15 eqtrd 
 |-  ( S e. ( NrmSGrp ` G ) -> ( [ .0. ] ( G ~QG S ) ( +g ` H ) [ .0. ] ( G ~QG S ) ) = [ .0. ] ( G ~QG S ) )
17 1 qusgrp 
 |-  ( S e. ( NrmSGrp ` G ) -> H e. Grp )
18 eqid 
 |-  ( Base ` H ) = ( Base ` H )
19 1 6 18 quseccl 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ .0. e. ( Base ` G ) ) -> [ .0. ] ( G ~QG S ) e. ( Base ` H ) )
20 8 19 mpdan 
 |-  ( S e. ( NrmSGrp ` G ) -> [ .0. ] ( G ~QG S ) e. ( Base ` H ) )
21 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
22 18 10 21 grpid 
 |-  ( ( H e. Grp /\ [ .0. ] ( G ~QG S ) e. ( Base ` H ) ) -> ( ( [ .0. ] ( G ~QG S ) ( +g ` H ) [ .0. ] ( G ~QG S ) ) = [ .0. ] ( G ~QG S ) <-> ( 0g ` H ) = [ .0. ] ( G ~QG S ) ) )
23 17 20 22 syl2anc 
 |-  ( S e. ( NrmSGrp ` G ) -> ( ( [ .0. ] ( G ~QG S ) ( +g ` H ) [ .0. ] ( G ~QG S ) ) = [ .0. ] ( G ~QG S ) <-> ( 0g ` H ) = [ .0. ] ( G ~QG S ) ) )
24 16 23 mpbid 
 |-  ( S e. ( NrmSGrp ` G ) -> ( 0g ` H ) = [ .0. ] ( G ~QG S ) )
25 24 eqcomd 
 |-  ( S e. ( NrmSGrp ` G ) -> [ .0. ] ( G ~QG S ) = ( 0g ` H ) )