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 \subseteq ℋ \to span (A) \subseteq ⊥ (⊥ (A))$

Proof

Step	Hyp	Ref	Expression
1		ocss	$⊢ A \subseteq ℋ \to ⊥ (A) \subseteq ℋ$
2		ocss	$⊢ ⊥ (A) \subseteq ℋ \to ⊥ (⊥ (A)) \subseteq ℋ$
3	1 2	syl	$⊢ A \subseteq ℋ \to ⊥ (⊥ (A)) \subseteq ℋ$
4		ococss	$⊢ A \subseteq ℋ \to A \subseteq ⊥ (⊥ (A))$
5		spanss	$⊢ (⊥ (⊥ (A)) \subseteq ℋ \land A \subseteq ⊥ (⊥ (A))) \to span (A) \subseteq span (⊥ (⊥ (A)))$
6	3 4 5	syl2anc	$⊢ A \subseteq ℋ \to span (A) \subseteq span (⊥ (⊥ (A)))$
7		ocsh	$⊢ ⊥ (A) \subseteq ℋ \to ⊥ (⊥ (A)) \in S_{ℋ}$
8		spanid	$⊢ ⊥ (⊥ (A)) \in S_{ℋ} \to span (⊥ (⊥ (A))) = ⊥ (⊥ (A))$
9	1 7 8	3syl	$⊢ A \subseteq ℋ \to span (⊥ (⊥ (A))) = ⊥ (⊥ (A))$
10	6 9	sseqtrd	$⊢ A \subseteq ℋ \to span (A) \subseteq ⊥ (⊥ (A))$