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

Metamath Proof Explorer

Theorem 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 ⊢ 𝑋 = ( 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 minvecolem4b ( 𝜑 → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝑋 )

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 ⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
20 1 4 19 sspba ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → 𝑌 ⊆ 𝑋 )
21 15 18 20 syl2anc ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
22 1 8 imsxmet ⊢ ( 𝑈 ∈ NrmCVec → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
23 15 22 syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
24 9 methaus ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Haus )
25 23 24 syl ⊢ ( 𝜑 → 𝐽 ∈ Haus )
26 lmfun ⊢ ( 𝐽 ∈ Haus → Fun ( ⇝𝑡 ‘ 𝐽 ) )
27 25 26 syl ⊢ ( 𝜑 → Fun ( ⇝𝑡 ‘ 𝐽 ) )
28 1 2 3 4 5 6 7 8 9 10 11 12 13 minvecolem4a ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) )
29 eqid ⊢ ( 𝐽 ↾t 𝑌 ) = ( 𝐽 ↾t 𝑌 )
30 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
31 4 fvexi ⊢ 𝑌 ∈ V
32 31 a1i ⊢ ( 𝜑 → 𝑌 ∈ V )
33 9 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
34 23 33 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
35 xmetres2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) )
36 23 21 35 syl2anc ⊢ ( 𝜑 → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) )
37 eqid ⊢ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) )
38 37 mopntopon ⊢ ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) → ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ∈ ( TopOn ‘ 𝑌 ) )
39 36 38 syl ⊢ ( 𝜑 → ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ∈ ( TopOn ‘ 𝑌 ) )
40 lmcl ⊢ ( ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) → ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ∈ 𝑌 )
41 39 28 40 syl2anc ⊢ ( 𝜑 → ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ∈ 𝑌 )
42 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
43 29 30 32 34 41 42 12 lmss ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ↔ 𝐹 ( ⇝𝑡 ‘ ( 𝐽 ↾t 𝑌 ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) )
44 eqid ⊢ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) = ( 𝐷 ↾ ( 𝑌 × 𝑌 ) )
45 44 9 37 metrest ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑌 ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) )
46 23 21 45 syl2anc ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑌 ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) )
47 46 fveq2d ⊢ ( 𝜑 → ( ⇝𝑡 ‘ ( 𝐽 ↾t 𝑌 ) ) = ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )
48 47 breqd ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( 𝐽 ↾t 𝑌 ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ↔ 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) )
49 43 48 bitrd ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ↔ 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) )
50 28 49 mpbird ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) )
51 funbrfv ⊢ ( Fun ( ⇝𝑡 ‘ 𝐽 ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) )
52 27 50 51 sylc ⊢ ( 𝜑 → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) )
53 52 41 eqeltrd ⊢ ( 𝜑 → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝑌 )
54 21 53 sseldd ⊢ ( 𝜑 → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝑋 )