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

Metamath Proof Explorer

Theorem mulginvinv

Description: The group multiple operator commutes with the group inverse function. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 31-Aug-2021)

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

Proof

Step Hyp Ref Expression
1 mulginvcom.b 
 |-  B = ( Base ` G )
2 mulginvcom.t 
 |-  .x. = ( .g ` G )
3 mulginvcom.i 
 |-  I = ( invg ` G )
4 1 3 grpinvcl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( I ` X ) e. B )
5 4 3adant2 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( I ` X ) e. B )
6 1 2 3 mulginvcom 
 |-  ( ( G e. Grp /\ N e. ZZ /\ ( I ` X ) e. B ) -> ( N .x. ( I ` ( I ` X ) ) ) = ( I ` ( N .x. ( I ` X ) ) ) )
7 5 6 syld3an3 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N .x. ( I ` ( I ` X ) ) ) = ( I ` ( N .x. ( I ` X ) ) ) )
8 1 3 grpinvinv 
 |-  ( ( G e. Grp /\ X e. B ) -> ( I ` ( I ` X ) ) = X )
9 8 3adant2 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( I ` ( I ` X ) ) = X )
10 9 oveq2d 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N .x. ( I ` ( I ` X ) ) ) = ( N .x. X ) )
11 7 10 eqtr3d 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( I ` ( N .x. ( I ` X ) ) ) = ( N .x. X ) )