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 )