Definition df-cntz 14142

Description: Define the centralizer 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.)

Assertion

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

Distinct variable group:   m, s, x, y

Detailed syntax breakdown of Definition df-cntz

Step	Hyp	Ref	Expression
1		ccntz 14140	. 2 class Cntz
2		vm	. . 3 setvar m
3		cvv 2821	. . 3 class _V
4		vs	. . . 4 setvar s
5	2	cv 1401	. . . . . 6 class m
6		cbs 13404	. . . . . 6 class Base
7	5, 6	cfv 5377	. . . . 5 class ( Base ` m )
8	7	cpw 3688	. . . 4 class ~P ( Base ` m )
9		vx	. . . . . . . . 9 setvar x
10	9	cv 1401	. . . . . . . 8 class x
11		vy	. . . . . . . . 9 setvar y
12	11	cv 1401	. . . . . . . 8 class y
13		cplusg 13484	. . . . . . . . 9 class +g
14	5, 13	cfv 5377	. . . . . . . 8 class ( +g ` m )
15	10, 12, 14	co 6085	. . . . . . 7 class ( x ( +g ` m ) y )
16	12, 10, 14	co 6085	. . . . . . 7 class ( y ( +g ` m ) x )
17	15, 16	wceq 1402	. . . . . 6 wff ( x ( +g ` m ) y ) = ( y ( +g ` m ) x )
18	4	cv 1401	. . . . . 6 class s
19	17, 11, 18	wral 2528	. . . . 5 wff A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x )
20	19, 9, 7	crab 2532	. . . 4 class { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) }
21	4, 8, 20	cmpt 4192	. . 3 class ( s e. ~P ( Base ` m ) |-> { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) } )
22	2, 3, 21	cmpt 4192	. 2 class ( m e. _V |-> ( s e. ~P ( Base ` m ) |-> { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) } ) )
23	1, 22	wceq 1402	1 wff 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 ) } ) )

This definition is used by:  cntzex  14144  cntrval  14145  cntzfval  14146  cntzval  14147  cntzrcl  14153