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

Metamath Proof Explorer

Theorem cntzssv

Description: The centralizer is unconditionally a subset. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses cntzrcl.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
cntzrcl.z ⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion cntzssv ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵

Proof

Step Hyp Ref Expression
1 cntzrcl.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 cntzrcl.z ⊢ 𝑍 = ( Cntz ‘ 𝑀 )
3 0ss ⊢ ∅ ⊆ 𝐵
4 sseq1 ⊢ ( ( 𝑍 ‘ 𝑆 ) = ∅ → ( ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 ↔ ∅ ⊆ 𝐵 ) )
5 3 4 mpbiri ⊢ ( ( 𝑍 ‘ 𝑆 ) = ∅ → ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 )
6 n0 ⊢ ( ( 𝑍 ‘ 𝑆 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) )
7 1 2 cntzrcl ⊢ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) → ( 𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵 ) )
8 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
9 1 8 2 cntzval ⊢ ( 𝑆 ⊆ 𝐵 → ( 𝑍 ‘ 𝑆 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) } )
10 7 9 simpl2im ⊢ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) → ( 𝑍 ‘ 𝑆 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) } )
11 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) } ⊆ 𝐵
12 10 11 eqsstrdi ⊢ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) → ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 )
13 12 exlimiv ⊢ ( ∃ 𝑥 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) → ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 )
14 6 13 sylbi ⊢ ( ( 𝑍 ‘ 𝑆 ) ≠ ∅ → ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 )
15 5 14 pm2.61ine ⊢ ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵