Theorem grpsubid1

Description: Subtraction of the identity from a group element. (Contributed by Mario Carneiro, 14-Jan-2015)

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

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		id	$$⊢X\in B\to X\in B$$
5	1 2	grpidcl	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}\in B$$
6		eqid	$$⊢{+}_G={+}_G$$
7		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
8	1 6 7 3	grpsubval	$$⊢\left(X\in B\wedge \underset{\dot{}}{0}\in B\right)\to X\underset{\dot{}}{-}\underset{\dot{}}{0}=X{+}_G{inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)$$
9	4 5 8	syl2anr	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X\underset{\dot{}}{-}\underset{\dot{}}{0}=X{+}_G{inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)$$
10	2 7	grpinvid	$$⊢G\in \mathrm{Grp}\to {inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
11	10	adantr	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to {inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
12	11	oveq2d	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X{+}_G{inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)=X{+}_G\underset{\dot{}}{0}$$
13	1 6 2	grprid	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X{+}_G\underset{\dot{}}{0}=X$$
14	9 12 13	3eqtrd	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X\underset{\dot{}}{-}\underset{\dot{}}{0}=X$$