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 = ( Base ` G )
	grpsubcl.m	|- .- = ( -g ` G )
	grpinvsub.n	|- N = ( invg ` G )
	grpinvval2.z	|- .0. = ( 0g ` G )
Assertion	grpinvval2	|- ( ( G e. Grp /\ X e. B ) -> ( N ` X ) = ( .0. .- X ) )

Proof

Step	Hyp	Ref	Expression
1		grpsubcl.b	|- B = ( Base ` G )
2		grpsubcl.m	|- .- = ( -g ` G )
3		grpinvsub.n	|- N = ( invg ` G )
4		grpinvval2.z	|- .0. = ( 0g ` G )
5	1 4	grpidcl	|- ( G e. Grp -> .0. e. B )
6		eqid	|- ( +g ` G ) = ( +g ` G )
7	1 6 3 2	grpsubval	|- ( ( .0. e. B /\ X e. B ) -> ( .0. .- X ) = ( .0. ( +g ` G ) ( N ` X ) ) )
8	5 7	sylan	|- ( ( G e. Grp /\ X e. B ) -> ( .0. .- X ) = ( .0. ( +g ` G ) ( N ` X ) ) )
9	1 3	grpinvcl	|- ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )
10	1 6 4	grplid	|- ( ( G e. Grp /\ ( N ` X ) e. B ) -> ( .0. ( +g ` G ) ( N ` X ) ) = ( N ` X ) )
11	9 10	syldan	|- ( ( G e. Grp /\ X e. B ) -> ( .0. ( +g ` G ) ( N ` X ) ) = ( N ` X ) )
12	8 11	eqtr2d	|- ( ( G e. Grp /\ X e. B ) -> ( N ` X ) = ( .0. .- X ) )