Theorem ablsub2inv

Description: Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015)

	Ref	Expression
Hypotheses	ablsub2inv.b	$$⊢B={\mathrm{Base}}_G$$
	ablsub2inv.m	$$⊢\underset{\dot{}}{-}={-}_G$$
	ablsub2inv.n	$$⊢N={inv}_g\left(G\right)$$
	ablsub2inv.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	ablsub2inv.x	$$⊢\phi \to X\in B$$
	ablsub2inv.y	$$⊢\phi \to Y\in B$$
Assertion	ablsub2inv	$$⊢\phi \to N\left(X\right)\underset{\dot{}}{-}N\left(Y\right)=Y\underset{\dot{}}{-}X$$

Proof

Step	Hyp	Ref	Expression
1		ablsub2inv.b	$$⊢B={\mathrm{Base}}_G$$
2		ablsub2inv.m	$$⊢\underset{\dot{}}{-}={-}_G$$
3		ablsub2inv.n	$$⊢N={inv}_g\left(G\right)$$
4		ablsub2inv.g	$$⊢\phi \to G\in \mathrm{Abel}$$
5		ablsub2inv.x	$$⊢\phi \to X\in B$$
6		ablsub2inv.y	$$⊢\phi \to Y\in B$$
7		eqid	$$⊢{+}_G={+}_G$$
8		ablgrp	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{Grp}$$
9	4 8	syl	$$⊢\phi \to G\in \mathrm{Grp}$$
10	1 3	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)\in B$$
11	9 5 10	syl2anc	$$⊢\phi \to N\left(X\right)\in B$$
12	1 7 2 3 9 11 6	grpsubinv	$$⊢\phi \to N\left(X\right)\underset{\dot{}}{-}N\left(Y\right)=N\left(X\right){+}_{G}Y$$
13	1 7	ablcom	$$⊢\left(G\in \mathrm{Abel}\wedge N\left(X\right)\in B\wedge Y\in B\right)\to N\left(X\right){+}_{G}Y=Y{+}_{G}N\left(X\right)$$
14	4 11 6 13	syl3anc	$$⊢\phi \to N\left(X\right){+}_{G}Y=Y{+}_{G}N\left(X\right)$$
15	1 3	grpinvinv	$$⊢\left(G\in \mathrm{Grp}\wedge Y\in B\right)\to N\left(N\left(Y\right)\right)=Y$$
16	9 6 15	syl2anc	$$⊢\phi \to N\left(N\left(Y\right)\right)=Y$$
17	16	oveq1d	$$⊢\phi \to N\left(N\left(Y\right)\right){+}_{G}N\left(X\right)=Y{+}_{G}N\left(X\right)$$
18	14 17	eqtr4d	$$⊢\phi \to N\left(X\right){+}_{G}Y=N\left(N\left(Y\right)\right){+}_{G}N\left(X\right)$$
19	1 3	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge Y\in B\right)\to N\left(Y\right)\in B$$
20	9 6 19	syl2anc	$$⊢\phi \to N\left(Y\right)\in B$$
21	1 7 3	grpinvadd	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge N\left(Y\right)\in B\right)\to N\left(X{+}_{G}N\left(Y\right)\right)=N\left(N\left(Y\right)\right){+}_{G}N\left(X\right)$$
22	9 5 20 21	syl3anc	$$⊢\phi \to N\left(X{+}_{G}N\left(Y\right)\right)=N\left(N\left(Y\right)\right){+}_{G}N\left(X\right)$$
23	18 22	eqtr4d	$$⊢\phi \to N\left(X\right){+}_{G}Y=N\left(X{+}_{G}N\left(Y\right)\right)$$
24	1 7 3 2	grpsubval	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y=X{+}_{G}N\left(Y\right)$$
25	5 6 24	syl2anc	$$⊢\phi \to X\underset{\dot{}}{-}Y=X{+}_{G}N\left(Y\right)$$
26	25	fveq2d	$$⊢\phi \to N\left(X\underset{\dot{}}{-}Y\right)=N\left(X{+}_{G}N\left(Y\right)\right)$$
27	23 26	eqtr4d	$$⊢\phi \to N\left(X\right){+}_{G}Y=N\left(X\underset{\dot{}}{-}Y\right)$$
28	1 2 3	grpinvsub	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to N\left(X\underset{\dot{}}{-}Y\right)=Y\underset{\dot{}}{-}X$$
29	9 5 6 28	syl3anc	$$⊢\phi \to N\left(X\underset{\dot{}}{-}Y\right)=Y\underset{\dot{}}{-}X$$
30	12 27 29	3eqtrd	$$⊢\phi \to N\left(X\right)\underset{\dot{}}{-}N\left(Y\right)=Y\underset{\dot{}}{-}X$$