Definition df-cntz 18711

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 = (𝑚 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑚) ↦ {𝑥 ∈ (Base‘𝑚) ∣ ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝑚)𝑦) = (𝑦(+g‘𝑚)𝑥)}))

Distinct variable group:   𝑚,𝑠,𝑥,𝑦

Detailed syntax breakdown of Definition df-cntz

Step	Hyp	Ref	Expression
1		ccntz 18709	. 2 class Cntz
2		vm	. . 3 setvar 𝑚
3		cvv 3408	. . 3 class V
4		vs	. . . 4 setvar 𝑠
5	2	cv 1542	. . . . . 6 class 𝑚
6		cbs 16760	. . . . . 6 class Base
7	5, 6	cfv 6380	. . . . 5 class (Base‘𝑚)
8	7	cpw 4513	. . . 4 class 𝒫 (Base‘𝑚)
9		vx	. . . . . . . . 9 setvar 𝑥
10	9	cv 1542	. . . . . . . 8 class 𝑥
11		vy	. . . . . . . . 9 setvar 𝑦
12	11	cv 1542	. . . . . . . 8 class 𝑦
13		cplusg 16802	. . . . . . . . 9 class +g
14	5, 13	cfv 6380	. . . . . . . 8 class (+g‘𝑚)
15	10, 12, 14	co 7213	. . . . . . 7 class (𝑥(+g‘𝑚)𝑦)
16	12, 10, 14	co 7213	. . . . . . 7 class (𝑦(+g‘𝑚)𝑥)
17	15, 16	wceq 1543	. . . . . 6 wff (𝑥(+g‘𝑚)𝑦) = (𝑦(+g‘𝑚)𝑥)
18	4	cv 1542	. . . . . 6 class 𝑠
19	17, 11, 18	wral 3061	. . . . 5 wff ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝑚)𝑦) = (𝑦(+g‘𝑚)𝑥)
20	19, 9, 7	crab 3065	. . . 4 class {𝑥 ∈ (Base‘𝑚) ∣ ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝑚)𝑦) = (𝑦(+g‘𝑚)𝑥)}
21	4, 8, 20	cmpt 5135	. . 3 class (𝑠 ∈ 𝒫 (Base‘𝑚) ↦ {𝑥 ∈ (Base‘𝑚) ∣ ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝑚)𝑦) = (𝑦(+g‘𝑚)𝑥)})
22	2, 3, 21	cmpt 5135	. 2 class (𝑚 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑚) ↦ {𝑥 ∈ (Base‘𝑚) ∣ ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝑚)𝑦) = (𝑦(+g‘𝑚)𝑥)}))
23	1, 22	wceq 1543	1 wff Cntz = (𝑚 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑚) ↦ {𝑥 ∈ (Base‘𝑚) ∣ ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝑚)𝑦) = (𝑦(+g‘𝑚)𝑥)}))

This definition is referenced by:  cntzfval  18714