This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )