grpinvinv

Description: Double inverse law for groups. Lemma 2.2.1(c) of Herstein p. 55. (Contributed by NM, 31-Mar-2014)

Step	Hyp	Ref	Expression
1		grpinvinv.b	$⊢ B = {Base}_{G}$
2		grpinvinv.n	$⊢ N = {inv}_{g} (G)$
3	1 2	grpinvcl	$⊢ (G \in Grp \land X \in B) \to N (X) \in B$
4		eqid	$⊢ +_{G} = +_{G}$
5		eqid	$⊢ 0_{G} = 0_{G}$
6	1 4 5 2	grprinv	$⊢ (G \in Grp \land N (X) \in B) \to N (X) +_{G} N (N (X)) = 0_{G}$
7	3 6	syldan	$⊢ (G \in Grp \land X \in B) \to N (X) +_{G} N (N (X)) = 0_{G}$
8	1 4 5 2	grplinv	$⊢ (G \in Grp \land X \in B) \to N (X) +_{G} X = 0_{G}$
9	7 8	eqtr4d	$⊢ (G \in Grp \land X \in B) \to N (X) +_{G} N (N (X)) = N (X) +_{G} X$
10		simpl	$⊢ (G \in Grp \land X \in B) \to G \in Grp$
11	1 2	grpinvcl	$⊢ (G \in Grp \land N (X) \in B) \to N (N (X)) \in B$
12	3 11	syldan	$⊢ (G \in Grp \land X \in B) \to N (N (X)) \in B$
13		simpr	$⊢ (G \in Grp \land X \in B) \to X \in B$
14	1 4	grplcan	$⊢ (G \in Grp \land (N (N (X)) \in B \land X \in B \land N (X) \in B)) \to (N (X) +_{G} N (N (X)) = N (X) +_{G} X \leftrightarrow N (N (X)) = X)$
15	10 12 13 3 14	syl13anc	$⊢ (G \in Grp \land X \in B) \to (N (X) +_{G} N (N (X)) = N (X) +_{G} X \leftrightarrow N (N (X)) = X)$
16	9 15	mpbid	$⊢ (G \in Grp \land X \in B) \to N (N (X)) = X$

Metamath Proof Explorer