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

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 ⊢ 𝑋 = ran 𝐺
grpasscan1.2 ⊢ 𝑁 = ( inv ‘ 𝐺 )
Assertion grpo2inv ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝐴 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 grpasscan1.1 ⊢ 𝑋 = ran 𝐺
2 grpasscan1.2 ⊢ 𝑁 = ( inv ‘ 𝐺 )
3 1 2 grpoinvcl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 )
4 eqid ⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
5 1 4 2 grporinv ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) 𝐺 ( 𝑁 ‘ ( 𝑁 ‘ 𝐴 ) ) ) = ( GId ‘ 𝐺 ) )
6 3 5 syldan ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) 𝐺 ( 𝑁 ‘ ( 𝑁 ‘ 𝐴 ) ) ) = ( GId ‘ 𝐺 ) )
7 1 4 2 grpolinv ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) = ( GId ‘ 𝐺 ) )
8 6 7 eqtr4d ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) 𝐺 ( 𝑁 ‘ ( 𝑁 ‘ 𝐴 ) ) ) = ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) )
9 1 2 grpoinvcl ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝐴 ) ) ∈ 𝑋 )
10 3 9 syldan ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝐴 ) ) ∈ 𝑋 )
11 simpr ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
12 10 11 3 3jca ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝑁 ‘ 𝐴 ) ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 ) )
13 1 grpolcan ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝑁 ‘ ( 𝑁 ‘ 𝐴 ) ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 ) ) → ( ( ( 𝑁 ‘ 𝐴 ) 𝐺 ( 𝑁 ‘ ( 𝑁 ‘ 𝐴 ) ) ) = ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) ↔ ( 𝑁 ‘ ( 𝑁 ‘ 𝐴 ) ) = 𝐴 ) )
14 12 13 syldan ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ 𝐴 ) 𝐺 ( 𝑁 ‘ ( 𝑁 ‘ 𝐴 ) ) ) = ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) ↔ ( 𝑁 ‘ ( 𝑁 ‘ 𝐴 ) ) = 𝐴 ) )
15 8 14 mpbid ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝐴 ) ) = 𝐴 )