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	$$⊢\mathrm{Cntz}=\left(m\in \mathrm{V}⟼\left(s\in 𝒫{\mathrm{Base}}_m⟼\left\{x\in {\mathrm{Base}}_m|\forall y\in sx{+}_{m}y=y{+}_{m}x\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccntz	$$class\mathrm{Cntz}$$
1		vm	$$setvarm$$
2		cvv	$$class\mathrm{V}$$
3		vs	$$setvars$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarm$$
6	5 4	cfv	$$class{\mathrm{Base}}_m$$
7	6	cpw	$$class𝒫{\mathrm{Base}}_m$$
8		vx	$$setvarx$$
9		vy	$$setvary$$
10	3	cv	$$setvars$$
11	8	cv	$$setvarx$$
12		cplusg	$$class{+}_{𝑔}$$
13	5 12	cfv	$$class{+}_m$$
14	9	cv	$$setvary$$
15	11 14 13	co	$$class\left(x{+}_{m}y\right)$$
16	14 11 13	co	$$class\left(y{+}_{m}x\right)$$
17	15 16	wceq	$$wffx{+}_{m}y=y{+}_{m}x$$
18	17 9 10	wral	$$wff\forall y\in sx{+}_{m}y=y{+}_{m}x$$
19	18 8 6	crab	$$class\left\{x\in {\mathrm{Base}}_m|\forall y\in sx{+}_{m}y=y{+}_{m}x\right\}$$
20	3 7 19	cmpt	$$class\left(s\in 𝒫{\mathrm{Base}}_m⟼\left\{x\in {\mathrm{Base}}_m|\forall y\in sx{+}_{m}y=y{+}_{m}x\right\}\right)$$
21	1 2 20	cmpt	$$class\left(m\in \mathrm{V}⟼\left(s\in 𝒫{\mathrm{Base}}_m⟼\left\{x\in {\mathrm{Base}}_m|\forall y\in sx{+}_{m}y=y{+}_{m}x\right\}\right)\right)$$
22	0 21	wceq	$$wff\mathrm{Cntz}=\left(m\in \mathrm{V}⟼\left(s\in 𝒫{\mathrm{Base}}_m⟼\left\{x\in {\mathrm{Base}}_m|\forall y\in sx{+}_{m}y=y{+}_{m}x\right\}\right)\right)$$