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

Metamath Proof Explorer

Theorem spanid

Description: A subspace of Hilbert space is its own span. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spanid ⊢ A ∈ S ℋ → span ⁡ A = A

Proof

Step Hyp Ref Expression
1 shss ⊢ A ∈ S ℋ → A ⊆ ℋ
2 spanval ⊢ A ⊆ ℋ → span ⁡ A = ⋂ x ∈ S ℋ | A ⊆ x
3 1 2 syl ⊢ A ∈ S ℋ → span ⁡ A = ⋂ x ∈ S ℋ | A ⊆ x
4 intmin ⊢ A ∈ S ℋ → ⋂ x ∈ S ℋ | A ⊆ x = A
5 3 4 eqtrd ⊢ A ∈ S ℋ → span ⁡ A = A