Metamath Proof Explorer

Theorem grpo2inv

Description: Double inverse law for groups. Lemma 2.2.1(c) of Herstein p. 55. (Contributed by NM, 27-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypotheses grpasscan1.1 ⊢ X = ran ⁡ G
grpasscan1.2 ⊢ N = inv ⁡ G
Assertion grpo2inv ⊢ G ∈ GrpOp ∧ A ∈ X → N ⁡ N ⁡ A = A

Proof

Step Hyp Ref Expression
1 grpasscan1.1 ⊢ X = ran ⁡ G
2 grpasscan1.2 ⊢ N = inv ⁡ G
3 1 2 grpoinvcl ⊢ G ∈ GrpOp ∧ A ∈ X → N ⁡ A ∈ X
4 eqid ⊢ GId ⁡ G = GId ⁡ G
5 1 4 2 grporinv ⊢ G ∈ GrpOp ∧ N ⁡ A ∈ X → N ⁡ A G N ⁡ N ⁡ A = GId ⁡ G
6 3 5 syldan ⊢ G ∈ GrpOp ∧ A ∈ X → N ⁡ A G N ⁡ N ⁡ A = GId ⁡ G
7 1 4 2 grpolinv ⊢ G ∈ GrpOp ∧ A ∈ X → N ⁡ A G A = GId ⁡ G
8 6 7 eqtr4d ⊢ G ∈ GrpOp ∧ A ∈ X → N ⁡ A G N ⁡ N ⁡ A = N ⁡ A G A
9 1 2 grpoinvcl ⊢ G ∈ GrpOp ∧ N ⁡ A ∈ X → N ⁡ N ⁡ A ∈ X
10 3 9 syldan ⊢ G ∈ GrpOp ∧ A ∈ X → N ⁡ N ⁡ A ∈ X
11 simpr ⊢ G ∈ GrpOp ∧ A ∈ X → A ∈ X
12 10 11 3 3jca ⊢ G ∈ GrpOp ∧ A ∈ X → N ⁡ N ⁡ A ∈ X ∧ A ∈ X ∧ N ⁡ A ∈ X
13 1 grpolcan ⊢ G ∈ GrpOp ∧ N ⁡ N ⁡ A ∈ X ∧ A ∈ X ∧ N ⁡ A ∈ X → N ⁡ A G N ⁡ N ⁡ A = N ⁡ A G A ↔ N ⁡ N ⁡ A = A
14 12 13 syldan ⊢ G ∈ GrpOp ∧ A ∈ X → N ⁡ A G N ⁡ N ⁡ A = N ⁡ A G A ↔ N ⁡ N ⁡ A = A
15 8 14 mpbid ⊢ G ∈ GrpOp ∧ A ∈ X → N ⁡ N ⁡ A = A