Theorem spancl

Description: The span of a subset of Hilbert space is a subspace. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	spancl	|- ( A C_ ~H -> ( span ` A ) e. SH )

Proof

Step	Hyp	Ref	Expression
1		spanval	|- ( A C_ ~H -> ( span ` A ) = |^| { x e. SH | A C_ x } )
2		ssrab2	|- { x e. SH | A C_ x } C_ SH
3		helsh	|- ~H e. SH
4		sseq2	|- ( x = ~H -> ( A C_ x <-> A C_ ~H ) )
5	4	rspcev	|- ( ( ~H e. SH /\ A C_ ~H ) -> E. x e. SH A C_ x )
6	3 5	mpan	|- ( A C_ ~H -> E. x e. SH A C_ x )
7		rabn0	|- ( { x e. SH | A C_ x } =/= (/) <-> E. x e. SH A C_ x )
8	6 7	sylibr	|- ( A C_ ~H -> { x e. SH | A C_ x } =/= (/) )
9		shintcl	|- ( ( { x e. SH | A C_ x } C_ SH /\ { x e. SH | A C_ x } =/= (/) ) -> |^| { x e. SH | A C_ x } e. SH )
10	2 8 9	sylancr	|- ( A C_ ~H -> |^| { x e. SH | A C_ x } e. SH )
11	1 10	eqeltrd	|- ( A C_ ~H -> ( span ` A ) e. SH )