Theorem ablnncan

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

	Ref	Expression
Hypotheses	ablnncan.b	$$⊢B={\mathrm{Base}}_G$$
	ablnncan.m	$$⊢\underset{\dot{}}{-}={-}_G$$
	ablnncan.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	ablnncan.x	$$⊢\phi \to X\in B$$
	ablnncan.y	$$⊢\phi \to Y\in B$$
Assertion	ablnncan	$$⊢\phi \to X\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}Y\right)=Y$$

Proof

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