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 ⊆ ℋ ∧ y = ∩{z ∈ Sℋ ∣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 ℋ
5	3, 4	wss 1487	. . . 4 wff x ⊆ ℋ
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 Sℋ
12	10, 8, 11	crab 1204	. . . . . 6 class {z ∈ Sℋ ∣x ⊆ z}
13	12	cint 1965	. . . . 5 class ∩{z ∈ Sℋ ∣x ⊆ z}
14	7, 13	wceq 1091	. . . 4 wff y = ∩{z ∈ Sℋ ∣x ⊆ z}
15	5, 14	wa 196	. . 3 wff (x ⊆ ℋ ∧ y = ∩{z ∈ Sℋ ∣x ⊆ z})
16	15, 2, 6	copab 2055	. 2 class {⟨x, y⟩∣(x ⊆ ℋ ∧ y = ∩{z ∈ Sℋ ∣x ⊆ z})}
17	1, 16	wceq 1091	1 wff span = {⟨x, y⟩∣(x ⊆ ℋ ∧ y = ∩{z ∈ Sℋ ∣x ⊆ z})}

This definition is referenced by:  spanvalt 5300

metamath.org