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 = ( invg ` G )
Assertion grpinvinv 
|- ( ( G e. Grp /\ X e. B ) -> ( N ` ( N ` X ) ) = X )

Proof

Step Hyp Ref Expression
1 grpinvinv.b 
 |-  B = ( Base ` G )
2 grpinvinv.n 
 |-  N = ( invg ` G )
3 1 2 grpinvcl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )
4 eqid 
 |-  ( +g ` G ) = ( +g ` G )
5 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
6 1 4 5 2 grprinv 
 |-  ( ( G e. Grp /\ ( N ` X ) e. B ) -> ( ( N ` X ) ( +g ` G ) ( N ` ( N ` X ) ) ) = ( 0g ` G ) )
7 3 6 syldan 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( N ` X ) ( +g ` G ) ( N ` ( N ` X ) ) ) = ( 0g ` G ) )
8 1 4 5 2 grplinv 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( N ` X ) ( +g ` G ) X ) = ( 0g ` G ) )
9 7 8 eqtr4d 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( N ` X ) ( +g ` G ) ( N ` ( N ` X ) ) ) = ( ( N ` X ) ( +g ` G ) X ) )
10 simpl 
 |-  ( ( G e. Grp /\ X e. B ) -> G e. Grp )
11 1 2 grpinvcl 
 |-  ( ( G e. Grp /\ ( N ` X ) e. B ) -> ( N ` ( N ` X ) ) e. B )
12 3 11 syldan 
 |-  ( ( G e. Grp /\ X e. B ) -> ( N ` ( N ` X ) ) e. B )
13 simpr 
 |-  ( ( G e. Grp /\ X e. B ) -> X e. B )
14 1 4 grplcan 
 |-  ( ( G e. Grp /\ ( ( N ` ( N ` X ) ) e. B /\ X e. B /\ ( N ` X ) e. B ) ) -> ( ( ( N ` X ) ( +g ` G ) ( N ` ( N ` X ) ) ) = ( ( N ` X ) ( +g ` G ) X ) <-> ( N ` ( N ` X ) ) = X ) )
15 10 12 13 3 14 syl13anc 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( ( N ` X ) ( +g ` G ) ( N ` ( N ` X ) ) ) = ( ( N ` X ) ( +g ` G ) X ) <-> ( N ` ( N ` X ) ) = X ) )
16 9 15 mpbid 
 |-  ( ( G e. Grp /\ X e. B ) -> ( N ` ( N ` X ) ) = X )