Theorem grpsubid

Description: Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014)

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

Proof

Step	Hyp	Ref	Expression
1		grpsubid.b	$$⊢B={\mathrm{Base}}_G$$
2		grpsubid.o	$$⊢\underset{\dot{}}{0}=0_G$$
3		grpsubid.m	$$⊢\underset{\dot{}}{-}={-}_G$$
4		eqid	$$⊢{+}_G={+}_G$$
5		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
6	1 4 5 3	grpsubval	$$⊢\left(X\in B\wedge X\in B\right)\to X\underset{\dot{}}{-}X=X{+}_G{inv}_g\left(G\right)\left(X\right)$$
7	6	anidms	$$⊢X\in B\to X\underset{\dot{}}{-}X=X{+}_G{inv}_g\left(G\right)\left(X\right)$$
8	7	adantl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X\underset{\dot{}}{-}X=X{+}_G{inv}_g\left(G\right)\left(X\right)$$
9	1 4 2 5	grprinv	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X{+}_G{inv}_g\left(G\right)\left(X\right)=\underset{\dot{}}{0}$$
10	8 9	eqtrd	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X\underset{\dot{}}{-}X=\underset{\dot{}}{0}$$