Theorem grpinvval2

Description: A df-neg -like equation for inverse in terms of group subtraction. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	grpsubcl.b	$$⊢B={\mathrm{Base}}_G$$
	grpsubcl.m	$$⊢\underset{\dot{}}{-}={-}_G$$
	grpinvsub.n	$$⊢N={inv}_g\left(G\right)$$
	grpinvval2.z	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	grpinvval2	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)=\underset{\dot{}}{0}\underset{\dot{}}{-}X$$

Proof

Step	Hyp	Ref	Expression
1		grpsubcl.b	$$⊢B={\mathrm{Base}}_G$$
2		grpsubcl.m	$$⊢\underset{\dot{}}{-}={-}_G$$
3		grpinvsub.n	$$⊢N={inv}_g\left(G\right)$$
4		grpinvval2.z	$$⊢\underset{\dot{}}{0}=0_G$$
5	1 4	grpidcl	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}\in B$$
6		eqid	$$⊢{+}_G={+}_G$$
7	1 6 3 2	grpsubval	$$⊢\left(\underset{\dot{}}{0}\in B\wedge X\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{-}X=\underset{\dot{}}{0}{+}_{G}N\left(X\right)$$
8	5 7	sylan	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{-}X=\underset{\dot{}}{0}{+}_{G}N\left(X\right)$$
9	1 3	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)\in B$$
10	1 6 4	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge N\left(X\right)\in B\right)\to \underset{\dot{}}{0}{+}_{G}N\left(X\right)=N\left(X\right)$$
11	9 10	syldan	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \underset{\dot{}}{0}{+}_{G}N\left(X\right)=N\left(X\right)$$
12	8 11	eqtr2d	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)=\underset{\dot{}}{0}\underset{\dot{}}{-}X$$