grpinvid

Description: The inverse of the identity element of a group. (Contributed by NM, 24-Aug-2011)

	Ref	Expression
Hypotheses	grpinvid.u	$⊢ \underset{˙}{0} = 0_{G}$
	grpinvid.n	$⊢ N = {inv}_{g} (G)$
Assertion	grpinvid	$⊢ G \in Grp \to N (\underset{˙}{0}) = \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		grpinvid.u	$⊢ \underset{˙}{0} = 0_{G}$
2		grpinvid.n	$⊢ N = {inv}_{g} (G)$
3		eqid	$⊢ {Base}_{G} = {Base}_{G}$
4	3 1	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in {Base}_{G}$
5		eqid	$⊢ +_{G} = +_{G}$
6	3 5 1	grplid	$⊢ (G \in Grp \land \underset{˙}{0} \in {Base}_{G}) \to \underset{˙}{0} +_{G} \underset{˙}{0} = \underset{˙}{0}$
7	4 6	mpdan	$⊢ G \in Grp \to \underset{˙}{0} +_{G} \underset{˙}{0} = \underset{˙}{0}$
8	3 5 1 2	grpinvid1	$⊢ (G \in Grp \land \underset{˙}{0} \in {Base}_{G} \land \underset{˙}{0} \in {Base}_{G}) \to (N (\underset{˙}{0}) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} +_{G} \underset{˙}{0} = \underset{˙}{0})$
9	4 4 8	mpd3an23	$⊢ G \in Grp \to (N (\underset{˙}{0}) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} +_{G} \underset{˙}{0} = \underset{˙}{0})$
10	7 9	mpbird	$⊢ G \in Grp \to N (\underset{˙}{0}) = \underset{˙}{0}$

Metamath Proof Explorer