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

Metamath Proof Explorer

Theorem gsumvallem2

Description: Lemma for properties of the set of identities of G . The set of identities of a monoid is exactly the unique identity element. (Contributed by Mario Carneiro, 7-Dec-2014)

		Ref	Expression
	Hypotheses	gsumvallem2.b	$⊢ B = {Base}_{G}$
		gsumvallem2.z	$⊢ \underset{˙}{0} = 0_{G}$
		gsumvallem2.p	$⊢ \underset{˙}{+} = +_{G}$
		gsumvallem2.o	$⊢ O = \{x \in B \| \forall y \in B (x \underset{˙}{+} y = y \land y \underset{˙}{+} x = y)\}$
	Assertion	gsumvallem2	$⊢ G \in Mnd \to O = \{\underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		gsumvallem2.b	$⊢ B = {Base}_{G}$
2		gsumvallem2.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumvallem2.p	$⊢ \underset{˙}{+} = +_{G}$
4		gsumvallem2.o	$⊢ O = \{x \in B \| \forall y \in B (x \underset{˙}{+} y = y \land y \underset{˙}{+} x = y)\}$
5	1 2 3 4	mgmidsssn0	$⊢ G \in Mnd \to O \subseteq \{\underset{˙}{0}\}$
6	1 2	mndidcl	$⊢ G \in Mnd \to \underset{˙}{0} \in B$
7	1 3 2	mndlrid	$⊢ (G \in Mnd \land y \in B) \to (\underset{˙}{0} \underset{˙}{+} y = y \land y \underset{˙}{+} \underset{˙}{0} = y)$
8	7	ralrimiva	$⊢ G \in Mnd \to \forall y \in B (\underset{˙}{0} \underset{˙}{+} y = y \land y \underset{˙}{+} \underset{˙}{0} = y)$
9		oveq1	$⊢ x = \underset{˙}{0} \to x \underset{˙}{+} y = \underset{˙}{0} \underset{˙}{+} y$
10	9	eqeq1d	$⊢ x = \underset{˙}{0} \to (x \underset{˙}{+} y = y \leftrightarrow \underset{˙}{0} \underset{˙}{+} y = y)$
11	10	ovanraleqv	$⊢ x = \underset{˙}{0} \to (\forall y \in B (x \underset{˙}{+} y = y \land y \underset{˙}{+} x = y) \leftrightarrow \forall y \in B (\underset{˙}{0} \underset{˙}{+} y = y \land y \underset{˙}{+} \underset{˙}{0} = y))$
12	11 4	elrab2	$⊢ \underset{˙}{0} \in O \leftrightarrow (\underset{˙}{0} \in B \land \forall y \in B (\underset{˙}{0} \underset{˙}{+} y = y \land y \underset{˙}{+} \underset{˙}{0} = y))$
13	6 8 12	sylanbrc	$⊢ G \in Mnd \to \underset{˙}{0} \in O$
14	13	snssd	$⊢ G \in Mnd \to \{\underset{˙}{0}\} \subseteq O$
15	5 14	eqssd	$⊢ G \in Mnd \to O = \{\underset{˙}{0}\}$