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 ⊢ B = Base M
cntzrec.z ⊢ Z = Cntz ⁡ M
Assertion cntziinsn ⊢ S ⊆ B → Z ⁡ S = B ∩ ⋂ x ∈ S Z ⁡ x

Proof

Step Hyp Ref Expression
1 cntzrec.b ⊢ B = Base M
2 cntzrec.z ⊢ Z = Cntz ⁡ M
3 eqid ⊢ + M = + M
4 1 3 2 cntzval ⊢ S ⊆ B → Z ⁡ S = y ∈ B | ∀ x ∈ S y + M x = x + M y
5 ssel2 ⊢ S ⊆ B ∧ x ∈ S → x ∈ B
6 1 3 2 cntzsnval ⊢ x ∈ B → Z ⁡ x = y ∈ B | y + M x = x + M y
7 5 6 syl ⊢ S ⊆ B ∧ x ∈ S → Z ⁡ x = y ∈ B | y + M x = x + M y
8 7 iineq2dv ⊢ S ⊆ B → ⋂ x ∈ S Z ⁡ x = ⋂ x ∈ S y ∈ B | y + M x = x + M y
9 8 ineq2d ⊢ S ⊆ B → B ∩ ⋂ x ∈ S Z ⁡ x = B ∩ ⋂ x ∈ S y ∈ B | y + M x = x + M y
10 riinrab ⊢ B ∩ ⋂ x ∈ S y ∈ B | y + M x = x + M y = y ∈ B | ∀ x ∈ S y + M x = x + M y
11 9 10 eqtrdi ⊢ S ⊆ B → B ∩ ⋂ x ∈ S Z ⁡ x = y ∈ B | ∀ x ∈ S y + M x = x + M y
12 4 11 eqtr4d ⊢ S ⊆ B → Z ⁡ S = B ∩ ⋂ x ∈ S Z ⁡ x