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

Metamath Proof Explorer

Theorem spancl

Description: The span of a subset of Hilbert space is a subspace. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spancl ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) ∈ Sℋ )

Proof

Step Hyp Ref Expression
1 spanval ⊢ ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )
2 ssrab2 ⊢ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ Sℋ
3 helsh ⊢ ℋ ∈ Sℋ
4 sseq2 ⊢ ( 𝑥 = ℋ → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ℋ ) )
5 4 rspcev ⊢ ( ( ℋ ∈ Sℋ ∧ 𝐴 ⊆ ℋ ) → ∃ 𝑥 ∈ Sℋ 𝐴 ⊆ 𝑥 )
6 3 5 mpan ⊢ ( 𝐴 ⊆ ℋ → ∃ 𝑥 ∈ Sℋ 𝐴 ⊆ 𝑥 )
7 rabn0 ⊢ ( { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ≠ ∅ ↔ ∃ 𝑥 ∈ Sℋ 𝐴 ⊆ 𝑥 )
8 6 7 sylibr ⊢ ( 𝐴 ⊆ ℋ → { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ≠ ∅ )
9 shintcl ⊢ ( ( { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ Sℋ ∧ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ≠ ∅ ) → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ∈ Sℋ )
10 2 8 9 sylancr ⊢ ( 𝐴 ⊆ ℋ → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ∈ Sℋ )
11 1 10 eqeltrd ⊢ ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) ∈ Sℋ )