Theorem cntziinsn

Description: Express any centralizer as an intersection of singleton centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	cntzrec.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	cntzrec.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion	cntziinsn	⊢ ( 𝑆 ⊆ 𝐵 → ( 𝑍 ‘ 𝑆 ) = ( 𝐵 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑍 ‘ { 𝑥 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		cntzrec.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		cntzrec.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
3		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
4	1 3 2	cntzval	⊢ ( 𝑆 ⊆ 𝐵 → ( 𝑍 ‘ 𝑆 ) = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) } )
5		ssel2	⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 )
6	1 3 2	cntzsnval	⊢ ( 𝑥 ∈ 𝐵 → ( 𝑍 ‘ { 𝑥 } ) = { 𝑦 ∈ 𝐵 ∣ ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) } )
7	5 6	syl	⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑍 ‘ { 𝑥 } ) = { 𝑦 ∈ 𝐵 ∣ ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) } )
8	7	iineq2dv	⊢ ( 𝑆 ⊆ 𝐵 → ∩ 𝑥 ∈ 𝑆 ( 𝑍 ‘ { 𝑥 } ) = ∩ 𝑥 ∈ 𝑆 { 𝑦 ∈ 𝐵 ∣ ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) } )
9	8	ineq2d	⊢ ( 𝑆 ⊆ 𝐵 → ( 𝐵 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑍 ‘ { 𝑥 } ) ) = ( 𝐵 ∩ ∩ 𝑥 ∈ 𝑆 { 𝑦 ∈ 𝐵 ∣ ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) } ) )
10		riinrab	⊢ ( 𝐵 ∩ ∩ 𝑥 ∈ 𝑆 { 𝑦 ∈ 𝐵 ∣ ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) } ) = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) }
11	9 10	eqtrdi	⊢ ( 𝑆 ⊆ 𝐵 → ( 𝐵 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑍 ‘ { 𝑥 } ) ) = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) } )
12	4 11	eqtr4d	⊢ ( 𝑆 ⊆ 𝐵 → ( 𝑍 ‘ 𝑆 ) = ( 𝐵 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑍 ‘ { 𝑥 } ) ) )