Metamath Proof Explorer

Theorem grpsubrcan

Description: Right cancellation law for group subtraction. (Contributed by NM, 31-Mar-2014)

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

Proof

Step	Hyp	Ref	Expression
1		grpsubcl.b	$⊢ B = {Base}_{G}$
2		grpsubcl.m	$⊢ \underset{˙}{-} = -_{G}$
3		eqid	$⊢ +_{G} = +_{G}$
4		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
5	1 3 4 2	grpsubval	$⊢ (X \in B \land Z \in B) \to X \underset{˙}{-} Z = X +_{G} {inv}_{g} (G) (Z)$
6	5	3adant2	$⊢ (X \in B \land Y \in B \land Z \in B) \to X \underset{˙}{-} Z = X +_{G} {inv}_{g} (G) (Z)$
7	1 3 4 2	grpsubval	$⊢ (Y \in B \land Z \in B) \to Y \underset{˙}{-} Z = Y +_{G} {inv}_{g} (G) (Z)$
8	7	3adant1	$⊢ (X \in B \land Y \in B \land Z \in B) \to Y \underset{˙}{-} Z = Y +_{G} {inv}_{g} (G) (Z)$
9	6 8	eqeq12d	$⊢ (X \in B \land Y \in B \land Z \in B) \to (X \underset{˙}{-} Z = Y \underset{˙}{-} Z \leftrightarrow X +_{G} {inv}_{g} (G) (Z) = Y +_{G} {inv}_{g} (G) (Z))$
10	9	adantl	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Z = Y \underset{˙}{-} Z \leftrightarrow X +_{G} {inv}_{g} (G) (Z) = Y +_{G} {inv}_{g} (G) (Z))$
11		simpl	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to G \in Grp$
12		simpr1	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
13		simpr2	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
14	1 4	grpinvcl	$⊢ (G \in Grp \land Z \in B) \to {inv}_{g} (G) (Z) \in B$
15	14	3ad2antr3	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to {inv}_{g} (G) (Z) \in B$
16	1 3	grprcan	$⊢ (G \in Grp \land (X \in B \land Y \in B \land {inv}_{g} (G) (Z) \in B)) \to (X +_{G} {inv}_{g} (G) (Z) = Y +_{G} {inv}_{g} (G) (Z) \leftrightarrow X = Y)$
17	11 12 13 15 16	syl13anc	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X +_{G} {inv}_{g} (G) (Z) = Y +_{G} {inv}_{g} (G) (Z) \leftrightarrow X = Y)$
18	10 17	bitrd	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Z = Y \underset{˙}{-} Z \leftrightarrow X = Y)$