Editing Von Neumann bicommutant theorem (section)

== Proof ==
Let {{mvar|H}} be a Hilbert space and {{math|''L''(''H'')}} the bounded operators on {{mvar|H}}. Consider a self-adjoint unital [[subalgebra]] {{math|'''M'''}} of {{math|''L''(''H'')}} (this means that {{math|'''M'''}} contains the adjoints of its members, and the identity operator on {{mvar|H}}).

The theorem is equivalent to the combination of the following three statements:

:(i) {{math|cl<sub>''W''</sub>('''M''') ⊆ '''M'''′′}}
:(ii) {{math|cl<sub>''S''</sub>('''M''') ⊆ cl<sub>''W''</sub>('''M''')}}
:(iii) {{math|'''M'''′′ ⊆ cl<sub>''S''</sub>('''M''')}}

where the {{mvar|W}} and {{mvar|S}} subscripts stand for [[Closure (topology)|closure]]s in the [[weak operator topology|weak]] and [[strong operator topology|strong]] operator topologies, respectively.

===Proof of (i)===
For any {{mvar|x}} and {{mvar|y}} in {{mvar|H}}, the map ''T'' → <''Tx'', ''y''> is continuous in the weak operator topology, by its definition. Therefore, for any fixed operator {{mvar|O}}, so is the map

:<math>T \to \langle (OT - TO)x, y\rangle = \langle Tx, O^*y\rangle - \langle TOx, y\rangle </math>

Let ''S'' be any subset of {{math|''L''(''H'')}}, and ''S''′ its [[commutant]]. For any operator {{mvar|T}} in ''S''′, this function is zero for all ''O'' in ''S''. For any {{mvar|T}} not in ''S''′, it must be nonzero for some ''O'' in ''S'' and some ''x'' and ''y'' in {{mvar|H}}. By its continuity there is an open neighborhood of {{mvar|T}} for the weak operator topology on which it is nonzero, and which therefore is also not in ''S''′. Hence any commutant ''S''′ is [[Closed set|closed]] in the weak operator topology.  In particular, so is {{math|'''M'''′′}}; since it contains {{math|'''M'''}}, it also contains its weak operator closure.

===Proof of (ii)===
This follows directly from the weak operator topology being coarser than the strong operator topology: for every point {{mvar|x}} in {{math|cl<sub>''S''</sub>('''M''')}}, every open neighborhood of {{mvar|x}} in the weak operator topology is also open in the strong operator topology and therefore contains a member of {{math|'''M'''}}; therefore {{mvar|x}} is also a member of {{math|cl<sub>''W''</sub>('''M''')}}.

===Proof of (iii)===
Fix {{math|''X'' ∈ '''M'''′′}}. We must show that {{math|''X'' ∈ cl<sub>''S''</sub>('''M''')}}, i.e. for each ''h'' ∈ ''H'' and any {{math|''ε'' > 0}}, there exists ''T'' in {{math|'''M'''}} with {{math|{{!!}}''Xh'' − ''Th''{{!!}} < ''ε''}}.

Fix ''h'' in {{mvar|H}}. The [[Cyclic subspace | cyclic subspace]] {{math|'''M'''''h'' {{=}} {''Mh'' : ''M'' ∈ '''M'''}}} is invariant under the action of any ''T'' in {{math|'''M'''}}. Its [[Closure (topology)|closure]] {{math|cl('''M'''''h'')}} in the norm of ''H'' is a closed linear subspace, with corresponding [[orthogonal projection]] {{mvar|P}} : ''H'' → {{math|cl('''M'''''h'')}} in ''L''(''H''). In fact, this ''P'' is in {{math|'''M'''′}}, as we now show.

:'''Lemma.''' {{math|''P'' ∈ '''M'''′}}.

:'''Proof.''' Fix {{math|''x'' ∈ ''H''}}. As {{math|''Px'' ∈ cl('''M'''''h'')}}, it is the limit of a sequence {{mvar|O<sub>n</sub>h}} with {{mvar|O<sub>n</sub>}} in {{math|'''M'''}}. For any {{math|''T'' ∈ '''M'''}}, {{mvar|TO<sub>n</sub>h}} is also in {{math|'''M'''''h''}}, and by the continuity of {{mvar|T}}, this sequence converges to {{mvar|TPx}}. So {{math|''TPx'' ∈ cl('''M'''''h'')}}, and hence ''PTPx'' = ''TPx''. Since ''x'' was arbitrary, we have ''PTP'' = ''TP'' for all {{mvar|T}} in {{math|'''M'''}}.  

:Since {{math|'''M'''}} is closed under the adjoint operation and ''P'' is [[self-adjoint operator|self-adjoint]], for any {{math|''x'', ''y'' ∈ ''H''}} we have

::<math>\langle x,TPy\rangle = \langle x,PTPy\rangle = \langle (PTP)^*x,y\rangle = \langle PT^*Px,y\rangle = \langle T^*Px,y\rangle = \langle Px,Ty\rangle = \langle x,PTy\rangle</math>

:So ''TP'' = ''PT'' for all {{math|''T'' ∈ '''M'''}}, meaning ''P'' lies in {{math|'''M'''′}}.

By definition of the [[bicommutant]], we must have ''XP'' = ''PX''. Since {{math|'''M'''}} is unital, {{math|''h'' ∈ '''M'''''h''}}, and so {{math| ''h'' {{=}} ''Ph''}}. Hence {{math|''Xh'' {{=}} ''XPh'' {{=}} ''PXh'' ∈ cl('''M'''''h'')}}. So for each {{math|''ε'' > 0}}, there exists ''T'' in {{math|'''M'''}} with {{math|{{!!}}''Xh'' − ''Th''{{!!}} < ''ε''}}, i.e. {{mvar|X}} is in the strong operator closure of {{math|'''M'''}}.

=== Non-unital case ===
A C*-algebra {{math|'''M'''}} acting on '''H''' is said to act ''non-degenerately'' if for ''h'' in {{mvar|H}}, {{math|'''M'''''h'' {{=}} {0} }} implies {{math|''h'' {{=}} 0}}. In this case, it can be shown using an [[approximate identity]] in {{math|'''M'''}} that the identity operator ''I'' lies in the strong closure of {{math|'''M'''}}. Therefore, the conclusion of the bicommutant theorem holds for {{math|'''M'''}}.