Theorem mgmlrid

Description: The identity element of a magma, if it exists, is a left and right identity. (Contributed by Mario Carneiro, 27-Dec-2014)

	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	mgmlrid	$$⊢\left(\phi \wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{+}X=X\wedge X\underset{\dot{}}{+}\underset{\dot{}}{0}=X\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		eqid	$$⊢\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
6	1 2 3 4	ismgmid	$$⊢\phi \to \left(\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)\leftrightarrow \underset{\dot{}}{0}=\underset{\dot{}}{0}\right)$$
7	5 6	mpbiri	$$⊢\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)$$
8	7	simprd	$$⊢\phi \to \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)$$
9		oveq2	$$⊢x=X\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=\underset{\dot{}}{0}\underset{\dot{}}{+}X$$
10		id	$$⊢x=X\to x=X$$
11	9 10	eqeq12d	$$⊢x=X\to \left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{+}X=X\right)$$
12		oveq1	$$⊢x=X\to x\underset{\dot{}}{+}\underset{\dot{}}{0}=X\underset{\dot{}}{+}\underset{\dot{}}{0}$$
13	12 10	eqeq12d	$$⊢x=X\to \left(x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\leftrightarrow X\underset{\dot{}}{+}\underset{\dot{}}{0}=X\right)$$
14	11 13	anbi12d	$$⊢x=X\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{+}X=X\wedge X\underset{\dot{}}{+}\underset{\dot{}}{0}=X\right)\right)$$
15	14	rspccva	$$⊢\left(\forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{+}X=X\wedge X\underset{\dot{}}{+}\underset{\dot{}}{0}=X\right)$$
16	8 15	sylan	$$⊢\left(\phi \wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{+}X=X\wedge X\underset{\dot{}}{+}\underset{\dot{}}{0}=X\right)$$