Metamath Proof Explorer

Theorem qussub

Description: Value of the group subtraction 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 )
qussub.p 
|- .- = ( -g ` G )
qussub.a 
|- N = ( -g ` H )
Assertion qussub 
|- ( ( S e. ( NrmSGrp ` G ) /\ X e. V /\ Y e. V ) -> ( [ X ] ( G ~QG S ) N [ Y ] ( G ~QG S ) ) = [ ( X .- Y ) ] ( G ~QG S ) )

Proof

Step Hyp Ref Expression
1 qusgrp.h 
 |-  H = ( G /s ( G ~QG S ) )
2 qusinv.v 
 |-  V = ( Base ` G )
3 qussub.p 
 |-  .- = ( -g ` G )
4 qussub.a 
 |-  N = ( -g ` H )
5 eqid 
 |-  ( Base ` H ) = ( Base ` H )
6 1 2 5 quseccl 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V ) -> [ X ] ( G ~QG S ) e. ( Base ` H ) )
7 6 3adant3 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V /\ Y e. V ) -> [ X ] ( G ~QG S ) e. ( Base ` H ) )
8 1 2 5 quseccl 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ Y e. V ) -> [ Y ] ( G ~QG S ) e. ( Base ` H ) )
9 eqid 
 |-  ( +g ` H ) = ( +g ` H )
10 eqid 
 |-  ( invg ` H ) = ( invg ` H )
11 5 9 10 4 grpsubval 
 |-  ( ( [ X ] ( G ~QG S ) e. ( Base ` H ) /\ [ Y ] ( G ~QG S ) e. ( Base ` H ) ) -> ( [ X ] ( G ~QG S ) N [ Y ] ( G ~QG S ) ) = ( [ X ] ( G ~QG S ) ( +g ` H ) ( ( invg ` H ) ` [ Y ] ( G ~QG S ) ) ) )
12 7 8 11 3imp3i2an 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V /\ Y e. V ) -> ( [ X ] ( G ~QG S ) N [ Y ] ( G ~QG S ) ) = ( [ X ] ( G ~QG S ) ( +g ` H ) ( ( invg ` H ) ` [ Y ] ( G ~QG S ) ) ) )
13 eqid 
 |-  ( invg ` G ) = ( invg ` G )
14 1 2 13 10 qusinv 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ Y e. V ) -> ( ( invg ` H ) ` [ Y ] ( G ~QG S ) ) = [ ( ( invg ` G ) ` Y ) ] ( G ~QG S ) )
15 14 3adant2 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V /\ Y e. V ) -> ( ( invg ` H ) ` [ Y ] ( G ~QG S ) ) = [ ( ( invg ` G ) ` Y ) ] ( G ~QG S ) )
16 15 oveq2d 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V /\ Y e. V ) -> ( [ X ] ( G ~QG S ) ( +g ` H ) ( ( invg ` H ) ` [ Y ] ( G ~QG S ) ) ) = ( [ X ] ( G ~QG S ) ( +g ` H ) [ ( ( invg ` G ) ` Y ) ] ( G ~QG S ) ) )
17 nsgsubg 
 |-  ( S e. ( NrmSGrp ` G ) -> S e. ( SubGrp ` G ) )
18 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
19 17 18 syl 
 |-  ( S e. ( NrmSGrp ` G ) -> G e. Grp )
20 2 13 grpinvcl 
 |-  ( ( G e. Grp /\ Y e. V ) -> ( ( invg ` G ) ` Y ) e. V )
21 19 20 sylan 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ Y e. V ) -> ( ( invg ` G ) ` Y ) e. V )
22 21 3adant2 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V /\ Y e. V ) -> ( ( invg ` G ) ` Y ) e. V )
23 eqid 
 |-  ( +g ` G ) = ( +g ` G )
24 1 2 23 9 qusadd 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V /\ ( ( invg ` G ) ` Y ) e. V ) -> ( [ X ] ( G ~QG S ) ( +g ` H ) [ ( ( invg ` G ) ` Y ) ] ( G ~QG S ) ) = [ ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) ] ( G ~QG S ) )
25 22 24 syld3an3 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V /\ Y e. V ) -> ( [ X ] ( G ~QG S ) ( +g ` H ) [ ( ( invg ` G ) ` Y ) ] ( G ~QG S ) ) = [ ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) ] ( G ~QG S ) )
26 2 23 13 3 grpsubval 
 |-  ( ( X e. V /\ Y e. V ) -> ( X .- Y ) = ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) )
27 26 3adant1 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V /\ Y e. V ) -> ( X .- Y ) = ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) )
28 27 eceq1d 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V /\ Y e. V ) -> [ ( X .- Y ) ] ( G ~QG S ) = [ ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) ] ( G ~QG S ) )
29 25 28 eqtr4d 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V /\ Y e. V ) -> ( [ X ] ( G ~QG S ) ( +g ` H ) [ ( ( invg ` G ) ` Y ) ] ( G ~QG S ) ) = [ ( X .- Y ) ] ( G ~QG S ) )
30 12 16 29 3eqtrd 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V /\ Y e. V ) -> ( [ X ] ( G ~QG S ) N [ Y ] ( G ~QG S ) ) = [ ( X .- Y ) ] ( G ~QG S ) )