Theorem mulgnegneg

Description: The inverse of a negative group multiple is the positive group multiple. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 30-Aug-2021)

	Ref	Expression
Hypotheses	mulgnncl.b	|- B = ( Base ` G )
	mulgnncl.t	|- .x. = ( .g ` G )
	mulgneg.i	|- I = ( invg ` G )
Assertion	mulgnegneg	|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( I ` ( -u N .x. X ) ) = ( N .x. X ) )

Proof

Step	Hyp	Ref	Expression
1		mulgnncl.b	|- B = ( Base ` G )
2		mulgnncl.t	|- .x. = ( .g ` G )
3		mulgneg.i	|- I = ( invg ` G )
4	1 2 3	mulgneg	|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) )
5	4	fveq2d	|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( I ` ( -u N .x. X ) ) = ( I ` ( I ` ( N .x. X ) ) ) )
6		simp1	|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> G e. Grp )
7	1 2	mulgcl	|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N .x. X ) e. B )
8	1 3	grpinvinv	|- ( ( G e. Grp /\ ( N .x. X ) e. B ) -> ( I ` ( I ` ( N .x. X ) ) ) = ( N .x. X ) )
9	6 7 8	syl2anc	|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( I ` ( I ` ( N .x. X ) ) ) = ( N .x. X ) )
10	5 9	eqtrd	|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( I ` ( -u N .x. X ) ) = ( N .x. X ) )