ismgmid2

Description: Show that a given element is the identity element of a magma. (Contributed by Mario Carneiro, 27-Dec-2014)

Step	Hyp	Ref	Expression
1		ismgmid.b	$⊢ B = {Base}_{G}$
2		ismgmid.o	$⊢ \underset{˙}{0} = 0_{G}$
3		ismgmid.p	$⊢ \underset{˙}{+} = +_{G}$
4		ismgmid2.u	$⊢ φ \to U \in B$
5		ismgmid2.l	$⊢ (φ \land x \in B) \to U \underset{˙}{+} x = x$
6		ismgmid2.r	$⊢ (φ \land x \in B) \to x \underset{˙}{+} U = x$
7	5 6	jca	$⊢ (φ \land x \in B) \to (U \underset{˙}{+} x = x \land x \underset{˙}{+} U = x)$
8	7	ralrimiva	$⊢ φ \to \forall x \in B (U \underset{˙}{+} x = x \land x \underset{˙}{+} U = x)$
9		oveq1	$⊢ e = U \to e \underset{˙}{+} x = U \underset{˙}{+} x$
10	9	eqeq1d	$⊢ e = U \to (e \underset{˙}{+} x = x \leftrightarrow U \underset{˙}{+} x = x)$
11	10	ovanraleqv	$⊢ e = U \to (\forall x \in B (e \underset{˙}{+} x = x \land x \underset{˙}{+} e = x) \leftrightarrow \forall x \in B (U \underset{˙}{+} x = x \land x \underset{˙}{+} U = x))$
12	11	rspcev	$⊢ (U \in B \land \forall x \in B (U \underset{˙}{+} x = x \land x \underset{˙}{+} U = x)) \to \exists e \in B \forall x \in B (e \underset{˙}{+} x = x \land x \underset{˙}{+} e = x)$
13	4 8 12	syl2anc	$⊢ φ \to \exists e \in B \forall x \in B (e \underset{˙}{+} x = x \land x \underset{˙}{+} e = x)$
14	1 2 3 13	ismgmid	$⊢ φ \to ((U \in B \land \forall x \in B (U \underset{˙}{+} x = x \land x \underset{˙}{+} U = x)) \leftrightarrow \underset{˙}{0} = U)$
15	4 8 14	mpbi2and	$⊢ φ \to \underset{˙}{0} = U$
16	15	eqcomd	$⊢ φ \to U = \underset{˙}{0}$

Metamath Proof Explorer