Theorem 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	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	minveco.m	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
	minveco.n	⊢ 𝑁 = ( normCV ‘ 𝑈 )
	minveco.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	minveco.u	⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
	minveco.w	⊢ ( 𝜑 → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
	minveco.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
	minveco.d	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
	minveco.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	minveco.r	⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
	minveco.s	⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
	minveco.f	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑌 )
	minveco.1	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
Assertion	minvecolem4a	⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		minveco.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		minveco.m	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3		minveco.n	⊢ 𝑁 = ( normCV ‘ 𝑈 )
4		minveco.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
5		minveco.u	⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
6		minveco.w	⊢ ( 𝜑 → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
7		minveco.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8		minveco.d	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
9		minveco.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
10		minveco.r	⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
11		minveco.s	⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
12		minveco.f	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑌 )
13		minveco.1	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
14		phnv	⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )
15	5 14	syl	⊢ ( 𝜑 → 𝑈 ∈ NrmCVec )
16		elin	⊢ ( 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) ↔ ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝑊 ∈ CBan ) )
17	6 16	sylib	⊢ ( 𝜑 → ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝑊 ∈ CBan ) )
18	17	simpld	⊢ ( 𝜑 → 𝑊 ∈ ( SubSp ‘ 𝑈 ) )
19		eqid	⊢ ( IndMet ‘ 𝑊 ) = ( IndMet ‘ 𝑊 )
20		eqid	⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
21	4 8 19 20	sspims	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → ( IndMet ‘ 𝑊 ) = ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) )
22	15 18 21	syl2anc	⊢ ( 𝜑 → ( IndMet ‘ 𝑊 ) = ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) )
23	17	simprd	⊢ ( 𝜑 → 𝑊 ∈ CBan )
24		eqid	⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
25	24 19	cbncms	⊢ ( 𝑊 ∈ CBan → ( IndMet ‘ 𝑊 ) ∈ ( CMet ‘ ( BaseSet ‘ 𝑊 ) ) )
26	23 25	syl	⊢ ( 𝜑 → ( IndMet ‘ 𝑊 ) ∈ ( CMet ‘ ( BaseSet ‘ 𝑊 ) ) )
27	22 26	eqeltrrd	⊢ ( 𝜑 → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ ( BaseSet ‘ 𝑊 ) ) )
28	1 2 3 4 5 6 7 8 9 10 11 12 13	minvecolem3	⊢ ( 𝜑 → 𝐹 ∈ ( Cau ‘ 𝐷 ) )
29	1 8	imsmet	⊢ ( 𝑈 ∈ NrmCVec → 𝐷 ∈ ( Met ‘ 𝑋 ) )
30	5 14 29	3syl	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
31		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
32	30 31	syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
33		causs	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )
34	32 12 33	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )
35	28 34	mpbid	⊢ ( 𝜑 → 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) )
36		eqid	⊢ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) )
37	36	cmetcau	⊢ ( ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ ( BaseSet ‘ 𝑊 ) ) ∧ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝐹 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )
38	27 35 37	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )
39		xmetres	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ ( 𝑋 ∩ 𝑌 ) ) )
40	36	methaus	⊢ ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ ( 𝑋 ∩ 𝑌 ) ) → ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ∈ Haus )
41	32 39 40	3syl	⊢ ( 𝜑 → ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ∈ Haus )
42		lmfun	⊢ ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ∈ Haus → Fun ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )
43		funfvbrb	⊢ ( Fun ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( 𝐹 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ↔ 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) )
44	41 42 43	3syl	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ↔ 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) )
45	38 44	mpbid	⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) )