Definition df-cntr

Description: Define thecenter of a magma, which is the elements that commute with all others. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Assertion	df-cntr	|- Cntr = ( m e. _V |-> ( ( Cntz ` m ) ` ( Base ` m ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccntr	|- Cntr
1		vm	|- m
2		cvv	|- _V
3		ccntz	|- Cntz
4	1	cv	|- m
5	4 3	cfv	|- ( Cntz ` m )
6		cbs	|- Base
7	4 6	cfv	|- ( Base ` m )
8	7 5	cfv	|- ( ( Cntz ` m ) ` ( Base ` m ) )
9	1 2 8	cmpt	|- ( m e. _V |-> ( ( Cntz ` m ) ` ( Base ` m ) ) )
10	0 9	wceq	|- Cntr = ( m e. _V |-> ( ( Cntz ` m ) ` ( Base ` m ) ) )