Definition df-cntz 16971

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 16969	. 2 class Cntz
2		vm	. . 3 setvar m
3		cvv 3045	. . 3 class _V
4		vs	. . . 4 setvar s
5	2	cv 1443	. . . . . 6 class m
6		cbs 15121	. . . . . 6 class Base
7	5, 6	cfv 5582	. . . . 5 class ( Base ` m )
8	7	cpw 3951	. . . 4 class ~P ( Base ` m )
9		vx	. . . . . . . . 9 setvar x
10	9	cv 1443	. . . . . . . 8 class x
11		vy	. . . . . . . . 9 setvar y
12	11	cv 1443	. . . . . . . 8 class y
13		cplusg 15190	. . . . . . . . 9 class +g
14	5, 13	cfv 5582	. . . . . . . 8 class ( +g ` m )
15	10, 12, 14	co 6290	. . . . . . 7 class ( x ( +g ` m ) y )
16	12, 10, 14	co 6290	. . . . . . 7 class ( y ( +g ` m ) x )
17	15, 16	wceq 1444	. . . . . 6 wff ( x ( +g ` m ) y ) = ( y ( +g ` m ) x )
18	4	cv 1443	. . . . . 6 class s
19	17, 11, 18	wral 2737	. . . . 5 wff A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x )
20	19, 9, 7	crab 2741	. . . 4 class { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) }
21	4, 8, 20	cmpt 4461	. . 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 4461	. 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 1444	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 referenced by:  cntzfval  16974