Definition df-span 10699

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

Assertion

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

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-span

Step	Hyp	Ref	Expression
1		cspn 10225	. 2 class span
2		vx	. . . . . 6 set x
3	2	cv 1135	. . . . 5 class x
4		chil 10212	. . . . 5 class ~H
5	3, 4	wss 2426	. . . 4 wff x C_ ~H
6		vy	. . . . . 6 set y
7	6	cv 1135	. . . . 5 class y
8		vz	. . . . . . . . 9 set z
9	8	cv 1135	. . . . . . . 8 class z
10	3, 9	wss 2426	. . . . . . 7 wff x C_ z
11		csh 10221	. . . . . . 7 class SH
12	10, 8, 11	crab 1942	. . . . . 6 class {z e. SH | x C_ z}
13	12	cint 3036	. . . . 5 class |^|{z e. SH | x C_ z}
14	7, 13	wceq 1136	. . . 4 wff y = |^|{z e. SH | x C_ z}
15	5, 14	wa 239	. . 3 wff (x C_ ~H /\ y = |^|{z e. SH | x C_ z})
16	15, 2, 6	copab 3213	. 2 class {<.x, y>. | (x C_ ~H /\ y = |^|{z e. SH | x C_ z})}
17	1, 16	wceq 1136	1 wff span = {<.x, y>. | (x C_ ~H /\ y = |^|{z e. SH | x C_ z})}

This definition is referenced by:  spanval 10724

Copyright terms: Public domain