Theorem grpsubinv

Description: Subtraction of an inverse. (Contributed by NM, 7-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		grpsubinv.b	$$⊢B={\mathrm{Base}}_G$$
2		grpsubinv.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpsubinv.m	$$⊢\underset{\dot{}}{-}={-}_G$$
4		grpsubinv.n	$$⊢N={inv}_g\left(G\right)$$
5		grpsubinv.g	$$⊢\phi \to G\in \mathrm{Grp}$$
6		grpsubinv.x	$$⊢\phi \to X\in B$$
7		grpsubinv.y	$$⊢\phi \to Y\in B$$
8	1 4	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge Y\in B\right)\to N\left(Y\right)\in B$$
9	5 7 8	syl2anc	$$⊢\phi \to N\left(Y\right)\in B$$
10	1 2 4 3	grpsubval	$$⊢\left(X\in B\wedge N\left(Y\right)\in B\right)\to X\underset{\dot{}}{-}N\left(Y\right)=X\underset{\dot{}}{+}N\left(N\left(Y\right)\right)$$
11	6 9 10	syl2anc	$$⊢\phi \to X\underset{\dot{}}{-}N\left(Y\right)=X\underset{\dot{}}{+}N\left(N\left(Y\right)\right)$$
12	1 4	grpinvinv	$$⊢\left(G\in \mathrm{Grp}\wedge Y\in B\right)\to N\left(N\left(Y\right)\right)=Y$$
13	5 7 12	syl2anc	$$⊢\phi \to N\left(N\left(Y\right)\right)=Y$$
14	13	oveq2d	$$⊢\phi \to X\underset{\dot{}}{+}N\left(N\left(Y\right)\right)=X\underset{\dot{}}{+}Y$$
15	11 14	eqtrd	$$⊢\phi \to X\underset{\dot{}}{-}N\left(Y\right)=X\underset{\dot{}}{+}Y$$