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 ⊢ B = Base M
cntzrcl.z ⊢ Z = Cntz ⁡ M
Assertion cntzssv ⊢ Z ⁡ S ⊆ B

Proof

Step Hyp Ref Expression
1 cntzrcl.b ⊢ B = Base M
2 cntzrcl.z ⊢ Z = Cntz ⁡ M
3 0ss ⊢ ∅ ⊆ B
4 sseq1 ⊢ Z ⁡ S = ∅ → Z ⁡ S ⊆ B ↔ ∅ ⊆ B
5 3 4 mpbiri ⊢ Z ⁡ S = ∅ → Z ⁡ S ⊆ B
6 n0 ⊢ Z ⁡ S ≠ ∅ ↔ ∃ x x ∈ Z ⁡ S
7 1 2 cntzrcl ⊢ x ∈ Z ⁡ S → M ∈ V ∧ S ⊆ B
8 eqid ⊢ + M = + M
9 1 8 2 cntzval ⊢ S ⊆ B → Z ⁡ S = x ∈ B | ∀ y ∈ S x + M y = y + M x
10 7 9 simpl2im ⊢ x ∈ Z ⁡ S → Z ⁡ S = x ∈ B | ∀ y ∈ S x + M y = y + M x
11 ssrab2 ⊢ x ∈ B | ∀ y ∈ S x + M y = y + M x ⊆ B
12 10 11 eqsstrdi ⊢ x ∈ Z ⁡ S → Z ⁡ S ⊆ B
13 12 exlimiv ⊢ ∃ x x ∈ Z ⁡ S → Z ⁡ S ⊆ B
14 6 13 sylbi ⊢ Z ⁡ S ≠ ∅ → Z ⁡ S ⊆ B
15 5 14 pm2.61ine ⊢ Z ⁡ S ⊆ B