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

Metamath Proof Explorer

Theorem spanssoc

Description: The span of a subset of Hilbert space is less than or equal to its closure (double orthogonal complement). (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spanssoc 
|- ( A C_ ~H -> ( span ` A ) C_ ( _|_ ` ( _|_ ` A ) ) )

Proof

Step Hyp Ref Expression
1 ocss 
 |-  ( A C_ ~H -> ( _|_ ` A ) C_ ~H )
2 ocss 
 |-  ( ( _|_ ` A ) C_ ~H -> ( _|_ ` ( _|_ ` A ) ) C_ ~H )
3 1 2 syl 
 |-  ( A C_ ~H -> ( _|_ ` ( _|_ ` A ) ) C_ ~H )
4 ococss 
 |-  ( A C_ ~H -> A C_ ( _|_ ` ( _|_ ` A ) ) )
5 spanss 
 |-  ( ( ( _|_ ` ( _|_ ` A ) ) C_ ~H /\ A C_ ( _|_ ` ( _|_ ` A ) ) ) -> ( span ` A ) C_ ( span ` ( _|_ ` ( _|_ ` A ) ) ) )
6 3 4 5 syl2anc 
 |-  ( A C_ ~H -> ( span ` A ) C_ ( span ` ( _|_ ` ( _|_ ` A ) ) ) )
7 ocsh 
 |-  ( ( _|_ ` A ) C_ ~H -> ( _|_ ` ( _|_ ` A ) ) e. SH )
8 spanid 
 |-  ( ( _|_ ` ( _|_ ` A ) ) e. SH -> ( span ` ( _|_ ` ( _|_ ` A ) ) ) = ( _|_ ` ( _|_ ` A ) ) )
9 1 7 8 3syl 
 |-  ( A C_ ~H -> ( span ` ( _|_ ` ( _|_ ` A ) ) ) = ( _|_ ` ( _|_ ` A ) ) )
10 6 9 sseqtrd 
 |-  ( A C_ ~H -> ( span ` A ) C_ ( _|_ ` ( _|_ ` A ) ) )