Metamath Proof Explorer

Theorem grpnpcan

Description: Cancellation law for subtraction ( npcan analog). (Contributed by NM, 19-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		grpsubadd.b	$⊢ B = {Base}_{G}$
2		grpsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
4		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
5	1 4	grpinvcl	$⊢ (G \in Grp \land Y \in B) \to {inv}_{g} (G) (Y) \in B$
6	5	3adant2	$⊢ (G \in Grp \land X \in B \land Y \in B) \to {inv}_{g} (G) (Y) \in B$
7	1 2	grpcl	$⊢ (G \in Grp \land X \in B \land {inv}_{g} (G) (Y) \in B) \to X \underset{˙}{+} {inv}_{g} (G) (Y) \in B$
8	6 7	syld3an3	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} {inv}_{g} (G) (Y) \in B$
9	1 2 4 3	grpsubval	$⊢ (X \underset{˙}{+} {inv}_{g} (G) (Y) \in B \land {inv}_{g} (G) (Y) \in B) \to (X \underset{˙}{+} {inv}_{g} (G) (Y)) \underset{˙}{-} {inv}_{g} (G) (Y) = (X \underset{˙}{+} {inv}_{g} (G) (Y)) \underset{˙}{+} {inv}_{g} (G) ({inv}_{g} (G) (Y))$
10	8 6 9	syl2anc	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (X \underset{˙}{+} {inv}_{g} (G) (Y)) \underset{˙}{-} {inv}_{g} (G) (Y) = (X \underset{˙}{+} {inv}_{g} (G) (Y)) \underset{˙}{+} {inv}_{g} (G) ({inv}_{g} (G) (Y))$
11	1 2 3	grppncan	$⊢ (G \in Grp \land X \in B \land {inv}_{g} (G) (Y) \in B) \to (X \underset{˙}{+} {inv}_{g} (G) (Y)) \underset{˙}{-} {inv}_{g} (G) (Y) = X$
12	6 11	syld3an3	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (X \underset{˙}{+} {inv}_{g} (G) (Y)) \underset{˙}{-} {inv}_{g} (G) (Y) = X$
13	1 2 4 3	grpsubval	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{-} Y = X \underset{˙}{+} {inv}_{g} (G) (Y)$
14	13	3adant1	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{-} Y = X \underset{˙}{+} {inv}_{g} (G) (Y)$
15	14	eqcomd	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} {inv}_{g} (G) (Y) = X \underset{˙}{-} Y$
16	1 4	grpinvinv	$⊢ (G \in Grp \land Y \in B) \to {inv}_{g} (G) ({inv}_{g} (G) (Y)) = Y$
17	16	3adant2	$⊢ (G \in Grp \land X \in B \land Y \in B) \to {inv}_{g} (G) ({inv}_{g} (G) (Y)) = Y$
18	15 17	oveq12d	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (X \underset{˙}{+} {inv}_{g} (G) (Y)) \underset{˙}{+} {inv}_{g} (G) ({inv}_{g} (G) (Y)) = (X \underset{˙}{-} Y) \underset{˙}{+} Y$
19	10 12 18	3eqtr3rd	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (X \underset{˙}{-} Y) \underset{˙}{+} Y = X$