Theorem spanval

Description: Value of the linear span of a subset of Hilbert space. The span is the intersection of all subspaces constraining the subset. Definition of span in Schechter p. 276. (Contributed by NM, 2-Jun-2004) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	spanval	|- ( A C_ ~H -> ( span ` A ) = |^| { x e. SH | A C_ x } )

Proof

Step	Hyp	Ref	Expression
1		df-span	|- span = ( y e. ~P ~H |-> |^| { x e. SH | y C_ x } )
2		sseq1	|- ( y = A -> ( y C_ x <-> A C_ x ) )
3	2	rabbidv	|- ( y = A -> { x e. SH | y C_ x } = { x e. SH | A C_ x } )
4	3	inteqd	|- ( y = A -> |^| { x e. SH | y C_ x } = |^| { x e. SH | A C_ x } )
5		ax-hilex	|- ~H e. _V
6	5	elpw2	|- ( A e. ~P ~H <-> A C_ ~H )
7	6	biimpri	|- ( A C_ ~H -> A e. ~P ~H )
8		helsh	|- ~H e. SH
9		sseq2	|- ( x = ~H -> ( A C_ x <-> A C_ ~H ) )
10	9	rspcev	|- ( ( ~H e. SH /\ A C_ ~H ) -> E. x e. SH A C_ x )
11	8 10	mpan	|- ( A C_ ~H -> E. x e. SH A C_ x )
12		intexrab	|- ( E. x e. SH A C_ x <-> |^| { x e. SH | A C_ x } e. _V )
13	11 12	sylib	|- ( A C_ ~H -> |^| { x e. SH | A C_ x } e. _V )
14	1 4 7 13	fvmptd3	|- ( A C_ ~H -> ( span ` A ) = |^| { x e. SH | A C_ x } )