Theorem mulgm1

Description: Group multiple (exponentiation) operation at negative one. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by Mario Carneiro, 20-Dec-2014)

	Ref	Expression
Hypotheses	mulgnncl.b	|- B = ( Base ` G )
	mulgnncl.t	|- .x. = ( .g ` G )
	mulgneg.i	|- I = ( invg ` G )
Assertion	mulgm1	|- ( ( G e. Grp /\ X e. B ) -> ( -u 1 .x. X ) = ( I ` 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		1z	|- 1 e. ZZ
5	1 2 3	mulgneg	|- ( ( G e. Grp /\ 1 e. ZZ /\ X e. B ) -> ( -u 1 .x. X ) = ( I ` ( 1 .x. X ) ) )
6	4 5	mp3an2	|- ( ( G e. Grp /\ X e. B ) -> ( -u 1 .x. X ) = ( I ` ( 1 .x. X ) ) )
7	1 2	mulg1	|- ( X e. B -> ( 1 .x. X ) = X )
8	7	adantl	|- ( ( G e. Grp /\ X e. B ) -> ( 1 .x. X ) = X )
9	8	fveq2d	|- ( ( G e. Grp /\ X e. B ) -> ( I ` ( 1 .x. X ) ) = ( I ` X ) )
10	6 9	eqtrd	|- ( ( G e. Grp /\ X e. B ) -> ( -u 1 .x. X ) = ( I ` X ) )