This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpinvinv

Description: Double inverse law for groups. Lemma 2.2.1(c) of Herstein p. 55. (Contributed by NM, 31-Mar-2014)

Ref Expression
Hypotheses grpinvinv.b ⊢ B = Base G
grpinvinv.n ⊢ N = inv g ⁡ G
Assertion grpinvinv ⊢ G ∈ Grp ∧ X ∈ B → N ⁡ N ⁡ X = X

Proof

Step Hyp Ref Expression
1 grpinvinv.b ⊢ B = Base G
2 grpinvinv.n ⊢ N = inv g ⁡ G
3 1 2 grpinvcl ⊢ G ∈ Grp ∧ X ∈ B → N ⁡ X ∈ B
4 eqid ⊢ + G = + G
5 eqid ⊢ 0 G = 0 G
6 1 4 5 2 grprinv ⊢ G ∈ Grp ∧ N ⁡ X ∈ B → N ⁡ X + G N ⁡ N ⁡ X = 0 G
7 3 6 syldan ⊢ G ∈ Grp ∧ X ∈ B → N ⁡ X + G N ⁡ N ⁡ X = 0 G
8 1 4 5 2 grplinv ⊢ G ∈ Grp ∧ X ∈ B → N ⁡ X + G X = 0 G
9 7 8 eqtr4d ⊢ G ∈ Grp ∧ X ∈ B → N ⁡ X + G N ⁡ N ⁡ X = N ⁡ X + G X
10 simpl ⊢ G ∈ Grp ∧ X ∈ B → G ∈ Grp
11 1 2 grpinvcl ⊢ G ∈ Grp ∧ N ⁡ X ∈ B → N ⁡ N ⁡ X ∈ B
12 3 11 syldan ⊢ G ∈ Grp ∧ X ∈ B → N ⁡ N ⁡ X ∈ B
13 simpr ⊢ G ∈ Grp ∧ X ∈ B → X ∈ B
14 1 4 grplcan ⊢ G ∈ Grp ∧ N ⁡ N ⁡ X ∈ B ∧ X ∈ B ∧ N ⁡ X ∈ B → N ⁡ X + G N ⁡ N ⁡ X = N ⁡ X + G X ↔ N ⁡ N ⁡ X = X
15 10 12 13 3 14 syl13anc ⊢ G ∈ Grp ∧ X ∈ B → N ⁡ X + G N ⁡ N ⁡ X = N ⁡ X + G X ↔ N ⁡ N ⁡ X = X
16 9 15 mpbid ⊢ G ∈ Grp ∧ X ∈ B → N ⁡ N ⁡ X = X