Metamath Proof Explorer

Theorem spansn

Description: The span of a singleton in Hilbert space equals its closure. (Contributed by NM, 4-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spansn ⊢ A ∈ ℋ → span ⁡ A = ⊥ ⁡ ⊥ ⁡ A

Proof

Step Hyp Ref Expression
1 sneq ⊢ A = if A ∈ ℋ A 0 ℎ → A = if A ∈ ℋ A 0 ℎ
2 1 fveq2d ⊢ A = if A ∈ ℋ A 0 ℎ → span ⁡ A = span ⁡ if A ∈ ℋ A 0 ℎ
3 1 fveq2d ⊢ A = if A ∈ ℋ A 0 ℎ → ⊥ ⁡ A = ⊥ ⁡ if A ∈ ℋ A 0 ℎ
4 3 fveq2d ⊢ A = if A ∈ ℋ A 0 ℎ → ⊥ ⁡ ⊥ ⁡ A = ⊥ ⁡ ⊥ ⁡ if A ∈ ℋ A 0 ℎ
5 2 4 eqeq12d ⊢ A = if A ∈ ℋ A 0 ℎ → span ⁡ A = ⊥ ⁡ ⊥ ⁡ A ↔ span ⁡ if A ∈ ℋ A 0 ℎ = ⊥ ⁡ ⊥ ⁡ if A ∈ ℋ A 0 ℎ
6 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
7 6 spansni ⊢ span ⁡ if A ∈ ℋ A 0 ℎ = ⊥ ⁡ ⊥ ⁡ if A ∈ ℋ A 0 ℎ
8 5 7 dedth ⊢ A ∈ ℋ → span ⁡ A = ⊥ ⁡ ⊥ ⁡ A