minvecolem4b

Description: Lemma for minveco . The convergent point of the Cauchy sequence F is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	minveco.x	$⊢ X = BaseSet (U)$
	minveco.m	$⊢ M = -_{v} (U)$
	minveco.n	$⊢ N = {norm}_{CV} (U)$
	minveco.y	$⊢ Y = BaseSet (W)$
	minveco.u	$⊢ φ \to U \in {CPreHil}_{OLD}$
	minveco.w	$⊢ φ \to W \in (SubSp (U) \cap CBan)$
	minveco.a	$⊢ φ \to A \in X$
	minveco.d	$⊢ D = IndMet (U)$
	minveco.j	$⊢ J = MetOpen (D)$
	minveco.r	$⊢ R = ran (y \in Y ⟼ N (A M y))$
	minveco.s	$⊢ S = inf (R ℝ <)$
	minveco.f	$⊢ φ \to F : ℕ ⟶ Y$
	minveco.1	$⊢ (φ \land n \in ℕ) \to {(A D F (n))}^{2} \leq S^{2} + (\frac{1}{n})$
Assertion	minvecolem4b	$⊢ φ \to \underset{t}{⇝} (J) (F) \in X$

Proof

Step	Hyp	Ref	Expression
1		minveco.x	$⊢ X = BaseSet (U)$
2		minveco.m	$⊢ M = -_{v} (U)$
3		minveco.n	$⊢ N = {norm}_{CV} (U)$
4		minveco.y	$⊢ Y = BaseSet (W)$
5		minveco.u	$⊢ φ \to U \in {CPreHil}_{OLD}$
6		minveco.w	$⊢ φ \to W \in (SubSp (U) \cap CBan)$
7		minveco.a	$⊢ φ \to A \in X$
8		minveco.d	$⊢ D = IndMet (U)$
9		minveco.j	$⊢ J = MetOpen (D)$
10		minveco.r	$⊢ R = ran (y \in Y ⟼ N (A M y))$
11		minveco.s	$⊢ S = inf (R ℝ <)$
12		minveco.f	$⊢ φ \to F : ℕ ⟶ Y$
13		minveco.1	$⊢ (φ \land n \in ℕ) \to {(A D F (n))}^{2} \leq S^{2} + (\frac{1}{n})$
14		phnv	$⊢ U \in {CPreHil}_{OLD} \to U \in NrmCVec$
15	5 14	syl	$⊢ φ \to U \in NrmCVec$
16		elin	$⊢ W \in (SubSp (U) \cap CBan) \leftrightarrow (W \in SubSp (U) \land W \in CBan)$
17	6 16	sylib	$⊢ φ \to (W \in SubSp (U) \land W \in CBan)$
18	17	simpld	$⊢ φ \to W \in SubSp (U)$
19		eqid	$⊢ SubSp (U) = SubSp (U)$
20	1 4 19	sspba	$⊢ (U \in NrmCVec \land W \in SubSp (U)) \to Y \subseteq X$
21	15 18 20	syl2anc	$⊢ φ \to Y \subseteq X$
22	1 8	imsxmet	$⊢ U \in NrmCVec \to D \in ∞Met (X)$
23	15 22	syl	$⊢ φ \to D \in ∞Met (X)$
24	9	methaus	$⊢ D \in ∞Met (X) \to J \in Haus$
25	23 24	syl	$⊢ φ \to J \in Haus$
26		lmfun	$⊢ J \in Haus \to Fun \underset{t}{⇝} (J)$
27	25 26	syl	$⊢ φ \to Fun \underset{t}{⇝} (J)$
28	1 2 3 4 5 6 7 8 9 10 11 12 13	minvecolem4a	$⊢ φ \to F \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F)$
29		eqid	$⊢ J ↾_{𝑡} Y = J ↾_{𝑡} Y$
30		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
31	4	fvexi	$⊢ Y \in V$
32	31	a1i	$⊢ φ \to Y \in V$
33	9	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
34	23 33	syl	$⊢ φ \to J \in Top$
35		xmetres2	$⊢ (D \in ∞Met (X) \land Y \subseteq X) \to {D ↾}_{(Y \times Y)} \in ∞Met (Y)$
36	23 21 35	syl2anc	$⊢ φ \to {D ↾}_{(Y \times Y)} \in ∞Met (Y)$
37		eqid	$⊢ MetOpen ({D ↾}_{(Y \times Y)}) = MetOpen ({D ↾}_{(Y \times Y)})$
38	37	mopntopon	$⊢ {D ↾}_{(Y \times Y)} \in ∞Met (Y) \to MetOpen ({D ↾}_{(Y \times Y)}) \in TopOn (Y)$
39	36 38	syl	$⊢ φ \to MetOpen ({D ↾}_{(Y \times Y)}) \in TopOn (Y)$
40		lmcl	$⊢ (MetOpen ({D ↾}_{(Y \times Y)}) \in TopOn (Y) \land F \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F)) \to \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F) \in Y$
41	39 28 40	syl2anc	$⊢ φ \to \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F) \in Y$
42		1zzd	$⊢ φ \to 1 \in ℤ$
43	29 30 32 34 41 42 12	lmss	$⊢ φ \to (F \underset{t}{⇝} (J) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F) \leftrightarrow F \underset{t}{⇝} (J ↾_{𝑡} Y) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F))$
44		eqid	$⊢ {D ↾}_{(Y \times Y)} = {D ↾}_{(Y \times Y)}$
45	44 9 37	metrest	$⊢ (D \in ∞Met (X) \land Y \subseteq X) \to J ↾_{𝑡} Y = MetOpen ({D ↾}_{(Y \times Y)})$
46	23 21 45	syl2anc	$⊢ φ \to J ↾_{𝑡} Y = MetOpen ({D ↾}_{(Y \times Y)})$
47	46	fveq2d	$⊢ φ \to \underset{t}{⇝} (J ↾_{𝑡} Y) = \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)}))$
48	47	breqd	$⊢ φ \to (F \underset{t}{⇝} (J ↾_{𝑡} Y) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F) \leftrightarrow F \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F))$
49	43 48	bitrd	$⊢ φ \to (F \underset{t}{⇝} (J) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F) \leftrightarrow F \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F))$
50	28 49	mpbird	$⊢ φ \to F \underset{t}{⇝} (J) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F)$
51		funbrfv	$⊢ Fun \underset{t}{⇝} (J) \to (F \underset{t}{⇝} (J) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F) \to \underset{t}{⇝} (J) (F) = \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F))$
52	27 50 51	sylc	$⊢ φ \to \underset{t}{⇝} (J) (F) = \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F)$
53	52 41	eqeltrd	$⊢ φ \to \underset{t}{⇝} (J) (F) \in Y$
54	21 53	sseldd	$⊢ φ \to \underset{t}{⇝} (J) (F) \in X$

Metamath Proof Explorer

Theorem minvecolem4b

Proof