MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cntz Structured version   Visualization version   GIF version

Definition df-cntz 17522
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
StepHypRef Expression
1 ccntz 17520 . 2 class Cntz
2 vm . . 3 setvar 𝑚
3 cvv 3173 . . 3 class V
4 vs . . . 4 setvar 𝑠
52cv 1474 . . . . . 6 class 𝑚
6 cbs 15644 . . . . . 6 class Base
75, 6cfv 5790 . . . . 5 class (Base‘𝑚)
87cpw 4108 . . . 4 class 𝒫 (Base‘𝑚)
9 vx . . . . . . . . 9 setvar 𝑥
109cv 1474 . . . . . . . 8 class 𝑥
11 vy . . . . . . . . 9 setvar 𝑦
1211cv 1474 . . . . . . . 8 class 𝑦
13 cplusg 15717 . . . . . . . . 9 class +g
145, 13cfv 5790 . . . . . . . 8 class (+g𝑚)
1510, 12, 14co 6527 . . . . . . 7 class (𝑥(+g𝑚)𝑦)
1612, 10, 14co 6527 . . . . . . 7 class (𝑦(+g𝑚)𝑥)
1715, 16wceq 1475 . . . . . 6 wff (𝑥(+g𝑚)𝑦) = (𝑦(+g𝑚)𝑥)
184cv 1474 . . . . . 6 class 𝑠
1917, 11, 18wral 2896 . . . . 5 wff 𝑦𝑠 (𝑥(+g𝑚)𝑦) = (𝑦(+g𝑚)𝑥)
2019, 9, 7crab 2900 . . . 4 class {𝑥 ∈ (Base‘𝑚) ∣ ∀𝑦𝑠 (𝑥(+g𝑚)𝑦) = (𝑦(+g𝑚)𝑥)}
214, 8, 20cmpt 4638 . . 3 class (𝑠 ∈ 𝒫 (Base‘𝑚) ↦ {𝑥 ∈ (Base‘𝑚) ∣ ∀𝑦𝑠 (𝑥(+g𝑚)𝑦) = (𝑦(+g𝑚)𝑥)})
222, 3, 21cmpt 4638 . 2 class (𝑚 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑚) ↦ {𝑥 ∈ (Base‘𝑚) ∣ ∀𝑦𝑠 (𝑥(+g𝑚)𝑦) = (𝑦(+g𝑚)𝑥)}))
231, 22wceq 1475 1 wff Cntz = (𝑚 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑚) ↦ {𝑥 ∈ (Base‘𝑚) ∣ ∀𝑦𝑠 (𝑥(+g𝑚)𝑦) = (𝑦(+g𝑚)𝑥)}))
Colors of variables: wff setvar class
This definition is referenced by:  cntzfval  17525
  Copyright terms: Public domain W3C validator