Theorem spansnch

Description: The span of a Hilbert space singleton belongs to the Hilbert lattice. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	spansnch	|- ( A e. ~H -> ( span ` { A } ) e. CH )

Proof

Step	Hyp	Ref	Expression
1		spansn	|- ( A e. ~H -> ( span ` { A } ) = ( _|_ ` ( _|_ ` { A } ) ) )
2		snssi	|- ( A e. ~H -> { A } C_ ~H )
3		occl	|- ( { A } C_ ~H -> ( _|_ ` { A } ) e. CH )
4		choccl	|- ( ( _|_ ` { A } ) e. CH -> ( _|_ ` ( _|_ ` { A } ) ) e. CH )
5	2 3 4	3syl	|- ( A e. ~H -> ( _|_ ` ( _|_ ` { A } ) ) e. CH )
6	1 5	eqeltrd	|- ( A e. ~H -> ( span ` { A } ) e. CH )