Theorem spanid

Description: A subspace of Hilbert space is its own span. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	spanid	|- ( A e. SH -> ( span ` A ) = A )

Proof

Step	Hyp	Ref	Expression
1		shss	|- ( A e. SH -> A C_ ~H )
2		spanval	|- ( A C_ ~H -> ( span ` A ) = |^| { x e. SH | A C_ x } )
3	1 2	syl	|- ( A e. SH -> ( span ` A ) = |^| { x e. SH | A C_ x } )
4		intmin	|- ( A e. SH -> |^| { x e. SH | A C_ x } = A )
5	3 4	eqtrd	|- ( A e. SH -> ( span ` A ) = A )