This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = {Base}_{G}$
		ismgmid.o	$⊢ \underset{˙}{0} = 0_{G}$
		ismgmid.p	$⊢ \underset{˙}{+} = +_{G}$
		mgmidcl.e	$⊢ φ \to \exists e \in B \forall x \in B (e \underset{˙}{+} x = x \land x \underset{˙}{+} e = x)$
	Assertion	mgmlrid	$⊢ (φ \land X \in B) \to (\underset{˙}{0} \underset{˙}{+} X = X \land X \underset{˙}{+} \underset{˙}{0} = X)$

Proof

Step	Hyp	Ref	Expression
1		ismgmid.b	$⊢ B = {Base}_{G}$
2		ismgmid.o	$⊢ \underset{˙}{0} = 0_{G}$
3		ismgmid.p	$⊢ \underset{˙}{+} = +_{G}$
4		mgmidcl.e	$⊢ φ \to \exists e \in B \forall x \in B (e \underset{˙}{+} x = x \land x \underset{˙}{+} e = x)$
5		eqid	$⊢ \underset{˙}{0} = \underset{˙}{0}$
6	1 2 3 4	ismgmid	$⊢ φ \to ((\underset{˙}{0} \in B \land \forall x \in B (\underset{˙}{0} \underset{˙}{+} x = x \land x \underset{˙}{+} \underset{˙}{0} = x)) \leftrightarrow \underset{˙}{0} = \underset{˙}{0})$
7	5 6	mpbiri	$⊢ φ \to (\underset{˙}{0} \in B \land \forall x \in B (\underset{˙}{0} \underset{˙}{+} x = x \land x \underset{˙}{+} \underset{˙}{0} = x))$
8	7	simprd	$⊢ φ \to \forall x \in B (\underset{˙}{0} \underset{˙}{+} x = x \land x \underset{˙}{+} \underset{˙}{0} = x)$
9		oveq2	$⊢ x = X \to \underset{˙}{0} \underset{˙}{+} x = \underset{˙}{0} \underset{˙}{+} X$
10		id	$⊢ x = X \to x = X$
11	9 10	eqeq12d	$⊢ x = X \to (\underset{˙}{0} \underset{˙}{+} x = x \leftrightarrow \underset{˙}{0} \underset{˙}{+} X = X)$
12		oveq1	$⊢ x = X \to x \underset{˙}{+} \underset{˙}{0} = X \underset{˙}{+} \underset{˙}{0}$
13	12 10	eqeq12d	$⊢ x = X \to (x \underset{˙}{+} \underset{˙}{0} = x \leftrightarrow X \underset{˙}{+} \underset{˙}{0} = X)$
14	11 13	anbi12d	$⊢ x = X \to ((\underset{˙}{0} \underset{˙}{+} x = x \land x \underset{˙}{+} \underset{˙}{0} = x) \leftrightarrow (\underset{˙}{0} \underset{˙}{+} X = X \land X \underset{˙}{+} \underset{˙}{0} = X))$
15	14	rspccva	$⊢ (\forall x \in B (\underset{˙}{0} \underset{˙}{+} x = x \land x \underset{˙}{+} \underset{˙}{0} = x) \land X \in B) \to (\underset{˙}{0} \underset{˙}{+} X = X \land X \underset{˙}{+} \underset{˙}{0} = X)$
16	8 15	sylan	$⊢ (φ \land X \in B) \to (\underset{˙}{0} \underset{˙}{+} X = X \land X \underset{˙}{+} \underset{˙}{0} = X)$