This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) )