Theorem ablpnpcan

Description: Cancellation law for mixed addition and subtraction. ( pnpcan analog.) (Contributed by NM, 29-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ablsubadd.b	$$⊢B={\mathrm{Base}}_G$$
2		ablsubadd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		ablsubadd.m	$$⊢\underset{\dot{}}{-}={-}_G$$
4		ablsubsub.g	$$⊢\phi \to G\in \mathrm{Abel}$$
5		ablsubsub.x	$$⊢\phi \to X\in B$$
6		ablsubsub.y	$$⊢\phi \to Y\in B$$
7		ablsubsub.z	$$⊢\phi \to Z\in B$$
8		ablpnpcan.g	$$⊢\phi \to G\in \mathrm{Abel}$$
9		ablpnpcan.x	$$⊢\phi \to X\in B$$
10		ablpnpcan.y	$$⊢\phi \to Y\in B$$
11		ablpnpcan.z	$$⊢\phi \to Z\in B$$
12	1 2 3	ablsub4	$$⊢\left(G\in \mathrm{Abel}\wedge \left(X\in B\wedge Y\in B\right)\wedge \left(X\in B\wedge Z\in B\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{+}Z\right)=\left(X\underset{\dot{}}{-}X\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{-}Z\right)$$
13	4 5 6 5 7 12	syl122anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{+}Z\right)=\left(X\underset{\dot{}}{-}X\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{-}Z\right)$$
14		ablgrp	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{Grp}$$
15	4 14	syl	$$⊢\phi \to G\in \mathrm{Grp}$$
16		eqid	$$⊢0_G=0_G$$
17	1 16 3	grpsubid	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X\underset{\dot{}}{-}X=0_G$$
18	15 5 17	syl2anc	$$⊢\phi \to X\underset{\dot{}}{-}X=0_G$$
19	18	oveq1d	$$⊢\phi \to \left(X\underset{\dot{}}{-}X\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{-}Z\right)=0_G\underset{\dot{}}{+}\left(Y\underset{\dot{}}{-}Z\right)$$
20	1 3	grpsubcl	$$⊢\left(G\in \mathrm{Grp}\wedge Y\in B\wedge Z\in B\right)\to Y\underset{\dot{}}{-}Z\in B$$
21	15 6 7 20	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{-}Z\in B$$
22	1 2 16	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge Y\underset{\dot{}}{-}Z\in B\right)\to 0_G\underset{\dot{}}{+}\left(Y\underset{\dot{}}{-}Z\right)=Y\underset{\dot{}}{-}Z$$
23	15 21 22	syl2anc	$$⊢\phi \to 0_G\underset{\dot{}}{+}\left(Y\underset{\dot{}}{-}Z\right)=Y\underset{\dot{}}{-}Z$$
24	13 19 23	3eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{+}Z\right)=Y\underset{\dot{}}{-}Z$$