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

Metamath Proof Explorer

Definition df-cntz

Description: Define thecentralizer of a subset of a magma, which is the set of elements each of which commutes with each element of the given subset. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Assertion df-cntz 
|- Cntz = ( m e. _V |-> ( s e. ~P ( Base ` m ) |-> { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccntz 
 |-  Cntz
1 vm 
 |-  m
2 cvv 
 |-  _V
3 vs 
 |-  s
4 cbs 
 |-  Base
5 1 cv 
 |-  m
6 5 4 cfv 
 |-  ( Base ` m )
7 6 cpw 
 |-  ~P ( Base ` m )
8 vx 
 |-  x
9 vy 
 |-  y
10 3 cv 
 |-  s
11 8 cv 
 |-  x
12 cplusg 
 |-  +g
13 5 12 cfv 
 |-  ( +g ` m )
14 9 cv 
 |-  y
15 11 14 13 co 
 |-  ( x ( +g ` m ) y )
16 14 11 13 co 
 |-  ( y ( +g ` m ) x )
17 15 16 wceq 
 |-  ( x ( +g ` m ) y ) = ( y ( +g ` m ) x )
18 17 9 10 wral 
 |-  A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x )
19 18 8 6 crab 
 |-  { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) }
20 3 7 19 cmpt 
 |-  ( s e. ~P ( Base ` m ) |-> { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) } )
21 1 2 20 cmpt 
 |-  ( m e. _V |-> ( s e. ~P ( Base ` m ) |-> { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) } ) )
22 0 21 wceq 
 |-  Cntz = ( m e. _V |-> ( s e. ~P ( Base ` m ) |-> { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) } ) )