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

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccntz ⊢ Cntz
1 vm ⊢ 𝑚
2 cvv ⊢ V
3 vs ⊢ 𝑠
4 cbs ⊢ Base
5 1 cv ⊢ 𝑚
6 5 4 cfv ⊢ ( Base ‘ 𝑚 )
7 6 cpw ⊢ 𝒫 ( Base ‘ 𝑚 )
8 vx ⊢ 𝑥
9 vy ⊢ 𝑦
10 3 cv ⊢ 𝑠
11 8 cv ⊢ 𝑥
12 cplusg ⊢ +g
13 5 12 cfv ⊢ ( +g ‘ 𝑚 )
14 9 cv ⊢ 𝑦
15 11 14 13 co ⊢ ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 )
16 14 11 13 co ⊢ ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 )
17 15 16 wceq ⊢ ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 )
18 17 9 10 wral ⊢ ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 )
19 18 8 6 crab ⊢ { 𝑥 ∈ ( Base ‘ 𝑚 ) ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) }
20 3 7 19 cmpt ⊢ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑚 ) ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) } )
21 1 2 20 cmpt ⊢ ( 𝑚 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑚 ) ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) } ) )
22 0 21 wceq ⊢ Cntz = ( 𝑚 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑚 ) ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) } ) )