Theorem mgmidmo

Description: A two-sided identity element is unique (if it exists) in any magma. (Contributed by Mario Carneiro, 7-Dec-2014) (Revised by NM, 17-Jun-2017)

	Ref	Expression
Assertion	mgmidmo	$$⊢{\exists }^{*}u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\to u\underset{\dot{}}{+}x=x$$
2	1	ralimi	$$⊢\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\to \forall x\in Bu\underset{\dot{}}{+}x=x$$
3		simpr	$$⊢\left(w\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}w=x\right)\to x\underset{\dot{}}{+}w=x$$
4	3	ralimi	$$⊢\forall x\in B\left(w\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}w=x\right)\to \forall x\in Bx\underset{\dot{}}{+}w=x$$
5		oveq1	$$⊢x=u\to x\underset{\dot{}}{+}w=u\underset{\dot{}}{+}w$$
6		id	$$⊢x=u\to x=u$$
7	5 6	eqeq12d	$$⊢x=u\to \left(x\underset{\dot{}}{+}w=x\leftrightarrow u\underset{\dot{}}{+}w=u\right)$$
8	7	rspcva	$$⊢\left(u\in B\wedge \forall x\in Bx\underset{\dot{}}{+}w=x\right)\to u\underset{\dot{}}{+}w=u$$
9		oveq2	$$⊢x=w\to u\underset{\dot{}}{+}x=u\underset{\dot{}}{+}w$$
10		id	$$⊢x=w\to x=w$$
11	9 10	eqeq12d	$$⊢x=w\to \left(u\underset{\dot{}}{+}x=x\leftrightarrow u\underset{\dot{}}{+}w=w\right)$$
12	11	rspcva	$$⊢\left(w\in B\wedge \forall x\in Bu\underset{\dot{}}{+}x=x\right)\to u\underset{\dot{}}{+}w=w$$
13	8 12	sylan9req	$$⊢\left(\left(u\in B\wedge \forall x\in Bx\underset{\dot{}}{+}w=x\right)\wedge \left(w\in B\wedge \forall x\in Bu\underset{\dot{}}{+}x=x\right)\right)\to u=w$$
14	13	an42s	$$⊢\left(\left(u\in B\wedge w\in B\right)\wedge \left(\forall x\in Bu\underset{\dot{}}{+}x=x\wedge \forall x\in Bx\underset{\dot{}}{+}w=x\right)\right)\to u=w$$
15	14	ex	$$⊢\left(u\in B\wedge w\in B\right)\to \left(\left(\forall x\in Bu\underset{\dot{}}{+}x=x\wedge \forall x\in Bx\underset{\dot{}}{+}w=x\right)\to u=w\right)$$
16	2 4 15	syl2ani	$$⊢\left(u\in B\wedge w\in B\right)\to \left(\left(\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\wedge \forall x\in B\left(w\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}w=x\right)\right)\to u=w\right)$$
17	16	rgen2	$$⊢\forall u\in B\forall w\in B\left(\left(\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\wedge \forall x\in B\left(w\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}w=x\right)\right)\to u=w\right)$$
18		oveq1	$$⊢u=w\to u\underset{\dot{}}{+}x=w\underset{\dot{}}{+}x$$
19	18	eqeq1d	$$⊢u=w\to \left(u\underset{\dot{}}{+}x=x\leftrightarrow w\underset{\dot{}}{+}x=x\right)$$
20	19	ovanraleqv	$$⊢u=w\to \left(\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\leftrightarrow \forall x\in B\left(w\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}w=x\right)\right)$$
21	20	rmo4	$$⊢{\exists }^{*}u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\leftrightarrow \forall u\in B\forall w\in B\left(\left(\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\wedge \forall x\in B\left(w\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}w=x\right)\right)\to u=w\right)$$
22	17 21	mpbir	$$⊢{\exists }^{*}u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$