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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
grpinvinv.n ⊢ 𝑁 = ( invg ‘ 𝐺 )
Assertion grpinvinv ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 grpinvinv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 grpinvinv.n ⊢ 𝑁 = ( invg ‘ 𝐺 )
3 1 2 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
4 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
5 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6 1 4 5 2 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑋 ) ( +g ‘ 𝐺 ) ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) ) = ( 0g ‘ 𝐺 ) )
7 3 6 syldan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑋 ) ( +g ‘ 𝐺 ) ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) ) = ( 0g ‘ 𝐺 ) )
8 1 4 5 2 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) = ( 0g ‘ 𝐺 ) )
9 7 8 eqtr4d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑋 ) ( +g ‘ 𝐺 ) ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) ) = ( ( 𝑁 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) )
10 simpl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → 𝐺 ∈ Grp )
11 1 2 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) ∈ 𝐵 )
12 3 11 syldan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) ∈ 𝐵 )
13 simpr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
14 1 4 grplcan ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 ) ) → ( ( ( 𝑁 ‘ 𝑋 ) ( +g ‘ 𝐺 ) ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) ) = ( ( 𝑁 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) ↔ ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 ) )
15 10 12 13 3 14 syl13anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 𝑁 ‘ 𝑋 ) ( +g ‘ 𝐺 ) ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) ) = ( ( 𝑁 ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) ↔ ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 ) )
16 9 15 mpbid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )