Theorem 0gisid

Description: In a structure with an identity element, the group identity element is an identity element of the structure. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by Mario Carneiro, 23-Dec-2013) (Revised by AV, 11-Aug-2026)

	Ref	Expression
Hypotheses	ismgmid.b	$$⊢B={\mathrm{Base}}_G$$
	ismgmid.o	$$⊢\underset{\dot{}}{0}=0_G$$
	ismgmid.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	mgmidcl.e	$$⊢\phi \to \exists e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$
Assertion	0gisid	$$⊢\phi \to \left(\underset{\dot{}}{0}\in B\wedge \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ismgmid.b	$$⊢B={\mathrm{Base}}_G$$
2		ismgmid.o	$$⊢\underset{\dot{}}{0}=0_G$$
3		ismgmid.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		mgmidcl.e	$$⊢\phi \to \exists e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$
5		oveq1	$$⊢e=i\to e\underset{\dot{}}{+}x=i\underset{\dot{}}{+}x$$
6	5	eqeq1d	$$⊢e=i\to \left(e\underset{\dot{}}{+}x=x\leftrightarrow i\underset{\dot{}}{+}x=x\right)$$
7	6	ovanraleqv	$$⊢e=i\to \left(\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\leftrightarrow \forall x\in B\left(i\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}i=x\right)\right)$$
8	7	cbvrexvw	$$⊢\exists e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\leftrightarrow \exists i\in B\forall x\in B\left(i\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}i=x\right)$$
9	1 2 3 4	ismgmid	$$⊢\phi \to \left(\left(i\in B\wedge \forall x\in B\left(i\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}i=x\right)\right)\leftrightarrow \underset{\dot{}}{0}=i\right)$$
10	9	biimpa	$$⊢\left(\phi \wedge \left(i\in B\wedge \forall x\in B\left(i\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}i=x\right)\right)\right)\to \underset{\dot{}}{0}=i$$
11		eleq1	$$⊢i=\underset{\dot{}}{0}\to \left(i\in B\leftrightarrow \underset{\dot{}}{0}\in B\right)$$
12		oveq1	$$⊢i=\underset{\dot{}}{0}\to i\underset{\dot{}}{+}x=\underset{\dot{}}{0}\underset{\dot{}}{+}x$$
13	12	eqeq1d	$$⊢i=\underset{\dot{}}{0}\to \left(i\underset{\dot{}}{+}x=x\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{+}x=x\right)$$
14	13	ovanraleqv	$$⊢i=\underset{\dot{}}{0}\to \left(\forall x\in B\left(i\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}i=x\right)\leftrightarrow \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$
15	11 14	anbi12d	$$⊢i=\underset{\dot{}}{0}\to \left(\left(i\in B\wedge \forall x\in B\left(i\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}i=x\right)\right)\leftrightarrow \left(\underset{\dot{}}{0}\in B\wedge \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)\right)$$
16	15	eqcoms	$$⊢\underset{\dot{}}{0}=i\to \left(\left(i\in B\wedge \forall x\in B\left(i\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}i=x\right)\right)\leftrightarrow \left(\underset{\dot{}}{0}\in B\wedge \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)\right)$$
17	16	adantl	$$⊢\left(\phi \wedge \underset{\dot{}}{0}=i\right)\to \left(\left(i\in B\wedge \forall x\in B\left(i\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}i=x\right)\right)\leftrightarrow \left(\underset{\dot{}}{0}\in B\wedge \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)\right)$$
18	17	biimpd	$$⊢\left(\phi \wedge \underset{\dot{}}{0}=i\right)\to \left(\left(i\in B\wedge \forall x\in B\left(i\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}i=x\right)\right)\to \left(\underset{\dot{}}{0}\in B\wedge \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)\right)$$
19	18	impancom	$$⊢\left(\phi \wedge \left(i\in B\wedge \forall x\in B\left(i\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}i=x\right)\right)\right)\to \left(\underset{\dot{}}{0}=i\to \left(\underset{\dot{}}{0}\in B\wedge \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)\right)$$
20	10 19	mpd	$$⊢\left(\phi \wedge \left(i\in B\wedge \forall x\in B\left(i\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}i=x\right)\right)\right)\to \left(\underset{\dot{}}{0}\in B\wedge \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$
21	20	rexlimdvaa	$$⊢\phi \to \left(\exists i\in B\forall x\in B\left(i\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}i=x\right)\to \left(\underset{\dot{}}{0}\in B\wedge \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)\right)$$
22	8 21	biimtrid	$$⊢\phi \to \left(\exists e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\to \left(\underset{\dot{}}{0}\in B\wedge \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)\right)$$
23	4 22	mpd	$$⊢\phi \to \left(\underset{\dot{}}{0}\in B\wedge \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$