Metamath Proof Explorer


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 ( 𝐴𝑍 ↔ ( 𝐴𝐵 ∧ ∀ 𝑦𝐵 ( 𝐴 + 𝑦 ) = ( 𝑦 + 𝐴 ) ) )