Theorem ablsubsub4

Description: Law for double subtraction. (Contributed by NM, 7-Apr-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$$
Assertion	ablsubsub4	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}Z=X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)$$

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		ablgrp	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{Grp}$$
9	4 8	syl	$$⊢\phi \to G\in \mathrm{Grp}$$
10	1 3	grpsubcl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y\in B$$
11	9 5 6 10	syl3anc	$$⊢\phi \to X\underset{\dot{}}{-}Y\in B$$
12		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
13	1 2 12 3	grpsubval	$$⊢\left(X\underset{\dot{}}{-}Y\in B\wedge Z\in B\right)\to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}Z=\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{+}{inv}_g\left(G\right)\left(Z\right)$$
14	11 7 13	syl2anc	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}Z=\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{+}{inv}_g\left(G\right)\left(Z\right)$$
15	1 12	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge Z\in B\right)\to {inv}_g\left(G\right)\left(Z\right)\in B$$
16	9 7 15	syl2anc	$$⊢\phi \to {inv}_g\left(G\right)\left(Z\right)\in B$$
17	1 2 3 4 5 6 16	ablsubsub	$$⊢\phi \to X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{-}{inv}_g\left(G\right)\left(Z\right)\right)=\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{+}{inv}_g\left(G\right)\left(Z\right)$$
18	1 2 3 12 9 6 7	grpsubinv	$$⊢\phi \to Y\underset{\dot{}}{-}{inv}_g\left(G\right)\left(Z\right)=Y\underset{\dot{}}{+}Z$$
19	18	oveq2d	$$⊢\phi \to X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{-}{inv}_g\left(G\right)\left(Z\right)\right)=X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)$$
20	14 17 19	3eqtr2d	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}Z=X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)$$