chlimi

Description: The limit property of a closed subspace of a Hilbert space. (Contributed by NM, 14-Sep-1999) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	chlim.1	$⊢ A \in V$
	Assertion	chlimi	$⊢ (H \in C_{ℋ} \land F : ℕ ⟶ H \land F \underset{v}{⇝} A) \to A \in H$

Proof

Step	Hyp	Ref	Expression
1		chlim.1	$⊢ A \in V$
2		isch2	$⊢ H \in C_{ℋ} \leftrightarrow (H \in S_{ℋ} \land \forall f \forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H))$
3	2	simprbi	$⊢ H \in C_{ℋ} \to \forall f \forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H)$
4		nnex	$⊢ ℕ \in V$
5		fex	$⊢ (F : ℕ ⟶ H \land ℕ \in V) \to F \in V$
6	4 5	mpan2	$⊢ F : ℕ ⟶ H \to F \in V$
7	6	adantr	$⊢ (F : ℕ ⟶ H \land F \underset{v}{⇝} A) \to F \in V$
8		feq1	$⊢ f = F \to (f : ℕ ⟶ H \leftrightarrow F : ℕ ⟶ H)$
9		breq1	$⊢ f = F \to (f \underset{v}{⇝} x \leftrightarrow F \underset{v}{⇝} x)$
10	8 9	anbi12d	$⊢ f = F \to ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \leftrightarrow (F : ℕ ⟶ H \land F \underset{v}{⇝} x))$
11	10	imbi1d	$⊢ f = F \to (((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \leftrightarrow ((F : ℕ ⟶ H \land F \underset{v}{⇝} x) \to x \in H))$
12	11	albidv	$⊢ f = F \to (\forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \leftrightarrow \forall x ((F : ℕ ⟶ H \land F \underset{v}{⇝} x) \to x \in H))$
13	12	spcgv	$⊢ F \in V \to (\forall f \forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \to \forall x ((F : ℕ ⟶ H \land F \underset{v}{⇝} x) \to x \in H))$
14		breq2	$⊢ x = A \to (F \underset{v}{⇝} x \leftrightarrow F \underset{v}{⇝} A)$
15	14	anbi2d	$⊢ x = A \to ((F : ℕ ⟶ H \land F \underset{v}{⇝} x) \leftrightarrow (F : ℕ ⟶ H \land F \underset{v}{⇝} A))$
16		eleq1	$⊢ x = A \to (x \in H \leftrightarrow A \in H)$
17	15 16	imbi12d	$⊢ x = A \to (((F : ℕ ⟶ H \land F \underset{v}{⇝} x) \to x \in H) \leftrightarrow ((F : ℕ ⟶ H \land F \underset{v}{⇝} A) \to A \in H))$
18	1 17	spcv	$⊢ \forall x ((F : ℕ ⟶ H \land F \underset{v}{⇝} x) \to x \in H) \to ((F : ℕ ⟶ H \land F \underset{v}{⇝} A) \to A \in H)$
19	13 18	syl6	$⊢ F \in V \to (\forall f \forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \to ((F : ℕ ⟶ H \land F \underset{v}{⇝} A) \to A \in H))$
20	7 19	syl	$⊢ (F : ℕ ⟶ H \land F \underset{v}{⇝} A) \to (\forall f \forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \to ((F : ℕ ⟶ H \land F \underset{v}{⇝} A) \to A \in H))$
21	20	pm2.43b	$⊢ \forall f \forall x ((f : ℕ ⟶ H \land f \underset{v}{⇝} x) \to x \in H) \to ((F : ℕ ⟶ H \land F \underset{v}{⇝} A) \to A \in H)$
22	3 21	syl	$⊢ H \in C_{ℋ} \to ((F : ℕ ⟶ H \land F \underset{v}{⇝} A) \to A \in H)$
23	22	3impib	$⊢ (H \in C_{ℋ} \land F : ℕ ⟶ H \land F \underset{v}{⇝} A) \to A \in H$

Metamath Proof Explorer

Theorem chlimi

Proof