Definition df-span 9212

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

Assertion

Ref	Expression
df-span	⊢ span = {⟨x, y⟩∣(x ⊆ ℋ ⋀ y = ∩{z ∈ Sℋ ∣x ⊆ z})}

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-span

Step	Hyp	Ref	Expression
1		cspn 8740	. 2 class span
2		vx	. . . . . 6 set x
3	2	cv 953	. . . . 5 class x
4		chil 8727	. . . . 5 class ℋ
5	3, 4	wss 2043	. . . 4 wff x ⊆ ℋ
6		vy	. . . . . 6 set y
7	6	cv 953	. . . . 5 class y
8		vz	. . . . . . . . 9 set z
9	8	cv 953	. . . . . . . 8 class z
10	3, 9	wss 2043	. . . . . . 7 wff x ⊆ z
11		csh 8736	. . . . . . 7 class Sℋ
12	10, 8, 11	crab 1645	. . . . . 6 class {z ∈ Sℋ ∣x ⊆ z}
13	12	cint 2528	. . . . 5 class ∩{z ∈ Sℋ ∣x ⊆ z}
14	7, 13	wceq 954	. . . 4 wff y = ∩{z ∈ Sℋ ∣x ⊆ z}
15	5, 14	wa 223	. . 3 wff (x ⊆ ℋ ⋀ y = ∩{z ∈ Sℋ ∣x ⊆ z})
16	15, 2, 6	copab 2661	. 2 class {⟨x, y⟩∣(x ⊆ ℋ ⋀ y = ∩{z ∈ Sℋ ∣x ⊆ z})}
17	1, 16	wceq 954	1 wff span = {⟨x, y⟩∣(x ⊆ ℋ ⋀ y = ∩{z ∈ Sℋ ∣x ⊆ z})}

This definition is referenced by:  spanvalt 9237

Copyright terms: Public domain