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

Metamath Proof Explorer

Theorem subgsubcl

Description: A subgroup is closed under group subtraction. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypothesis subgsubcl.p 
|- .- = ( -g ` G )
Assertion subgsubcl 
|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .- Y ) e. S )

Proof

Step Hyp Ref Expression
1 subgsubcl.p 
 |-  .- = ( -g ` G )
2 eqid 
 |-  ( Base ` G ) = ( Base ` G )
3 2 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
4 3 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> S C_ ( Base ` G ) )
5 simp2 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> X e. S )
6 4 5 sseldd 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> X e. ( Base ` G ) )
7 simp3 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> Y e. S )
8 4 7 sseldd 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> Y e. ( Base ` G ) )
9 eqid 
 |-  ( +g ` G ) = ( +g ` G )
10 eqid 
 |-  ( invg ` G ) = ( invg ` G )
11 2 9 10 1 grpsubval 
 |-  ( ( X e. ( Base ` G ) /\ Y e. ( Base ` G ) ) -> ( X .- Y ) = ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) )
12 6 8 11 syl2anc 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .- Y ) = ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) )
13 10 subginvcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ Y e. S ) -> ( ( invg ` G ) ` Y ) e. S )
14 13 3adant2 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( ( invg ` G ) ` Y ) e. S )
15 9 subgcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ ( ( invg ` G ) ` Y ) e. S ) -> ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) e. S )
16 14 15 syld3an3 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) e. S )
17 12 16 eqeltrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .- Y ) e. S )