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

Metamath Proof Explorer

Theorem spanval

Description: Value of the linear span of a subset of Hilbert space. The span is the intersection of all subspaces constraining the subset. Definition of span in Schechter p. 276. (Contributed by NM, 2-Jun-2004) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion spanval ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )

Proof

Step Hyp Ref Expression
1 df-span ⊢ span = ( 𝑦 ∈ 𝒫 ℋ ↦ ∩ { 𝑥 ∈ Sℋ ∣ 𝑦 ⊆ 𝑥 } )
2 sseq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥 ) )
3 2 rabbidv ⊢ ( 𝑦 = 𝐴 → { 𝑥 ∈ Sℋ ∣ 𝑦 ⊆ 𝑥 } = { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )
4 3 inteqd ⊢ ( 𝑦 = 𝐴 → ∩ { 𝑥 ∈ Sℋ ∣ 𝑦 ⊆ 𝑥 } = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )
5 ax-hilex ⊢ ℋ ∈ V
6 5 elpw2 ⊢ ( 𝐴 ∈ 𝒫 ℋ ↔ 𝐴 ⊆ ℋ )
7 6 biimpri ⊢ ( 𝐴 ⊆ ℋ → 𝐴 ∈ 𝒫 ℋ )
8 helsh ⊢ ℋ ∈ Sℋ
9 sseq2 ⊢ ( 𝑥 = ℋ → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ℋ ) )
10 9 rspcev ⊢ ( ( ℋ ∈ Sℋ ∧ 𝐴 ⊆ ℋ ) → ∃ 𝑥 ∈ Sℋ 𝐴 ⊆ 𝑥 )
11 8 10 mpan ⊢ ( 𝐴 ⊆ ℋ → ∃ 𝑥 ∈ Sℋ 𝐴 ⊆ 𝑥 )
12 intexrab ⊢ ( ∃ 𝑥 ∈ Sℋ 𝐴 ⊆ 𝑥 ↔ ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ∈ V )
13 11 12 sylib ⊢ ( 𝐴 ⊆ ℋ → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ∈ V )
14 1 4 7 13 fvmptd3 ⊢ ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )