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