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