This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ Cntz = m ∈ V ⟼ s ∈ 𝒫 Base m ⟼ x ∈ Base m | ∀ y ∈ s x + m y = y + m x

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccntz class Cntz
1 vm setvar m
2 cvv class V
3 vs setvar s
4 cbs class Base
5 1 cv setvar m
6 5 4 cfv class Base m
7 6 cpw class 𝒫 Base m
8 vx setvar x
9 vy setvar y
10 3 cv setvar s
11 8 cv setvar x
12 cplusg class + 𝑔
13 5 12 cfv class + m
14 9 cv setvar y
15 11 14 13 co class x + m y
16 14 11 13 co class y + m x
17 15 16 wceq wff x + m y = y + m x
18 17 9 10 wral wff ∀ y ∈ s x + m y = y + m x
19 18 8 6 crab class x ∈ Base m | ∀ y ∈ s x + m y = y + m x
20 3 7 19 cmpt class s ∈ 𝒫 Base m ⟼ x ∈ Base m | ∀ y ∈ s x + m y = y + m x
21 1 2 20 cmpt class m ∈ V ⟼ s ∈ 𝒫 Base m ⟼ x ∈ Base m | ∀ y ∈ s x + m y = y + m x
22 0 21 wceq wff Cntz = m ∈ V ⟼ s ∈ 𝒫 Base m ⟼ x ∈ Base m | ∀ y ∈ s x + m y = y + m x