Metamath Proof Explorer

Theorem cntzrcl

Description: Reverse closure for elements of the centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses cntzrcl.b ⊢ B = Base M
cntzrcl.z ⊢ Z = Cntz ⁡ M
Assertion cntzrcl ⊢ X ∈ Z ⁡ S → M ∈ V ∧ S ⊆ B

Proof

Step Hyp Ref Expression
1 cntzrcl.b ⊢ B = Base M
2 cntzrcl.z ⊢ Z = Cntz ⁡ M
3 noel ⊢ ¬ X ∈ ∅
4 fvprc ⊢ ¬ M ∈ V → Cntz ⁡ M = ∅
5 2 4 syl5eq ⊢ ¬ M ∈ V → Z = ∅
6 5 fveq1d ⊢ ¬ M ∈ V → Z ⁡ S = ∅ ⁡ S
7 0fv ⊢ ∅ ⁡ S = ∅
8 6 7 syl6eq ⊢ ¬ M ∈ V → Z ⁡ S = ∅
9 8 eleq2d ⊢ ¬ M ∈ V → X ∈ Z ⁡ S ↔ X ∈ ∅
10 3 9 mtbiri ⊢ ¬ M ∈ V → ¬ X ∈ Z ⁡ S
11 10 con4i ⊢ X ∈ Z ⁡ S → M ∈ V
12 eqid ⊢ + M = + M
13 1 12 2 cntzfval ⊢ M ∈ V → Z = x ∈ 𝒫 B ⟼ y ∈ B | ∀ z ∈ x y + M z = z + M y
14 11 13 syl ⊢ X ∈ Z ⁡ S → Z = x ∈ 𝒫 B ⟼ y ∈ B | ∀ z ∈ x y + M z = z + M y
15 14 dmeqd ⊢ X ∈ Z ⁡ S → dom ⁡ Z = dom ⁡ x ∈ 𝒫 B ⟼ y ∈ B | ∀ z ∈ x y + M z = z + M y
16 eqid ⊢ x ∈ 𝒫 B ⟼ y ∈ B | ∀ z ∈ x y + M z = z + M y = x ∈ 𝒫 B ⟼ y ∈ B | ∀ z ∈ x y + M z = z + M y
17 16 dmmptss ⊢ dom ⁡ x ∈ 𝒫 B ⟼ y ∈ B | ∀ z ∈ x y + M z = z + M y ⊆ 𝒫 B
18 15 17 eqsstrdi ⊢ X ∈ Z ⁡ S → dom ⁡ Z ⊆ 𝒫 B
19 elfvdm ⊢ X ∈ Z ⁡ S → S ∈ dom ⁡ Z
20 18 19 sseldd ⊢ X ∈ Z ⁡ S → S ∈ 𝒫 B
21 20 elpwid ⊢ X ∈ Z ⁡ S → S ⊆ B
22 11 21 jca ⊢ X ∈ Z ⁡ S → M ∈ V ∧ S ⊆ B