minvecolem4a

Description: Lemma for minveco . F is convergent in the subspace topology on Y . (Contributed by Mario Carneiro, 7-May-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	minvecolem4a	$⊢ φ \to F \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F)$

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	$⊢ IndMet (W) = IndMet (W)$
20		eqid	$⊢ SubSp (U) = SubSp (U)$
21	4 8 19 20	sspims	$⊢ (U \in NrmCVec \land W \in SubSp (U)) \to IndMet (W) = {D ↾}_{(Y \times Y)}$
22	15 18 21	syl2anc	$⊢ φ \to IndMet (W) = {D ↾}_{(Y \times Y)}$
23	17	simprd	$⊢ φ \to W \in CBan$
24		eqid	$⊢ BaseSet (W) = BaseSet (W)$
25	24 19	cbncms	$⊢ W \in CBan \to IndMet (W) \in CMet (BaseSet (W))$
26	23 25	syl	$⊢ φ \to IndMet (W) \in CMet (BaseSet (W))$
27	22 26	eqeltrrd	$⊢ φ \to {D ↾}_{(Y \times Y)} \in CMet (BaseSet (W))$
28	1 2 3 4 5 6 7 8 9 10 11 12 13	minvecolem3	$⊢ φ \to F \in Cau (D)$
29	1 8	imsmet	$⊢ U \in NrmCVec \to D \in Met (X)$
30	5 14 29	3syl	$⊢ φ \to D \in Met (X)$
31		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
32	30 31	syl	$⊢ φ \to D \in ∞Met (X)$
33		causs	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ Y) \to (F \in Cau (D) \leftrightarrow F \in Cau ({D ↾}_{(Y \times Y)}))$
34	32 12 33	syl2anc	$⊢ φ \to (F \in Cau (D) \leftrightarrow F \in Cau ({D ↾}_{(Y \times Y)}))$
35	28 34	mpbid	$⊢ φ \to F \in Cau ({D ↾}_{(Y \times Y)})$
36		eqid	$⊢ MetOpen ({D ↾}_{(Y \times Y)}) = MetOpen ({D ↾}_{(Y \times Y)})$
37	36	cmetcau	$⊢ ({D ↾}_{(Y \times Y)} \in CMet (BaseSet (W)) \land F \in Cau ({D ↾}_{(Y \times Y)})) \to F \in dom \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)}))$
38	27 35 37	syl2anc	$⊢ φ \to F \in dom \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)}))$
39		xmetres	$⊢ D \in ∞Met (X) \to {D ↾}_{(Y \times Y)} \in ∞Met (X \cap Y)$
40	36	methaus	$⊢ {D ↾}_{(Y \times Y)} \in ∞Met (X \cap Y) \to MetOpen ({D ↾}_{(Y \times Y)}) \in Haus$
41	32 39 40	3syl	$⊢ φ \to MetOpen ({D ↾}_{(Y \times Y)}) \in Haus$
42		lmfun	$⊢ MetOpen ({D ↾}_{(Y \times Y)}) \in Haus \to Fun \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)}))$
43		funfvbrb	$⊢ Fun \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) \to (F \in dom \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) \leftrightarrow F \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F))$
44	41 42 43	3syl	$⊢ φ \to (F \in dom \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) \leftrightarrow F \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F))$
45	38 44	mpbid	$⊢ φ \to F \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F)$

Metamath Proof Explorer

Theorem minvecolem4a

Proof