This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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ℋ ∣ 𝑥 ⊆ 𝑦 } )