grpnnncan2

Description: Cancellation law for group subtraction. ( nnncan2 analog.) (Contributed by NM, 15-Feb-2008) (Revised by Mario Carneiro, 2-Dec-2014)

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

Step	Hyp	Ref	Expression
1		grpnnncan2.b	$⊢ B = {Base}_{G}$
2		grpnnncan2.m	$⊢ \underset{˙}{-} = -_{G}$
3		simpl	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to G \in Grp$
4		simpr1	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
5		simpr3	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
6	1 2	grpsubcl	$⊢ (G \in Grp \land Y \in B \land Z \in B) \to Y \underset{˙}{-} Z \in B$
7	6	3adant3r1	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{-} Z \in B$
8		eqid	$⊢ +_{G} = +_{G}$
9	1 8 2	grpsubsub4	$⊢ (G \in Grp \land (X \in B \land Z \in B \land Y \underset{˙}{-} Z \in B)) \to (X \underset{˙}{-} Z) \underset{˙}{-} (Y \underset{˙}{-} Z) = X \underset{˙}{-} ((Y \underset{˙}{-} Z) +_{G} Z)$
10	3 4 5 7 9	syl13anc	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Z) \underset{˙}{-} (Y \underset{˙}{-} Z) = X \underset{˙}{-} ((Y \underset{˙}{-} Z) +_{G} Z)$
11	1 8 2	grpnpcan	$⊢ (G \in Grp \land Y \in B \land Z \in B) \to (Y \underset{˙}{-} Z) +_{G} Z = Y$
12	11	3adant3r1	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (Y \underset{˙}{-} Z) +_{G} Z = Y$
13	12	oveq2d	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{-} ((Y \underset{˙}{-} Z) +_{G} Z) = X \underset{˙}{-} Y$
14	10 13	eqtrd	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Z) \underset{˙}{-} (Y \underset{˙}{-} Z) = X \underset{˙}{-} Y$

Metamath Proof Explorer