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 = {Base}_{G}$
	grpsubcl.m	$⊢ \underset{˙}{-} = -_{G}$
	grpinvsub.n	$⊢ N = {inv}_{g} (G)$
	grpinvval2.z	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	grpinvval2	$⊢ (G \in Grp \land X \in B) \to N (X) = \underset{˙}{0} \underset{˙}{-} X$

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

Metamath Proof Explorer