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 ) ) )