Definition df-span

Description: Define the linear span of a subset of Hilbert space. Definition of span in Schechter p. 276. See spanval for its value. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	df-span	⊢ span = ( 𝑥 ∈ 𝒫 ℋ ↦ ∩ { 𝑦 ∈ Sℋ ∣ 𝑥 ⊆ 𝑦 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cspn	⊢ span
1		vx	⊢ 𝑥
2		chba	⊢ ℋ
3	2	cpw	⊢ 𝒫 ℋ
4		vy	⊢ 𝑦
5		csh	⊢ Sℋ
6	1	cv	⊢ 𝑥
7	4	cv	⊢ 𝑦
8	6 7	wss	⊢ 𝑥 ⊆ 𝑦
9	8 4 5	crab	⊢ { 𝑦 ∈ Sℋ ∣ 𝑥 ⊆ 𝑦 }
10	9	cint	⊢ ∩ { 𝑦 ∈ Sℋ ∣ 𝑥 ⊆ 𝑦 }
11	1 3 10	cmpt	⊢ ( 𝑥 ∈ 𝒫 ℋ ↦ ∩ { 𝑦 ∈ Sℋ ∣ 𝑥 ⊆ 𝑦 } )
12	0 11	wceq	⊢ span = ( 𝑥 ∈ 𝒫 ℋ ↦ ∩ { 𝑦 ∈ Sℋ ∣ 𝑥 ⊆ 𝑦 } )