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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mulginvcom.t	⊢ · = ( .g ‘ 𝐺 )
	mulginvcom.i	⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion	mulginvinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑁 · ( 𝐼 ‘ 𝑋 ) ) ) = ( 𝑁 · 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		mulginvcom.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mulginvcom.t	⊢ · = ( .g ‘ 𝐺 )
3		mulginvcom.i	⊢ 𝐼 = ( invg ‘ 𝐺 )
4	1 3	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 )
5	4	3adant2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 )
6	1 2 3	mulginvcom	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 ) → ( 𝑁 · ( 𝐼 ‘ ( 𝐼 ‘ 𝑋 ) ) ) = ( 𝐼 ‘ ( 𝑁 · ( 𝐼 ‘ 𝑋 ) ) ) )
7	5 6	syld3an3	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · ( 𝐼 ‘ ( 𝐼 ‘ 𝑋 ) ) ) = ( 𝐼 ‘ ( 𝑁 · ( 𝐼 ‘ 𝑋 ) ) ) )
8	1 3	grpinvinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝐼 ‘ 𝑋 ) ) = 𝑋 )
9	8	3adant2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝐼 ‘ 𝑋 ) ) = 𝑋 )
10	9	oveq2d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · ( 𝐼 ‘ ( 𝐼 ‘ 𝑋 ) ) ) = ( 𝑁 · 𝑋 ) )
11	7 10	eqtr3d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑁 · ( 𝐼 ‘ 𝑋 ) ) ) = ( 𝑁 · 𝑋 ) )