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