This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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