ablnncan

Description: Cancellation law for group subtraction. ( nncan analog.) (Contributed by NM, 7-Apr-2015)

Step	Hyp	Ref	Expression
1		ablnncan.b	$⊢ B = {Base}_{G}$
2		ablnncan.m	$⊢ \underset{˙}{-} = -_{G}$
3		ablnncan.g	$⊢ φ \to G \in Abel$
4		ablnncan.x	$⊢ φ \to X \in B$
5		ablnncan.y	$⊢ φ \to Y \in B$
6		eqid	$⊢ +_{G} = +_{G}$
7	1 6 2 3 4 4 5	ablsubsub	$⊢ φ \to X \underset{˙}{-} (X \underset{˙}{-} Y) = (X \underset{˙}{-} X) +_{G} Y$
8		ablgrp	$⊢ G \in Abel \to G \in Grp$
9	3 8	syl	$⊢ φ \to G \in Grp$
10		eqid	$⊢ 0_{G} = 0_{G}$
11	1 10 2	grpsubid	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{-} X = 0_{G}$
12	9 4 11	syl2anc	$⊢ φ \to X \underset{˙}{-} X = 0_{G}$
13	12	oveq1d	$⊢ φ \to (X \underset{˙}{-} X) +_{G} Y = 0_{G} +_{G} Y$
14	1 6 10	grplid	$⊢ (G \in Grp \land Y \in B) \to 0_{G} +_{G} Y = Y$
15	9 5 14	syl2anc	$⊢ φ \to 0_{G} +_{G} Y = Y$
16	7 13 15	3eqtrd	$⊢ φ \to X \underset{˙}{-} (X \underset{˙}{-} Y) = Y$

Metamath Proof Explorer