Definition df-span 9274

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

Assertion

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

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-span

Step	Hyp	Ref	Expression
1		cspn 8801	. 2 class span
2		vx	. . . . . 6 set x
3	2	cv 955	. . . . 5 class x
4		chil 8788	. . . . 5 class H~
5	3, 4	wss 2047	. . . 4 wff x (_ H~
6		vy	. . . . . 6 set y
7	6	cv 955	. . . . 5 class y
8		vz	. . . . . . . . 9 set z
9	8	cv 955	. . . . . . . 8 class z
10	3, 9	wss 2047	. . . . . . 7 wff x (_ z
11		csh 8797	. . . . . . 7 class SH
12	10, 8, 11	crab 1648	. . . . . 6 class {z e. SH | x (_ z}
13	12	cint 2533	. . . . 5 class |^|{z e. SH | x (_ z}
14	7, 13	wceq 956	. . . 4 wff y = |^|{z e. SH | x (_ z}
15	5, 14	wa 223	. . 3 wff (x (_ H~ /\ y = |^|{z e. SH | x (_ z})
16	15, 2, 6	copab 2666	. 2 class {<.x, y>. | (x (_ H~ /\ y = |^|{z e. SH | x (_ z})}
17	1, 16	wceq 956	1 wff span = {<.x, y>. | (x (_ H~ /\ y = |^|{z e. SH | x (_ z})}

This definition is referenced by:  spanvalt 9299

Copyright terms: Public domain