Theorem isgrpid2

Description: Properties showing that an element Z is the identity element of a group. (Contributed by NM, 7-Aug-2013)

	Ref	Expression
Hypotheses	grpinveu.b	$$⊢B={\mathrm{Base}}_G$$
	grpinveu.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpinveu.o	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	isgrpid2	$$⊢G\in \mathrm{Grp}\to \left(\left(Z\in B\wedge Z\underset{\dot{}}{+}Z=Z\right)\leftrightarrow \underset{\dot{}}{0}=Z\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	1 2 3	grpid	$$⊢\left(G\in \mathrm{Grp}\wedge Z\in B\right)\to \left(Z\underset{\dot{}}{+}Z=Z\leftrightarrow \underset{\dot{}}{0}=Z\right)$$
5	4	biimpd	$$⊢\left(G\in \mathrm{Grp}\wedge Z\in B\right)\to \left(Z\underset{\dot{}}{+}Z=Z\to \underset{\dot{}}{0}=Z\right)$$
6	5	expimpd	$$⊢G\in \mathrm{Grp}\to \left(\left(Z\in B\wedge Z\underset{\dot{}}{+}Z=Z\right)\to \underset{\dot{}}{0}=Z\right)$$
7	1 3	grpidcl	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}\in B$$
8	1 2 3	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge \underset{\dot{}}{0}\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
9	7 8	mpdan	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}\underset{\dot{}}{+}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
10	7 9	jca	$$⊢G\in \mathrm{Grp}\to \left(\underset{\dot{}}{0}\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{+}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)$$
11		eleq1	$$⊢\underset{\dot{}}{0}=Z\to \left(\underset{\dot{}}{0}\in B\leftrightarrow Z\in B\right)$$
12		id	$$⊢\underset{\dot{}}{0}=Z\to \underset{\dot{}}{0}=Z$$
13	12 12	oveq12d	$$⊢\underset{\dot{}}{0}=Z\to \underset{\dot{}}{0}\underset{\dot{}}{+}\underset{\dot{}}{0}=Z\underset{\dot{}}{+}Z$$
14	13 12	eqeq12d	$$⊢\underset{\dot{}}{0}=Z\to \left(\underset{\dot{}}{0}\underset{\dot{}}{+}\underset{\dot{}}{0}=\underset{\dot{}}{0}\leftrightarrow Z\underset{\dot{}}{+}Z=Z\right)$$
15	11 14	anbi12d	$$⊢\underset{\dot{}}{0}=Z\to \left(\left(\underset{\dot{}}{0}\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{+}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)\leftrightarrow \left(Z\in B\wedge Z\underset{\dot{}}{+}Z=Z\right)\right)$$
16	10 15	syl5ibcom	$$⊢G\in \mathrm{Grp}\to \left(\underset{\dot{}}{0}=Z\to \left(Z\in B\wedge Z\underset{\dot{}}{+}Z=Z\right)\right)$$
17	6 16	impbid	$$⊢G\in \mathrm{Grp}\to \left(\left(Z\in B\wedge Z\underset{\dot{}}{+}Z=Z\right)\leftrightarrow \underset{\dot{}}{0}=Z\right)$$