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 ‘ 𝑚 ) 𝑥 ) } ) )