Theorem elcntr

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

	Ref	Expression
Hypotheses	elcntr.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	elcntr.p	⊢ + = ( +g ‘ 𝑀 )
	elcntr.z	⊢ 𝑍 = ( Cntr ‘ 𝑀 )
Assertion	elcntr	⊢ ( 𝐴 ∈ 𝑍 ↔ ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 + 𝑦 ) = ( 𝑦 + 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elcntr.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		elcntr.p	⊢ + = ( +g ‘ 𝑀 )
3		elcntr.z	⊢ 𝑍 = ( Cntr ‘ 𝑀 )
4		eqid	⊢ ( Cntz ‘ 𝑀 ) = ( Cntz ‘ 𝑀 )
5	1 4	cntrval	⊢ ( ( Cntz ‘ 𝑀 ) ‘ 𝐵 ) = ( Cntr ‘ 𝑀 )
6	3 5	eqtr4i	⊢ 𝑍 = ( ( Cntz ‘ 𝑀 ) ‘ 𝐵 )
7	6	eleq2i	⊢ ( 𝐴 ∈ 𝑍 ↔ 𝐴 ∈ ( ( Cntz ‘ 𝑀 ) ‘ 𝐵 ) )
8		ssid	⊢ 𝐵 ⊆ 𝐵
9	1 2 4	elcntz	⊢ ( 𝐵 ⊆ 𝐵 → ( 𝐴 ∈ ( ( Cntz ‘ 𝑀 ) ‘ 𝐵 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 + 𝑦 ) = ( 𝑦 + 𝐴 ) ) ) )
10	8 9	ax-mp	⊢ ( 𝐴 ∈ ( ( Cntz ‘ 𝑀 ) ‘ 𝐵 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 + 𝑦 ) = ( 𝑦 + 𝐴 ) ) )
11	7 10	bitri	⊢ ( 𝐴 ∈ 𝑍 ↔ ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 + 𝑦 ) = ( 𝑦 + 𝐴 ) ) )