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

Metamath Proof Explorer

Theorem spanssoc

Description: The span of a subset of Hilbert space is less than or equal to its closure (double orthogonal complement). (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spanssoc ⊢ A ⊆ ℋ → span ⁡ A ⊆ ⊥ ⁡ ⊥ ⁡ A

Proof

Step Hyp Ref Expression
1 ocss ⊢ A ⊆ ℋ → ⊥ ⁡ A ⊆ ℋ
2 ocss ⊢ ⊥ ⁡ A ⊆ ℋ → ⊥ ⁡ ⊥ ⁡ A ⊆ ℋ
3 1 2 syl ⊢ A ⊆ ℋ → ⊥ ⁡ ⊥ ⁡ A ⊆ ℋ
4 ococss ⊢ A ⊆ ℋ → A ⊆ ⊥ ⁡ ⊥ ⁡ A
5 spanss ⊢ ⊥ ⁡ ⊥ ⁡ A ⊆ ℋ ∧ A ⊆ ⊥ ⁡ ⊥ ⁡ A → span ⁡ A ⊆ span ⁡ ⊥ ⁡ ⊥ ⁡ A
6 3 4 5 syl2anc ⊢ A ⊆ ℋ → span ⁡ A ⊆ span ⁡ ⊥ ⁡ ⊥ ⁡ A
7 ocsh ⊢ ⊥ ⁡ A ⊆ ℋ → ⊥ ⁡ ⊥ ⁡ A ∈ S ℋ
8 spanid ⊢ ⊥ ⁡ ⊥ ⁡ A ∈ S ℋ → span ⁡ ⊥ ⁡ ⊥ ⁡ A = ⊥ ⁡ ⊥ ⁡ A
9 1 7 8 3syl ⊢ A ⊆ ℋ → span ⁡ ⊥ ⁡ ⊥ ⁡ A = ⊥ ⁡ ⊥ ⁡ A
10 6 9 sseqtrd ⊢ A ⊆ ℋ → span ⁡ A ⊆ ⊥ ⁡ ⊥ ⁡ A