subgsubcl

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

		Ref	Expression
	Hypothesis	subgsubcl.p	$⊢ \underset{˙}{-} = -_{G}$
	Assertion	subgsubcl	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \underset{˙}{-} Y \in S$

Step	Hyp	Ref	Expression
1		subgsubcl.p	$⊢ \underset{˙}{-} = -_{G}$
2		eqid	$⊢ {Base}_{G} = {Base}_{G}$
3	2	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
4	3	3ad2ant1	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to S \subseteq {Base}_{G}$
5		simp2	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \in S$
6	4 5	sseldd	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \in {Base}_{G}$
7		simp3	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to Y \in S$
8	4 7	sseldd	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to Y \in {Base}_{G}$
9		eqid	$⊢ +_{G} = +_{G}$
10		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
11	2 9 10 1	grpsubval	$⊢ (X \in {Base}_{G} \land Y \in {Base}_{G}) \to X \underset{˙}{-} Y = X +_{G} {inv}_{g} (G) (Y)$
12	6 8 11	syl2anc	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \underset{˙}{-} Y = X +_{G} {inv}_{g} (G) (Y)$
13	10	subginvcl	$⊢ (S \in SubGrp (G) \land Y \in S) \to {inv}_{g} (G) (Y) \in S$
14	13	3adant2	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to {inv}_{g} (G) (Y) \in S$
15	9	subgcl	$⊢ (S \in SubGrp (G) \land X \in S \land {inv}_{g} (G) (Y) \in S) \to X +_{G} {inv}_{g} (G) (Y) \in S$
16	14 15	syld3an3	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X +_{G} {inv}_{g} (G) (Y) \in S$
17	12 16	eqeltrd	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \underset{˙}{-} Y \in S$

Metamath Proof Explorer