Theorem ablnnncan

Description: Cancellation law for group subtraction. ( nnncan analog.) (Contributed by NM, 29-Feb-2008) (Revised by AV, 27-Aug-2021)

	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	ablnnncan	$$⊢\phi \to \left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{-}Z=X\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		eqid	$$⊢{+}_G={+}_G$$
8		ablgrp	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{Grp}$$
9	3 8	syl	$$⊢\phi \to G\in \mathrm{Grp}$$
10	1 2	grpsubcl	$$⊢\left(G\in \mathrm{Grp}\wedge Y\in B\wedge Z\in B\right)\to Y\underset{\dot{}}{-}Z\in B$$
11	9 5 6 10	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{-}Z\in B$$
12	1 7 2 3 4 11 6	ablsubsub4	$$⊢\phi \to \left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{-}Z=X\underset{\dot{}}{-}\left(\left(Y\underset{\dot{}}{-}Z\right){+}_{G}Z\right)$$
13	1 7	ablcom	$$⊢\left(G\in \mathrm{Abel}\wedge Y\underset{\dot{}}{-}Z\in B\wedge Z\in B\right)\to \left(Y\underset{\dot{}}{-}Z\right){+}_{G}Z=Z{+}_G\left(Y\underset{\dot{}}{-}Z\right)$$
14	3 11 6 13	syl3anc	$$⊢\phi \to \left(Y\underset{\dot{}}{-}Z\right){+}_{G}Z=Z{+}_G\left(Y\underset{\dot{}}{-}Z\right)$$
15	1 7 2	ablpncan3	$$⊢\left(G\in \mathrm{Abel}\wedge \left(Z\in B\wedge Y\in B\right)\right)\to Z{+}_G\left(Y\underset{\dot{}}{-}Z\right)=Y$$
16	3 6 5 15	syl12anc	$$⊢\phi \to Z{+}_G\left(Y\underset{\dot{}}{-}Z\right)=Y$$
17	14 16	eqtrd	$$⊢\phi \to \left(Y\underset{\dot{}}{-}Z\right){+}_{G}Z=Y$$
18	17	oveq2d	$$⊢\phi \to X\underset{\dot{}}{-}\left(\left(Y\underset{\dot{}}{-}Z\right){+}_{G}Z\right)=X\underset{\dot{}}{-}Y$$
19	12 18	eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{-}Z=X\underset{\dot{}}{-}Y$$