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 } ) |
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 } ) |