Description: A subspace of Hilbert space is its own span. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | spanid | ⊢ ( 𝐴 ∈ Sℋ → ( span ‘ 𝐴 ) = 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | shss | ⊢ ( 𝐴 ∈ Sℋ → 𝐴 ⊆ ℋ ) | |
2 | spanval | ⊢ ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ) | |
3 | 1 2 | syl | ⊢ ( 𝐴 ∈ Sℋ → ( span ‘ 𝐴 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ) |
4 | intmin | ⊢ ( 𝐴 ∈ Sℋ → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } = 𝐴 ) | |
5 | 3 4 | eqtrd | ⊢ ( 𝐴 ∈ Sℋ → ( span ‘ 𝐴 ) = 𝐴 ) |