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	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
		mulginvcom.i	$⊢ I = {inv}_{g} (G)$
	Assertion	mulginvinv	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to I (N \underset{˙}{\cdot} I (X)) = N \underset{˙}{\cdot} X$

Proof

Step	Hyp	Ref	Expression
1		mulginvcom.b	$⊢ B = {Base}_{G}$
2		mulginvcom.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulginvcom.i	$⊢ I = {inv}_{g} (G)$
4	1 3	grpinvcl	$⊢ (G \in Grp \land X \in B) \to I (X) \in B$
5	4	3adant2	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to I (X) \in B$
6	1 2 3	mulginvcom	$⊢ (G \in Grp \land N \in ℤ \land I (X) \in B) \to N \underset{˙}{\cdot} I (I (X)) = I (N \underset{˙}{\cdot} I (X))$
7	5 6	syld3an3	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to N \underset{˙}{\cdot} I (I (X)) = I (N \underset{˙}{\cdot} I (X))$
8	1 3	grpinvinv	$⊢ (G \in Grp \land X \in B) \to I (I (X)) = X$
9	8	3adant2	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to I (I (X)) = X$
10	9	oveq2d	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to N \underset{˙}{\cdot} I (I (X)) = N \underset{˙}{\cdot} X$
11	7 10	eqtr3d	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to I (N \underset{˙}{\cdot} I (X)) = N \underset{˙}{\cdot} X$