Definition df-span 5276

Description: Define the linear span of a subset of Hilbert space. Definition of span in [Schechter] p. 276. See spanvalt 5300 for its value.

Assertion

Ref	Expression
df-span	|- span = {<.x, y>. | (x (_ H~ /\ y = |^|{z e. SH | x (_ z})}

Distinct variable group(s):   x,y,z

Detailed syntax breakdown of Definition df-span

Step	Hyp	Ref	Expression
1		cspn 4971	. 2 class span
2		vx	. . . . . 6 set x
3	2	cv 1089	. . . . 5 class x
4		chil 4958	. . . . 5 class H~
5	3, 4	wss 1487	. . . 4 wff x (_ H~
6		vy	. . . . . 6 set y
7	6	cv 1089	. . . . 5 class y
8		vz	. . . . . . . . 9 set z
9	8	cv 1089	. . . . . . . 8 class z
10	3, 9	wss 1487	. . . . . . 7 wff x (_ z
11		csh 4967	. . . . . . 7 class SH
12	10, 8, 11	crab 1204	. . . . . 6 class {z e. SH | x (_ z}
13	12	cint 1965	. . . . 5 class |^|{z e. SH | x (_ z}
14	7, 13	wceq 1091	. . . 4 wff y = |^|{z e. SH | x (_ z}
15	5, 14	wa 196	. . 3 wff (x (_ H~ /\ y = |^|{z e. SH | x (_ z})
16	15, 2, 6	copab 2055	. 2 class {<.x, y>. | (x (_ H~ /\ y = |^|{z e. SH | x (_ z})}
17	1, 16	wceq 1091	1 wff span = {<.x, y>. | (x (_ H~ /\ y = |^|{z e. SH | x (_ z})}

This definition is referenced by:  spanvalt 5300

metamath.org