grpsubsub

Description: Double group subtraction. (Contributed by NM, 24-Feb-2008) (Revised by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	grpsubadd.b	$⊢ B = {Base}_{G}$
	grpsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
	grpsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
Assertion	grpsubsub	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{-} (Y \underset{˙}{-} Z) = X \underset{˙}{+} (Z \underset{˙}{-} Y)$

Step	Hyp	Ref	Expression
1		grpsubadd.b	$⊢ B = {Base}_{G}$
2		grpsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
4		simpr1	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
5	1 3	grpsubcl	$⊢ (G \in Grp \land Y \in B \land Z \in B) \to Y \underset{˙}{-} Z \in B$
6	5	3adant3r1	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{-} Z \in B$
7		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
8	1 2 7 3	grpsubval	$⊢ (X \in B \land Y \underset{˙}{-} Z \in B) \to X \underset{˙}{-} (Y \underset{˙}{-} Z) = X \underset{˙}{+} {inv}_{g} (G) (Y \underset{˙}{-} Z)$
9	4 6 8	syl2anc	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{-} (Y \underset{˙}{-} Z) = X \underset{˙}{+} {inv}_{g} (G) (Y \underset{˙}{-} Z)$
10	1 3 7	grpinvsub	$⊢ (G \in Grp \land Y \in B \land Z \in B) \to {inv}_{g} (G) (Y \underset{˙}{-} Z) = Z \underset{˙}{-} Y$
11	10	3adant3r1	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to {inv}_{g} (G) (Y \underset{˙}{-} Z) = Z \underset{˙}{-} Y$
12	11	oveq2d	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{+} {inv}_{g} (G) (Y \underset{˙}{-} Z) = X \underset{˙}{+} (Z \underset{˙}{-} Y)$
13	9 12	eqtrd	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{-} (Y \underset{˙}{-} Z) = X \underset{˙}{+} (Z \underset{˙}{-} Y)$

Metamath Proof Explorer