isch3

Description: A Hilbert subspace is closed iff it is complete. A complete subspace is one in which every Cauchy sequence of vectors in the subspace converges to a member of the subspace (Definition of complete subspace in Beran p. 96). Remark 3.12 of Beran p. 107. (Contributed by NM, 24-Dec-2001) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

		Ref	Expression
	Assertion	isch3	$⊢ H \in C_{ℋ} \leftrightarrow (H \in S_{ℋ} \land \forall f \in Cauchy (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x))$

Proof

Step	Hyp	Ref	Expression
1		isch2	$⊢ H \in C_{ℋ} \leftrightarrow (H \in S_{ℋ} \land \forall f \forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H))$
2		ax-hcompl	$⊢ f \in Cauchy \to \exists x \in ℋ f \underset{v}{⇝} x$
3		rexex	$⊢ \exists x \in ℋ f \underset{v}{⇝} x \to \exists x f \underset{v}{⇝} x$
4	2 3	syl	$⊢ f \in Cauchy \to \exists x f \underset{v}{⇝} x$
5		19.29	$⊢ (\forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \land \exists x f \underset{v}{⇝} x) \to \exists x (((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \land f \underset{v}{⇝} x)$
6	4 5	sylan2	$⊢ (\forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \land f \in Cauchy) \to \exists x (((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \land f \underset{v}{⇝} x)$
7		id	$⊢ ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \to ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H)$
8	7	imp	$⊢ (((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \land (f : ℕ ⟶ H \land f \underset{v}{⇝} x)) \to x \in H$
9	8	an12s	$⊢ (f : ℕ ⟶ H \land (((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \land f \underset{v}{⇝} x)) \to x \in H$
10		simprr	$⊢ (f : ℕ ⟶ H \land (((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \land f \underset{v}{⇝} x)) \to f \underset{v}{⇝} x$
11	9 10	jca	$⊢ (f : ℕ ⟶ H \land (((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \land f \underset{v}{⇝} x)) \to (x \in H \land f \underset{v}{⇝} x)$
12	11	ex	$⊢ f : ℕ ⟶ H \to ((((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \land f \underset{v}{⇝} x) \to (x \in H \land f \underset{v}{⇝} x))$
13	12	eximdv	$⊢ f : ℕ ⟶ H \to (\exists x (((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \land f \underset{v}{⇝} x) \to \exists x (x \in H \land f \underset{v}{⇝} x))$
14	13	com12	$⊢ \exists x (((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \land f \underset{v}{⇝} x) \to (f : ℕ ⟶ H \to \exists x (x \in H \land f \underset{v}{⇝} x))$
15		df-rex	$⊢ \exists x \in H f \underset{v}{⇝} x \leftrightarrow \exists x (x \in H \land f \underset{v}{⇝} x)$
16	14 15	syl6ibr	$⊢ \exists x (((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \land f \underset{v}{⇝} x) \to (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x)$
17	6 16	syl	$⊢ (\forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \land f \in Cauchy) \to (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x)$
18	17	ex	$⊢ \forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \to (f \in Cauchy \to (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x))$
19		nfv	$⊢ Ⅎ x f \in Cauchy$
20		nfv	$⊢ Ⅎ x f : ℕ ⟶ H$
21		nfre1	$⊢ Ⅎ x \exists x \in H f \underset{v}{⇝} x$
22	20 21	nfim	$⊢ Ⅎ x (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x)$
23	19 22	nfim	$⊢ Ⅎ x (f \in Cauchy \to (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x))$
24		bi2.04	$⊢ (f \in Cauchy \to (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x)) \leftrightarrow (f : ℕ ⟶ H \to (f \in Cauchy \to \exists x \in H f \underset{v}{⇝} x))$
25		hlimcaui	$⊢ f \underset{v}{⇝} x \to f \in Cauchy$
26	25	imim1i	$⊢ (f \in Cauchy \to \exists x \in H f \underset{v}{⇝} x) \to (f \underset{v}{⇝} x \to \exists x \in H f \underset{v}{⇝} x)$
27		rexex	$⊢ \exists x \in H f \underset{v}{⇝} x \to \exists x f \underset{v}{⇝} x$
28		hlimeui	$⊢ \exists x f \underset{v}{⇝} x \leftrightarrow \exists! x f \underset{v}{⇝} x$
29	27 28	sylib	$⊢ \exists x \in H f \underset{v}{⇝} x \to \exists! x f \underset{v}{⇝} x$
30		exancom	$⊢ \exists x (x \in H \land f \underset{v}{⇝} x) \leftrightarrow \exists x (f \underset{v}{⇝} x \land x \in H)$
31	15 30	sylbb	$⊢ \exists x \in H f \underset{v}{⇝} x \to \exists x (f \underset{v}{⇝} x \land x \in H)$
32		eupick	$⊢ (\exists! x f \underset{v}{⇝} x \land \exists x (f \underset{v}{⇝} x \land x \in H)) \to (f \underset{v}{⇝} x \to x \in H)$
33	29 31 32	syl2anc	$⊢ \exists x \in H f \underset{v}{⇝} x \to (f \underset{v}{⇝} x \to x \in H)$
34	26 33	syli	$⊢ (f \in Cauchy \to \exists x \in H f \underset{v}{⇝} x) \to (f \underset{v}{⇝} x \to x \in H)$
35	34	imim2i	$⊢ (f : ℕ ⟶ H \to (f \in Cauchy \to \exists x \in H f \underset{v}{⇝} x)) \to (f : ℕ ⟶ H \to (f \underset{v}{⇝} x \to x \in H))$
36	24 35	sylbi	$⊢ (f \in Cauchy \to (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x)) \to (f : ℕ ⟶ H \to (f \underset{v}{⇝} x \to x \in H))$
37	36	impd	$⊢ (f \in Cauchy \to (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x)) \to ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H)$
38	23 37	alrimi	$⊢ (f \in Cauchy \to (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x)) \to \forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H)$
39	18 38	impbii	$⊢ \forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \leftrightarrow (f \in Cauchy \to (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x))$
40	39	albii	$⊢ \forall f \forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \leftrightarrow \forall f (f \in Cauchy \to (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x))$
41		df-ral	$⊢ \forall f \in Cauchy (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x) \leftrightarrow \forall f (f \in Cauchy \to (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x))$
42	40 41	bitr4i	$⊢ \forall f \forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \leftrightarrow \forall f \in Cauchy (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x)$
43	42	anbi2i	$⊢ (H \in S_{ℋ} \land \forall f \forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H)) \leftrightarrow (H \in S_{ℋ} \land \forall f \in Cauchy (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x))$
44	1 43	bitri	$⊢ H \in C_{ℋ} \leftrightarrow (H \in S_{ℋ} \land \forall f \in Cauchy (f : ℕ ⟶ H \to \exists x \in H f \underset{v}{⇝} x))$

Metamath Proof Explorer

Theorem isch3

Proof