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 
|- 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 ) ) )