Theorem grpnpncan0

Description: Cancellation law for group subtraction ( npncan2 analog). (Contributed by AV, 24-Nov-2019)

	Ref	Expression
Hypotheses	grpsubadd.b	$$⊢B={\mathrm{Base}}_G$$
	grpsubadd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpsubadd.m	$$⊢\underset{\dot{}}{-}={-}_G$$
	grpnpncan0.0	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	grpnpncan0	$$⊢\left(G\in \mathrm{Grp}\wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{-}X\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		grpsubadd.b	$$⊢B={\mathrm{Base}}_G$$
2		grpsubadd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpsubadd.m	$$⊢\underset{\dot{}}{-}={-}_G$$
4		grpnpncan0.0	$$⊢\underset{\dot{}}{0}=0_G$$
5		simpl	$$⊢\left(G\in \mathrm{Grp}\wedge \left(X\in B\wedge Y\in B\right)\right)\to G\in \mathrm{Grp}$$
6		simprl	$$⊢\left(G\in \mathrm{Grp}\wedge \left(X\in B\wedge Y\in B\right)\right)\to X\in B$$
7		simprr	$$⊢\left(G\in \mathrm{Grp}\wedge \left(X\in B\wedge Y\in B\right)\right)\to Y\in B$$
8	1 2 3	grpnpncan	$$⊢\left(G\in \mathrm{Grp}\wedge \left(X\in B\wedge Y\in B\wedge X\in B\right)\right)\to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{-}X\right)=X\underset{\dot{}}{-}X$$
9	5 6 7 6 8	syl13anc	$$⊢\left(G\in \mathrm{Grp}\wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{-}X\right)=X\underset{\dot{}}{-}X$$
10	1 4 3	grpsubid	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X\underset{\dot{}}{-}X=\underset{\dot{}}{0}$$
11	10	adantrr	$$⊢\left(G\in \mathrm{Grp}\wedge \left(X\in B\wedge Y\in B\right)\right)\to X\underset{\dot{}}{-}X=\underset{\dot{}}{0}$$
12	9 11	eqtrd	$$⊢\left(G\in \mathrm{Grp}\wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{-}X\right)=\underset{\dot{}}{0}$$