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