Theorem grpid

Description: Two ways of saying that an element of a group is the identity element. Provides a convenient way to compute the value of the identity element. (Contributed by NM, 24-Aug-2011)

	Ref	Expression
Hypotheses	grpinveu.b	$$⊢B={\mathrm{Base}}_G$$
	grpinveu.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpinveu.o	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	grpid	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \left(X\underset{\dot{}}{+}X=X\leftrightarrow \underset{\dot{}}{0}=X\right)$$

Proof

Step	Hyp	Ref	Expression
1		grpinveu.b	$$⊢B={\mathrm{Base}}_G$$
2		grpinveu.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpinveu.o	$$⊢\underset{\dot{}}{0}=0_G$$
4		eqcom	$$⊢\underset{\dot{}}{0}=X\leftrightarrow X=\underset{\dot{}}{0}$$
5	1 3	grpidcl	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}\in B$$
6	1 2	grprcan	$$⊢\left(G\in \mathrm{Grp}\wedge \left(X\in B\wedge \underset{\dot{}}{0}\in B\wedge X\in B\right)\right)\to \left(X\underset{\dot{}}{+}X=\underset{\dot{}}{0}\underset{\dot{}}{+}X\leftrightarrow X=\underset{\dot{}}{0}\right)$$
7	6	3exp2	$$⊢G\in \mathrm{Grp}\to \left(X\in B\to \left(\underset{\dot{}}{0}\in B\to \left(X\in B\to \left(X\underset{\dot{}}{+}X=\underset{\dot{}}{0}\underset{\dot{}}{+}X\leftrightarrow X=\underset{\dot{}}{0}\right)\right)\right)\right)$$
8	5 7	mpid	$$⊢G\in \mathrm{Grp}\to \left(X\in B\to \left(X\in B\to \left(X\underset{\dot{}}{+}X=\underset{\dot{}}{0}\underset{\dot{}}{+}X\leftrightarrow X=\underset{\dot{}}{0}\right)\right)\right)$$
9	8	pm2.43d	$$⊢G\in \mathrm{Grp}\to \left(X\in B\to \left(X\underset{\dot{}}{+}X=\underset{\dot{}}{0}\underset{\dot{}}{+}X\leftrightarrow X=\underset{\dot{}}{0}\right)\right)$$
10	9	imp	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \left(X\underset{\dot{}}{+}X=\underset{\dot{}}{0}\underset{\dot{}}{+}X\leftrightarrow X=\underset{\dot{}}{0}\right)$$
11	1 2 3	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}X=X$$
12	11	eqeq2d	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \left(X\underset{\dot{}}{+}X=\underset{\dot{}}{0}\underset{\dot{}}{+}X\leftrightarrow X\underset{\dot{}}{+}X=X\right)$$
13	10 12	bitr3d	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \left(X=\underset{\dot{}}{0}\leftrightarrow X\underset{\dot{}}{+}X=X\right)$$
14	4 13	syl5rbb	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \left(X\underset{\dot{}}{+}X=X\leftrightarrow \underset{\dot{}}{0}=X\right)$$