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 𝒫 y S | x y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cspn class span
1 vx setvar x
2 chba class
3 2 cpw class 𝒫
4 vy setvar y
5 csh class S
6 1 cv setvar x
7 4 cv setvar y
8 6 7 wss wff x y
9 8 4 5 crab class y S | x y
10 9 cint class y S | x y
11 1 3 10 cmpt class x 𝒫 y S | x y
12 0 11 wceq wff span = x 𝒫 y S | x y