Definition df-cntz 15071

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 15069	. 2 class Cntz
2		vm	. . 3 set m
3		cvv 2916	. . 3 class _V
4		vs	. . . 4 set s
5	2	cv 1648	. . . . . 6 class m
6		cbs 13424	. . . . . 6 class Base
7	5, 6	cfv 5413	. . . . 5 class ( Base ` m )
8	7	cpw 3759	. . . 4 class ~P ( Base ` m )
9		vx	. . . . . . . . 9 set x
10	9	cv 1648	. . . . . . . 8 class x
11		vy	. . . . . . . . 9 set y
12	11	cv 1648	. . . . . . . 8 class y
13		cplusg 13484	. . . . . . . . 9 class +g
14	5, 13	cfv 5413	. . . . . . . 8 class ( +g ` m )
15	10, 12, 14	co 6040	. . . . . . 7 class ( x ( +g ` m ) y )
16	12, 10, 14	co 6040	. . . . . . 7 class ( y ( +g ` m ) x )
17	15, 16	wceq 1649	. . . . . 6 wff ( x ( +g ` m ) y ) = ( y ( +g ` m ) x )
18	4	cv 1648	. . . . . 6 class s
19	17, 11, 18	wral 2666	. . . . 5 wff A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x )
20	19, 9, 7	crab 2670	. . . 4 class { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) }
21	4, 8, 20	cmpt 4226	. . 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 4226	. 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 1649	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  15074