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 e. GrpOp /\ A e. 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 e. GrpOp /\ A e. X ) -> ( N ` A ) e. X )
4		eqid	|- ( GId ` G ) = ( GId ` G )
5	1 4 2	grporinv	|- ( ( G e. GrpOp /\ ( N ` A ) e. X ) -> ( ( N ` A ) G ( N ` ( N ` A ) ) ) = ( GId ` G ) )
6	3 5	syldan	|- ( ( G e. GrpOp /\ A e. X ) -> ( ( N ` A ) G ( N ` ( N ` A ) ) ) = ( GId ` G ) )
7	1 4 2	grpolinv	|- ( ( G e. GrpOp /\ A e. X ) -> ( ( N ` A ) G A ) = ( GId ` G ) )
8	6 7	eqtr4d	|- ( ( G e. GrpOp /\ A e. X ) -> ( ( N ` A ) G ( N ` ( N ` A ) ) ) = ( ( N ` A ) G A ) )
9	1 2	grpoinvcl	|- ( ( G e. GrpOp /\ ( N ` A ) e. X ) -> ( N ` ( N ` A ) ) e. X )
10	3 9	syldan	|- ( ( G e. GrpOp /\ A e. X ) -> ( N ` ( N ` A ) ) e. X )
11		simpr	|- ( ( G e. GrpOp /\ A e. X ) -> A e. X )
12	10 11 3	3jca	|- ( ( G e. GrpOp /\ A e. X ) -> ( ( N ` ( N ` A ) ) e. X /\ A e. X /\ ( N ` A ) e. X ) )
13	1	grpolcan	|- ( ( G e. GrpOp /\ ( ( N ` ( N ` A ) ) e. X /\ A e. X /\ ( N ` A ) e. X ) ) -> ( ( ( N ` A ) G ( N ` ( N ` A ) ) ) = ( ( N ` A ) G A ) <-> ( N ` ( N ` A ) ) = A ) )
14	12 13	syldan	|- ( ( G e. GrpOp /\ A e. X ) -> ( ( ( N ` A ) G ( N ` ( N ` A ) ) ) = ( ( N ` A ) G A ) <-> ( N ` ( N ` A ) ) = A ) )
15	8 14	mpbid	|- ( ( G e. GrpOp /\ A e. X ) -> ( N ` ( N ` A ) ) = A )