Metamath Proof Explorer

Theorem cntzun

Description: The centralizer of a union is the intersection of the centralizers. (Contributed by Thierry Arnoux, 27-Nov-2023)

Ref Expression
Hypotheses cntzun.b ⊢ B = Base M
cntzun.z ⊢ Z = Cntz ⁡ M
Assertion cntzun ⊢ X ⊆ B ∧ Y ⊆ B → Z ⁡ X ∪ Y = Z ⁡ X ∩ Z ⁡ Y

Proof

Step Hyp Ref Expression
1 cntzun.b ⊢ B = Base M
2 cntzun.z ⊢ Z = Cntz ⁡ M
3 ralunb ⊢ ∀ y ∈ X ∪ Y x + M y = y + M x ↔ ∀ y ∈ X x + M y = y + M x ∧ ∀ y ∈ Y x + M y = y + M x
4 3 a1i ⊢ X ⊆ B ∧ Y ⊆ B ∧ x ∈ B → ∀ y ∈ X ∪ Y x + M y = y + M x ↔ ∀ y ∈ X x + M y = y + M x ∧ ∀ y ∈ Y x + M y = y + M x
5 4 pm5.32da ⊢ X ⊆ B ∧ Y ⊆ B → x ∈ B ∧ ∀ y ∈ X ∪ Y x + M y = y + M x ↔ x ∈ B ∧ ∀ y ∈ X x + M y = y + M x ∧ ∀ y ∈ Y x + M y = y + M x
6 anandi ⊢ x ∈ B ∧ ∀ y ∈ X x + M y = y + M x ∧ ∀ y ∈ Y x + M y = y + M x ↔ x ∈ B ∧ ∀ y ∈ X x + M y = y + M x ∧ x ∈ B ∧ ∀ y ∈ Y x + M y = y + M x
7 5 6 bitrdi ⊢ X ⊆ B ∧ Y ⊆ B → x ∈ B ∧ ∀ y ∈ X ∪ Y x + M y = y + M x ↔ x ∈ B ∧ ∀ y ∈ X x + M y = y + M x ∧ x ∈ B ∧ ∀ y ∈ Y x + M y = y + M x
8 unss ⊢ X ⊆ B ∧ Y ⊆ B ↔ X ∪ Y ⊆ B
9 eqid ⊢ + M = + M
10 1 9 2 elcntz ⊢ X ∪ Y ⊆ B → x ∈ Z ⁡ X ∪ Y ↔ x ∈ B ∧ ∀ y ∈ X ∪ Y x + M y = y + M x
11 8 10 sylbi ⊢ X ⊆ B ∧ Y ⊆ B → x ∈ Z ⁡ X ∪ Y ↔ x ∈ B ∧ ∀ y ∈ X ∪ Y x + M y = y + M x
12 1 9 2 elcntz ⊢ X ⊆ B → x ∈ Z ⁡ X ↔ x ∈ B ∧ ∀ y ∈ X x + M y = y + M x
13 1 9 2 elcntz ⊢ Y ⊆ B → x ∈ Z ⁡ Y ↔ x ∈ B ∧ ∀ y ∈ Y x + M y = y + M x
14 12 13 bi2anan9 ⊢ X ⊆ B ∧ Y ⊆ B → x ∈ Z ⁡ X ∧ x ∈ Z ⁡ Y ↔ x ∈ B ∧ ∀ y ∈ X x + M y = y + M x ∧ x ∈ B ∧ ∀ y ∈ Y x + M y = y + M x
15 7 11 14 3bitr4d ⊢ X ⊆ B ∧ Y ⊆ B → x ∈ Z ⁡ X ∪ Y ↔ x ∈ Z ⁡ X ∧ x ∈ Z ⁡ Y
16 elin ⊢ x ∈ Z ⁡ X ∩ Z ⁡ Y ↔ x ∈ Z ⁡ X ∧ x ∈ Z ⁡ Y
17 15 16 bitr4di ⊢ X ⊆ B ∧ Y ⊆ B → x ∈ Z ⁡ X ∪ Y ↔ x ∈ Z ⁡ X ∩ Z ⁡ Y
18 17 eqrdv ⊢ X ⊆ B ∧ Y ⊆ B → Z ⁡ X ∪ Y = Z ⁡ X ∩ Z ⁡ Y