Theorem 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	|- .+ = ( +g ` M )
	elcntr.z	|- Z = ( Cntr ` M )
Assertion	elcntr	|- ( A e. Z <-> ( A e. B /\ A. y e. B ( A .+ y ) = ( y .+ A ) ) )

Proof

Step	Hyp	Ref	Expression
1		elcntr.b	|- B = ( Base ` M )
2		elcntr.p	|- .+ = ( +g ` 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 e. Z <-> A e. ( ( Cntz ` M ) ` B ) )
8		ssid	|- B C_ B
9	1 2 4	elcntz	|- ( B C_ B -> ( A e. ( ( Cntz ` M ) ` B ) <-> ( A e. B /\ A. y e. B ( A .+ y ) = ( y .+ A ) ) ) )
10	8 9	ax-mp	|- ( A e. ( ( Cntz ` M ) ` B ) <-> ( A e. B /\ A. y e. B ( A .+ y ) = ( y .+ A ) ) )
11	7 10	bitri	|- ( A e. Z <-> ( A e. B /\ A. y e. B ( A .+ y ) = ( y .+ A ) ) )