Theorem elspani

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

	Ref	Expression
Hypothesis	elspan.1	|- B e. _V
Assertion	elspani	|- ( A C_ ~H -> ( B e. ( span ` A ) <-> A. x e. SH ( A C_ x -> B e. x ) ) )

Proof

Step	Hyp	Ref	Expression
1		elspan.1	|- B e. _V
2		spanval	|- ( A C_ ~H -> ( span ` A ) = |^| { x e. SH | A C_ x } )
3	2	eleq2d	|- ( A C_ ~H -> ( B e. ( span ` A ) <-> B e. |^| { x e. SH | A C_ x } ) )
4	1	elintrab	|- ( B e. |^| { x e. SH | A C_ x } <-> A. x e. SH ( A C_ x -> B e. x ) )
5	3 4	bitrdi	|- ( A C_ ~H -> ( B e. ( span ` A ) <-> A. x e. SH ( A C_ x -> B e. x ) ) )