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 ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )

Proof

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