Theorem ismgmid

Description: Conditions for a class to be the identity element of a magma, if it exists. (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	ismgmid	$$⊢\phi \to \left(\left(U\in B\wedge \forall x\in B\left(U\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}U=x\right)\right)\leftrightarrow \underset{\dot{}}{0}=U\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		id	$$⊢U\in B\to U\in B$$
6		mgmidmo	$$⊢{\exists }^{*}e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$
7		reu5	$$⊢\exists !e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\leftrightarrow \left(\exists e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\wedge {\exists }^{*}e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)$$
8	4 6 7	sylanblrc	$$⊢\phi \to \exists !e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$
9		oveq1	$$⊢e=U\to e\underset{\dot{}}{+}x=U\underset{\dot{}}{+}x$$
10	9	eqeq1d	$$⊢e=U\to \left(e\underset{\dot{}}{+}x=x\leftrightarrow U\underset{\dot{}}{+}x=x\right)$$
11	10	ovanraleqv	$$⊢e=U\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(U\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}U=x\right)\right)$$
12	11	riota2	$$⊢\left(U\in B\wedge \exists !e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\to \left(\forall x\in B\left(U\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}U=x\right)\leftrightarrow \left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)=U\right)$$
13	5 8 12	syl2anr	$$⊢\left(\phi \wedge U\in B\right)\to \left(\forall x\in B\left(U\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}U=x\right)\leftrightarrow \left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)=U\right)$$
14	13	pm5.32da	$$⊢\phi \to \left(\left(U\in B\wedge \forall x\in B\left(U\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}U=x\right)\right)\leftrightarrow \left(U\in B\wedge \left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)=U\right)\right)$$
15		riotacl	$$⊢\exists !e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\to \left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\in B$$
16	8 15	syl	$$⊢\phi \to \left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\in B$$
17		eleq1	$$⊢\left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)=U\to \left(\left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\in B\leftrightarrow U\in B\right)$$
18	16 17	syl5ibcom	$$⊢\phi \to \left(\left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)=U\to U\in B\right)$$
19	18	pm4.71rd	$$⊢\phi \to \left(\left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)=U\leftrightarrow \left(U\in B\wedge \left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)=U\right)\right)$$
20		df-riota	$$⊢\left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)=\left(\iota e|\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\right)$$
21	1 3 2	grpidval	$$⊢\underset{\dot{}}{0}=\left(\iota e|\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\right)$$
22	20 21	eqtr4i	$$⊢\left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)=\underset{\dot{}}{0}$$
23	22	eqeq1i	$$⊢\left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)=U\leftrightarrow \underset{\dot{}}{0}=U$$
24	23	a1i	$$⊢\phi \to \left(\left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)=U\leftrightarrow \underset{\dot{}}{0}=U\right)$$
25	14 19 24	3bitr2d	$$⊢\phi \to \left(\left(U\in B\wedge \forall x\in B\left(U\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}U=x\right)\right)\leftrightarrow \underset{\dot{}}{0}=U\right)$$