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 C_ B -> ( Z ` S ) = ( B i^i |^|_ x e. S ( Z ` { x } ) ) )

Proof

Step Hyp Ref Expression
1 cntzrec.b 
 |-  B = ( Base ` M )
2 cntzrec.z 
 |-  Z = ( Cntz ` M )
3 eqid 
 |-  ( +g ` M ) = ( +g ` M )
4 1 3 2 cntzval 
 |-  ( S C_ B -> ( Z ` S ) = { y e. B | A. x e. S ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) } )
5 ssel2 
 |-  ( ( S C_ B /\ x e. S ) -> x e. B )
6 1 3 2 cntzsnval 
 |-  ( x e. B -> ( Z ` { x } ) = { y e. B | ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) } )
7 5 6 syl 
 |-  ( ( S C_ B /\ x e. S ) -> ( Z ` { x } ) = { y e. B | ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) } )
8 7 iineq2dv 
 |-  ( S C_ B -> |^|_ x e. S ( Z ` { x } ) = |^|_ x e. S { y e. B | ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) } )
9 8 ineq2d 
 |-  ( S C_ B -> ( B i^i |^|_ x e. S ( Z ` { x } ) ) = ( B i^i |^|_ x e. S { y e. B | ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) } ) )
10 riinrab 
 |-  ( B i^i |^|_ x e. S { y e. B | ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) } ) = { y e. B | A. x e. S ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) }
11 9 10 eqtrdi 
 |-  ( S C_ B -> ( B i^i |^|_ x e. S ( Z ` { x } ) ) = { y e. B | A. x e. S ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) } )
12 4 11 eqtr4d 
 |-  ( S C_ B -> ( Z ` S ) = ( B i^i |^|_ x e. S ( Z ` { x } ) ) )