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

Metamath Proof Explorer

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 ⊢ ( 𝑆 ⊆ 𝐵 → ( 𝑍 ‘ 𝑆 ) = ( 𝐵 ∩ ∩ 𝑥 ∈ 𝑆 ( 𝑍 ‘ { 𝑥 } ) ) )