Metamath Proof Explorer

Theorem qusinv

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

Ref Expression
Hypotheses qusgrp.h 
|- H = ( G /s ( G ~QG S ) )
qusinv.v 
|- V = ( Base ` G )
qusinv.i 
|- I = ( invg ` G )
qusinv.n 
|- N = ( invg ` H )
Assertion qusinv 
|- ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> ( N ` [ X ] ( G ~QG S ) ) = [ ( I ` X ) ] ( G ~QG S ) )

Proof

Step Hyp Ref Expression
1 qusgrp.h 
 |-  H = ( G /s ( G ~QG S ) )
2 qusinv.v 
 |-  V = ( Base ` G )
3 qusinv.i 
 |-  I = ( invg ` G )
4 qusinv.n 
 |-  N = ( invg ` H )
5 nsgsubg 
 |-  ( S e. ( NrmSGrp ` G ) -> S e. ( SubGrp ` G ) )
6 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
7 5 6 syl 
 |-  ( S e. ( NrmSGrp ` G ) -> G e. Grp )
8 2 3 grpinvcl 
 |-  ( ( G e. Grp /\ X e. V ) -> ( I ` X ) e. V )
9 7 8 sylan 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> ( I ` X ) e. V )
10 eqid 
 |-  ( +g ` G ) = ( +g ` G )
11 eqid 
 |-  ( +g ` H ) = ( +g ` H )
12 1 2 10 11 qusadd 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V /\ ( I ` X ) e. V ) -> ( [ X ] ( G ~QG S ) ( +g ` H ) [ ( I ` X ) ] ( G ~QG S ) ) = [ ( X ( +g ` G ) ( I ` X ) ) ] ( G ~QG S ) )
13 9 12 mpd3an3 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> ( [ X ] ( G ~QG S ) ( +g ` H ) [ ( I ` X ) ] ( G ~QG S ) ) = [ ( X ( +g ` G ) ( I ` X ) ) ] ( G ~QG S ) )
14 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
15 2 10 14 3 grprinv 
 |-  ( ( G e. Grp /\ X e. V ) -> ( X ( +g ` G ) ( I ` X ) ) = ( 0g ` G ) )
16 7 15 sylan 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> ( X ( +g ` G ) ( I ` X ) ) = ( 0g ` G ) )
17 16 eceq1d 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> [ ( X ( +g ` G ) ( I ` X ) ) ] ( G ~QG S ) = [ ( 0g ` G ) ] ( G ~QG S ) )
18 1 14 qus0 
 |-  ( S e. ( NrmSGrp ` G ) -> [ ( 0g ` G ) ] ( G ~QG S ) = ( 0g ` H ) )
19 18 adantr 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> [ ( 0g ` G ) ] ( G ~QG S ) = ( 0g ` H ) )
20 13 17 19 3eqtrd 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> ( [ X ] ( G ~QG S ) ( +g ` H ) [ ( I ` X ) ] ( G ~QG S ) ) = ( 0g ` H ) )
21 1 qusgrp 
 |-  ( S e. ( NrmSGrp ` G ) -> H e. Grp )
22 21 adantr 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> H e. Grp )
23 eqid 
 |-  ( Base ` H ) = ( Base ` H )
24 1 2 23 quseccl 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> [ X ] ( G ~QG S ) e. ( Base ` H ) )
25 1 2 23 quseccl 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ ( I ` X ) e. V ) -> [ ( I ` X ) ] ( G ~QG S ) e. ( Base ` H ) )
26 9 25 syldan 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> [ ( I ` X ) ] ( G ~QG S ) e. ( Base ` H ) )
27 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
28 23 11 27 4 grpinvid1 
 |-  ( ( H e. Grp /\ [ X ] ( G ~QG S ) e. ( Base ` H ) /\ [ ( I ` X ) ] ( G ~QG S ) e. ( Base ` H ) ) -> ( ( N ` [ X ] ( G ~QG S ) ) = [ ( I ` X ) ] ( G ~QG S ) <-> ( [ X ] ( G ~QG S ) ( +g ` H ) [ ( I ` X ) ] ( G ~QG S ) ) = ( 0g ` H ) ) )
29 22 24 26 28 syl3anc 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> ( ( N ` [ X ] ( G ~QG S ) ) = [ ( I ` X ) ] ( G ~QG S ) <-> ( [ X ] ( G ~QG S ) ( +g ` H ) [ ( I ` X ) ] ( G ~QG S ) ) = ( 0g ` H ) ) )
30 20 29 mpbird 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> ( N ` [ X ] ( G ~QG S ) ) = [ ( I ` X ) ] ( G ~QG S ) )