Metamath Proof Explorer

Theorem spansni

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

Ref Expression
Hypothesis spansn.1 ⊢ A ∈ ℋ
Assertion spansni ⊢ span ⁡ A = ⊥ ⁡ ⊥ ⁡ A

Proof

Step Hyp Ref Expression
1 spansn.1 ⊢ A ∈ ℋ
2 snssi ⊢ A ∈ ℋ → A ⊆ ℋ
3 spanssoc ⊢ A ⊆ ℋ → span ⁡ A ⊆ ⊥ ⁡ ⊥ ⁡ A
4 1 2 3 mp2b ⊢ span ⁡ A ⊆ ⊥ ⁡ ⊥ ⁡ A
5 1 elexi ⊢ A ∈ V
6 5 snss ⊢ A ∈ y ↔ A ⊆ y
7 shmulcl ⊢ y ∈ S ℋ ∧ z ∈ ℂ ∧ A ∈ y → z ⋅ ℎ A ∈ y
8 7 3expia ⊢ y ∈ S ℋ ∧ z ∈ ℂ → A ∈ y → z ⋅ ℎ A ∈ y
9 8 ancoms ⊢ z ∈ ℂ ∧ y ∈ S ℋ → A ∈ y → z ⋅ ℎ A ∈ y
10 6 9 biimtrrid ⊢ z ∈ ℂ ∧ y ∈ S ℋ → A ⊆ y → z ⋅ ℎ A ∈ y
11 eleq1 ⊢ x = z ⋅ ℎ A → x ∈ y ↔ z ⋅ ℎ A ∈ y
12 11 imbi2d ⊢ x = z ⋅ ℎ A → A ⊆ y → x ∈ y ↔ A ⊆ y → z ⋅ ℎ A ∈ y
13 10 12 syl5ibrcom ⊢ z ∈ ℂ ∧ y ∈ S ℋ → x = z ⋅ ℎ A → A ⊆ y → x ∈ y
14 13 ralrimdva ⊢ z ∈ ℂ → x = z ⋅ ℎ A → ∀ y ∈ S ℋ A ⊆ y → x ∈ y
15 14 rexlimiv ⊢ ∃ z ∈ ℂ x = z ⋅ ℎ A → ∀ y ∈ S ℋ A ⊆ y → x ∈ y
16 1 h1de2ci ⊢ x ∈ ⊥ ⁡ ⊥ ⁡ A ↔ ∃ z ∈ ℂ x = z ⋅ ℎ A
17 vex ⊢ x ∈ V
18 17 elspani ⊢ A ⊆ ℋ → x ∈ span ⁡ A ↔ ∀ y ∈ S ℋ A ⊆ y → x ∈ y
19 1 2 18 mp2b ⊢ x ∈ span ⁡ A ↔ ∀ y ∈ S ℋ A ⊆ y → x ∈ y
20 15 16 19 3imtr4i ⊢ x ∈ ⊥ ⁡ ⊥ ⁡ A → x ∈ span ⁡ A
21 20 ssriv ⊢ ⊥ ⁡ ⊥ ⁡ A ⊆ span ⁡ A
22 4 21 eqssi ⊢ span ⁡ A = ⊥ ⁡ ⊥ ⁡ A