Metamath Proof Explorer


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