Definition df-span 28168

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

Assertion

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

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-span

Step	Hyp	Ref	Expression
1		cspn 27789	. 2 class span
2		vx	. . 3 setvar x
3		chil 27776	. . . 4 class ~H
4	3	cpw 4158	. . 3 class ~P ~H
5	2	cv 1482	. . . . . 6 class x
6		vy	. . . . . . 7 setvar y
7	6	cv 1482	. . . . . 6 class y
8	5, 7	wss 3574	. . . . 5 wff x C_ y
9		csh 27785	. . . . 5 class SH
10	8, 6, 9	crab 2916	. . . 4 class { y e. SH | x C_ y }
11	10	cint 4475	. . 3 class |^| { y e. SH | x C_ y }
12	2, 4, 11	cmpt 4729	. 2 class ( x e. ~P ~H |-> |^| { y e. SH | x C_ y } )
13	1, 12	wceq 1483	1 wff span = ( x e. ~P ~H |-> |^| { y e. SH | x C_ y } )

This definition is referenced by:  spanval  28192