Definition df-span

Description: Define the linear span of a subset of Hilbert space. Definition of span in Schechter p. 276. See spanval for its value. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	df-span	|- span = ( x e. ~P ~H |-> |^| { y e. SH | x C_ y } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cspn	|- span
1		vx	|- x
2		chba	|- ~H
3	2	cpw	|- ~P ~H
4		vy	|- y
5		csh	|- SH
6	1	cv	|- x
7	4	cv	|- y
8	6 7	wss	|- x C_ y
9	8 4 5	crab	|- { y e. SH | x C_ y }
10	9	cint	|- |^| { y e. SH | x C_ y }
11	1 3 10	cmpt	|- ( x e. ~P ~H |-> |^| { y e. SH | x C_ y } )
12	0 11	wceq	|- span = ( x e. ~P ~H |-> |^| { y e. SH | x C_ y } )