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 ⊢ · ˙ = ⋅ G
mulginvcom.i ⊢ I = inv g ⁡ G
Assertion mulginvinv ⊢ G ∈ Grp ∧ N ∈ ℤ ∧ X ∈ B → I ⁡ N · ˙ I ⁡ X = N · ˙ X

Proof

Step Hyp Ref Expression
1 mulginvcom.b ⊢ B = Base G
2 mulginvcom.t ⊢ · ˙ = ⋅ G
3 mulginvcom.i ⊢ I = inv g ⁡ G
4 1 3 grpinvcl ⊢ G ∈ Grp ∧ X ∈ B → I ⁡ X ∈ B
5 4 3adant2 ⊢ G ∈ Grp ∧ N ∈ ℤ ∧ X ∈ B → I ⁡ X ∈ B
6 1 2 3 mulginvcom ⊢ G ∈ Grp ∧ N ∈ ℤ ∧ I ⁡ X ∈ B → N · ˙ I ⁡ I ⁡ X = I ⁡ N · ˙ I ⁡ X
7 5 6 syld3an3 ⊢ G ∈ Grp ∧ N ∈ ℤ ∧ X ∈ B → N · ˙ I ⁡ I ⁡ X = I ⁡ N · ˙ I ⁡ X
8 1 3 grpinvinv ⊢ G ∈ Grp ∧ X ∈ B → I ⁡ I ⁡ X = X
9 8 3adant2 ⊢ G ∈ Grp ∧ N ∈ ℤ ∧ X ∈ B → I ⁡ I ⁡ X = X
10 9 oveq2d ⊢ G ∈ Grp ∧ N ∈ ℤ ∧ X ∈ B → N · ˙ I ⁡ I ⁡ X = N · ˙ X
11 7 10 eqtr3d ⊢ G ∈ Grp ∧ N ∈ ℤ ∧ X ∈ B → I ⁡ N · ˙ I ⁡ X = N · ˙ X