Theorem ablnnncan1

Description: Cancellation law for group subtraction. ( nnncan1 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$$
	ablsub32.z	$$⊢\phi \to Z\in B$$
Assertion	ablnnncan1	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}Z\right)=Z\underset{\dot{}}{-}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		ablsub32.z	$$⊢\phi \to Z\in B$$
7		ablgrp	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{Grp}$$
8	3 7	syl	$$⊢\phi \to G\in \mathrm{Grp}$$
9	1 2	grpsubcl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Z\in B\right)\to X\underset{\dot{}}{-}Z\in B$$
10	8 4 6 9	syl3anc	$$⊢\phi \to X\underset{\dot{}}{-}Z\in B$$
11	1 2 3 4 5 10	ablsub32	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}Z\right)=\left(X\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{-}Y$$
12	1 2 3 4 6	ablnncan	$$⊢\phi \to X\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}Z\right)=Z$$
13	12	oveq1d	$$⊢\phi \to \left(X\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{-}Y=Z\underset{\dot{}}{-}Y$$
14	11 13	eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}Z\right)=Z\underset{\dot{}}{-}Y$$