This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cntzssv

Description: The centralizer is unconditionally a subset. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses cntzrcl.b 
|- B = ( Base ` M )
cntzrcl.z 
|- Z = ( Cntz ` M )
Assertion cntzssv 
|- ( Z ` S ) C_ B

Proof

Step Hyp Ref Expression
1 cntzrcl.b 
 |-  B = ( Base ` M )
2 cntzrcl.z 
 |-  Z = ( Cntz ` M )
3 0ss 
 |-  (/) C_ B
4 sseq1 
 |-  ( ( Z ` S ) = (/) -> ( ( Z ` S ) C_ B <-> (/) C_ B ) )
5 3 4 mpbiri 
 |-  ( ( Z ` S ) = (/) -> ( Z ` S ) C_ B )
6 n0 
 |-  ( ( Z ` S ) =/= (/) <-> E. x x e. ( Z ` S ) )
7 1 2 cntzrcl 
 |-  ( x e. ( Z ` S ) -> ( M e. _V /\ S C_ B ) )
8 eqid 
 |-  ( +g ` M ) = ( +g ` M )
9 1 8 2 cntzval 
 |-  ( S C_ B -> ( Z ` S ) = { x e. B | A. y e. S ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) } )
10 7 9 simpl2im 
 |-  ( x e. ( Z ` S ) -> ( Z ` S ) = { x e. B | A. y e. S ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) } )
11 ssrab2 
 |-  { x e. B | A. y e. S ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) } C_ B
12 10 11 eqsstrdi 
 |-  ( x e. ( Z ` S ) -> ( Z ` S ) C_ B )
13 12 exlimiv 
 |-  ( E. x x e. ( Z ` S ) -> ( Z ` S ) C_ B )
14 6 13 sylbi 
 |-  ( ( Z ` S ) =/= (/) -> ( Z ` S ) C_ B )
15 5 14 pm2.61ine 
 |-  ( Z ` S ) C_ B