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 ⊢ 𝐵 = ( 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 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑁 · ( 𝐼 ‘ 𝑋 ) ) ) = ( 𝑁 · 𝑋 ) )