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 ) )