Metamath Proof Explorer


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 + ˙ = + M
elcntr.z Z = Cntr M
Assertion elcntr A Z A B y B A + ˙ y = y + ˙ A

Proof

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