Theorem ismgmid2

Description: Show that a given element is the identity element of a magma. (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$$
	ismgmid2.u	$$⊢\phi \to U\in B$$
	ismgmid2.l	$$⊢\left(\phi \wedge x\in B\right)\to U\underset{\dot{}}{+}x=x$$
	ismgmid2.r	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{+}U=x$$
Assertion	ismgmid2	$$⊢\phi \to U=\underset{\dot{}}{0}$$

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		ismgmid2.u	$$⊢\phi \to U\in B$$
5		ismgmid2.l	$$⊢\left(\phi \wedge x\in B\right)\to U\underset{\dot{}}{+}x=x$$
6		ismgmid2.r	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{+}U=x$$
7	5 6	jca	$$⊢\left(\phi \wedge x\in B\right)\to \left(U\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}U=x\right)$$
8	7	ralrimiva	$$⊢\phi \to \forall x\in B\left(U\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}U=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	rspcev	$$⊢\left(U\in B\wedge \forall x\in B\left(U\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}U=x\right)\right)\to \exists e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$
13	4 8 12	syl2anc	$$⊢\phi \to \exists e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$
14	1 2 3 13	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)$$
15	4 8 14	mpbi2and	$$⊢\phi \to \underset{\dot{}}{0}=U$$
16	15	eqcomd	$$⊢\phi \to U=\underset{\dot{}}{0}$$