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 ⊒ ( πœ‘ β†’ ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ∈ 𝑋 )