Theorem grpinvid

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

	Ref	Expression
Hypotheses	grpinvid.u	$$⊢\underset{\dot{}}{0}=0_G$$
	grpinvid.n	$$⊢N={inv}_g\left(G\right)$$
Assertion	grpinvid	$$⊢G\in \mathrm{Grp}\to N\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$

Proof

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