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.)

Step	Hyp	Ref	Expression
1		grpasscan1.1	$⊢ X = ran G$
2		grpasscan1.2	$⊢ N = inv (G)$
3	1 2	grpoinvcl	$⊢ (G \in GrpOp \land A \in X) \to N (A) \in X$
4		eqid	$⊢ GId (G) = GId (G)$
5	1 4 2	grporinv	$⊢ (G \in GrpOp \land N (A) \in X) \to N (A) G N (N (A)) = GId (G)$
6	3 5	syldan	$⊢ (G \in GrpOp \land A \in X) \to N (A) G N (N (A)) = GId (G)$
7	1 4 2	grpolinv	$⊢ (G \in GrpOp \land A \in X) \to N (A) G A = GId (G)$
8	6 7	eqtr4d	$⊢ (G \in GrpOp \land A \in X) \to N (A) G N (N (A)) = N (A) G A$
9	1 2	grpoinvcl	$⊢ (G \in GrpOp \land N (A) \in X) \to N (N (A)) \in X$
10	3 9	syldan	$⊢ (G \in GrpOp \land A \in X) \to N (N (A)) \in X$
11		simpr	$⊢ (G \in GrpOp \land A \in X) \to A \in X$
12	10 11 3	3jca	$⊢ (G \in GrpOp \land A \in X) \to (N (N (A)) \in X \land A \in X \land N (A) \in X)$
13	1	grpolcan	$⊢ (G \in GrpOp \land (N (N (A)) \in X \land A \in X \land N (A) \in X)) \to (N (A) G N (N (A)) = N (A) G A \leftrightarrow N (N (A)) = A)$
14	12 13	syldan	$⊢ (G \in GrpOp \land A \in X) \to (N (A) G N (N (A)) = N (A) G A \leftrightarrow N (N (A)) = A)$
15	8 14	mpbid	$⊢ (G \in GrpOp \land A \in X) \to N (N (A)) = A$

Metamath Proof Explorer