Theorem elcntr

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

	Ref	Expression
Hypotheses	elcntr.b	$$⊢B={\mathrm{Base}}_M$$
	elcntr.p	$$⊢\underset{\dot{}}{+}={+}_M$$
	elcntr.z	$$⊢Z=\mathrm{Cntr}\left(M\right)$$
Assertion	elcntr	$$⊢A\in Z\leftrightarrow \left(A\in B\wedge \forall y\in BA\underset{\dot{}}{+}y=y\underset{\dot{}}{+}A\right)$$

Proof

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