Metamath Proof Explorer

Theorem minveclem4b

Description: Lemma for minvec . The convergent point of the Cauchy sequence F is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014) (Revised by Mario Carneiro, 15-Oct-2015)

		Ref	Expression
	Hypotheses	minvec.x	$⊢ X = {Base}_{U}$
		minvec.m	$⊢ \underset{˙}{-} = -_{U}$
		minvec.n	$⊢ N = norm (U)$
		minvec.u	$⊢ φ \to U \in CPreHil$
		minvec.y	$⊢ φ \to Y \in LSubSp (U)$
		minvec.w	$⊢ φ \to U ↾_{𝑠} Y \in CMetSp$
		minvec.a	$⊢ φ \to A \in X$
		minvec.j	$⊢ J = TopOpen (U)$
		minvec.r	$⊢ R = ran (y \in Y ⟼ N (A \underset{˙}{-} y))$
		minvec.s	$⊢ S = sup (R ℝ <)$
		minvec.d	$⊢ D = {dist (U) ↾}_{(X \times X)}$
		minvec.f	$⊢ F = ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\})$
		minvec.p	$⊢ P = ⋃ (J fLim (X filGen F))$
	Assertion	minveclem4b	$⊢ φ \to P \in X$

Proof

Step	Hyp	Ref	Expression
1		minvec.x	$⊢ X = {Base}_{U}$
2		minvec.m	$⊢ \underset{˙}{-} = -_{U}$
3		minvec.n	$⊢ N = norm (U)$
4		minvec.u	$⊢ φ \to U \in CPreHil$
5		minvec.y	$⊢ φ \to Y \in LSubSp (U)$
6		minvec.w	$⊢ φ \to U ↾_{𝑠} Y \in CMetSp$
7		minvec.a	$⊢ φ \to A \in X$
8		minvec.j	$⊢ J = TopOpen (U)$
9		minvec.r	$⊢ R = ran (y \in Y ⟼ N (A \underset{˙}{-} y))$
10		minvec.s	$⊢ S = sup (R ℝ <)$
11		minvec.d	$⊢ D = {dist (U) ↾}_{(X \times X)}$
12		minvec.f	$⊢ F = ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\})$
13		minvec.p	$⊢ P = ⋃ (J fLim (X filGen F))$
14		eqid	$⊢ LSubSp (U) = LSubSp (U)$
15	1 14	lssss	$⊢ Y \in LSubSp (U) \to Y \subseteq X$
16	5 15	syl	$⊢ φ \to Y \subseteq X$
17	1 2 3 4 5 6 7 8 9 10 11 12 13	minveclem4a	$⊢ φ \to P \in ((J fLim (X filGen F)) \cap Y)$
18	17	elin2d	$⊢ φ \to P \in Y$
19	16 18	sseldd	$⊢ φ \to P \in X$