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 \in ℋ$
	Assertion	spansni	$⊢ span (\{A\}) = ⊥ (⊥ (\{A\}))$

Proof

Step	Hyp	Ref	Expression
1		spansn.1	$⊢ A \in ℋ$
2		snssi	$⊢ A \in ℋ \to \{A\} \subseteq ℋ$
3		spanssoc	$⊢ \{A\} \subseteq ℋ \to span (\{A\}) \subseteq ⊥ (⊥ (\{A\}))$
4	1 2 3	mp2b	$⊢ span (\{A\}) \subseteq ⊥ (⊥ (\{A\}))$
5	1	elexi	$⊢ A \in V$
6	5	snss	$⊢ A \in y \leftrightarrow \{A\} \subseteq y$
7		shmulcl	$⊢ (y \in S_{ℋ} \land z \in ℂ \land A \in y) \to z \cdot_{ℎ} A \in y$
8	7	3expia	$⊢ (y \in S_{ℋ} \land z \in ℂ) \to (A \in y \to z \cdot_{ℎ} A \in y)$
9	8	ancoms	$⊢ (z \in ℂ \land y \in S_{ℋ}) \to (A \in y \to z \cdot_{ℎ} A \in y)$
10	6 9	syl5bir	$⊢ (z \in ℂ \land y \in S_{ℋ}) \to (\{A\} \subseteq y \to z \cdot_{ℎ} A \in y)$
11		eleq1	$⊢ x = z \cdot_{ℎ} A \to (x \in y \leftrightarrow z \cdot_{ℎ} A \in y)$
12	11	imbi2d	$⊢ x = z \cdot_{ℎ} A \to ((\{A\} \subseteq y \to x \in y) \leftrightarrow (\{A\} \subseteq y \to z \cdot_{ℎ} A \in y))$
13	10 12	syl5ibrcom	$⊢ (z \in ℂ \land y \in S_{ℋ}) \to (x = z \cdot_{ℎ} A \to (\{A\} \subseteq y \to x \in y))$
14	13	ralrimdva	$⊢ z \in ℂ \to (x = z \cdot_{ℎ} A \to \forall y \in S_{ℋ} (\{A\} \subseteq y \to x \in y))$
15	14	rexlimiv	$⊢ \exists z \in ℂ x = z \cdot_{ℎ} A \to \forall y \in S_{ℋ} (\{A\} \subseteq y \to x \in y)$
16	1	h1de2ci	$⊢ x \in ⊥ (⊥ (\{A\})) \leftrightarrow \exists z \in ℂ x = z \cdot_{ℎ} A$
17		vex	$⊢ x \in V$
18	17	elspani	$⊢ \{A\} \subseteq ℋ \to (x \in span (\{A\}) \leftrightarrow \forall y \in S_{ℋ} (\{A\} \subseteq y \to x \in y))$
19	1 2 18	mp2b	$⊢ x \in span (\{A\}) \leftrightarrow \forall y \in S_{ℋ} (\{A\} \subseteq y \to x \in y)$
20	15 16 19	3imtr4i	$⊢ x \in ⊥ (⊥ (\{A\})) \to x \in span (\{A\})$
21	20	ssriv	$⊢ ⊥ (⊥ (\{A\})) \subseteq span (\{A\})$
22	4 21	eqssi	$⊢ span (\{A\}) = ⊥ (⊥ (\{A\}))$

Metamath Proof Explorer

Theorem spansni

Proof