elcntr

Description: Elementhood in the center of a magma. (Contributed by SN, 21-Mar-2025)

	Ref	Expression
Hypotheses	elcntr.b	$⊢ B = {Base}_{M}$
	elcntr.p	$⊢ \underset{˙}{+} = +_{M}$
	elcntr.z	$⊢ Z = Cntr (M)$
Assertion	elcntr	$⊢ A \in Z \leftrightarrow (A \in B \land \forall y \in B A \underset{˙}{+} y = y \underset{˙}{+} A)$

Step	Hyp	Ref	Expression
1		elcntr.b	$⊢ B = {Base}_{M}$
2		elcntr.p	$⊢ \underset{˙}{+} = +_{M}$
3		elcntr.z	$⊢ Z = Cntr (M)$
4		eqid	$⊢ Cntz (M) = Cntz (M)$
5	1 4	cntrval	$⊢ Cntz (M) (B) = Cntr (M)$
6	3 5	eqtr4i	$⊢ Z = Cntz (M) (B)$
7	6	eleq2i	$⊢ A \in Z \leftrightarrow A \in Cntz (M) (B)$
8		ssid	$⊢ B \subseteq B$
9	1 2 4	elcntz	$⊢ B \subseteq B \to (A \in Cntz (M) (B) \leftrightarrow (A \in B \land \forall y \in B A \underset{˙}{+} y = y \underset{˙}{+} A))$
10	8 9	ax-mp	$⊢ A \in Cntz (M) (B) \leftrightarrow (A \in B \land \forall y \in B A \underset{˙}{+} y = y \underset{˙}{+} A)$
11	7 10	bitri	$⊢ A \in Z \leftrightarrow (A \in B \land \forall y \in B A \underset{˙}{+} y = y \underset{˙}{+} A)$

Metamath Proof Explorer