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 ⊢ A ⊆ ℋ → span ⁡ A ∈ S ℋ

Proof

Step Hyp Ref Expression
1 spanval ⊢ A ⊆ ℋ → span ⁡ A = ⋂ x ∈ S ℋ | A ⊆ x
2 ssrab2 ⊢ x ∈ S ℋ | A ⊆ x ⊆ S ℋ
3 helsh ⊢ ℋ ∈ S ℋ
4 sseq2 ⊢ x = ℋ → A ⊆ x ↔ A ⊆ ℋ
5 4 rspcev ⊢ ℋ ∈ S ℋ ∧ A ⊆ ℋ → ∃ x ∈ S ℋ A ⊆ x
6 3 5 mpan ⊢ A ⊆ ℋ → ∃ x ∈ S ℋ A ⊆ x
7 rabn0 ⊢ x ∈ S ℋ | A ⊆ x ≠ ∅ ↔ ∃ x ∈ S ℋ A ⊆ x
8 6 7 sylibr ⊢ A ⊆ ℋ → x ∈ S ℋ | A ⊆ x ≠ ∅
9 shintcl ⊢ x ∈ S ℋ | A ⊆ x ⊆ S ℋ ∧ x ∈ S ℋ | A ⊆ x ≠ ∅ → ⋂ x ∈ S ℋ | A ⊆ x ∈ S ℋ
10 2 8 9 sylancr ⊢ A ⊆ ℋ → ⋂ x ∈ S ℋ | A ⊆ x ∈ S ℋ
11 1 10 eqeltrd ⊢ A ⊆ ℋ → span ⁡ A ∈ S ℋ