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 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )