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

Metamath Proof Explorer

Theorem subgsub

Description: The subtraction of elements in a subgroup is the same as subtraction in the group. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses subgsubcl.p 
|- .- = ( -g ` G )
subgsub.h 
|- H = ( G |`s S )
subgsub.n 
|- N = ( -g ` H )
Assertion subgsub 
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .- Y ) = ( X N Y ) )

Proof

Step Hyp Ref Expression
1 subgsubcl.p 
 |-  .- = ( -g ` G )
2 subgsub.h 
 |-  H = ( G |`s S )
3 subgsub.n 
 |-  N = ( -g ` H )
4 eqid 
 |-  ( +g ` G ) = ( +g ` G )
5 2 4 ressplusg 
 |-  ( S e. ( SubGrp ` G ) -> ( +g ` G ) = ( +g ` H ) )
6 5 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( +g ` G ) = ( +g ` H ) )
7 eqidd 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> X = X )
8 eqid 
 |-  ( invg ` G ) = ( invg ` G )
9 eqid 
 |-  ( invg ` H ) = ( invg ` H )
10 2 8 9 subginv 
 |-  ( ( S e. ( SubGrp ` G ) /\ Y e. S ) -> ( ( invg ` G ) ` Y ) = ( ( invg ` H ) ` Y ) )
11 10 3adant2 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( ( invg ` G ) ` Y ) = ( ( invg ` H ) ` Y ) )
12 6 7 11 oveq123d 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) = ( X ( +g ` H ) ( ( invg ` H ) ` Y ) ) )
13 eqid 
 |-  ( Base ` G ) = ( Base ` G )
14 13 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
15 14 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> S C_ ( Base ` G ) )
16 simp2 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> X e. S )
17 15 16 sseldd 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> X e. ( Base ` G ) )
18 simp3 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> Y e. S )
19 15 18 sseldd 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> Y e. ( Base ` G ) )
20 13 4 8 1 grpsubval 
 |-  ( ( X e. ( Base ` G ) /\ Y e. ( Base ` G ) ) -> ( X .- Y ) = ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) )
21 17 19 20 syl2anc 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .- Y ) = ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) )
22 2 subgbas 
 |-  ( S e. ( SubGrp ` G ) -> S = ( Base ` H ) )
23 22 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> S = ( Base ` H ) )
24 16 23 eleqtrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> X e. ( Base ` H ) )
25 18 23 eleqtrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> Y e. ( Base ` H ) )
26 eqid 
 |-  ( Base ` H ) = ( Base ` H )
27 eqid 
 |-  ( +g ` H ) = ( +g ` H )
28 26 27 9 3 grpsubval 
 |-  ( ( X e. ( Base ` H ) /\ Y e. ( Base ` H ) ) -> ( X N Y ) = ( X ( +g ` H ) ( ( invg ` H ) ` Y ) ) )
29 24 25 28 syl2anc 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X N Y ) = ( X ( +g ` H ) ( ( invg ` H ) ` Y ) ) )
30 12 21 29 3eqtr4d 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .- Y ) = ( X N Y ) )