Metamath Proof Explorer

Theorem minveclem4b

Description: Lemma for minvec . The convergent point of the Cauchy sequence F is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014) (Revised by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses minvec.x ⊒ 𝑋 = ( Base β€˜ π‘ˆ )
minvec.m ⊒ βˆ’ = ( -g β€˜ π‘ˆ )
minvec.n ⊒ 𝑁 = ( norm β€˜ π‘ˆ )
minvec.u ⊒ ( πœ‘ β†’ π‘ˆ ∈ β„‚PreHil )
minvec.y ⊒ ( πœ‘ β†’ π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) )
minvec.w ⊒ ( πœ‘ β†’ ( π‘ˆ β†Ύs π‘Œ ) ∈ CMetSp )
minvec.a ⊒ ( πœ‘ β†’ 𝐴 ∈ 𝑋 )
minvec.j ⊒ 𝐽 = ( TopOpen β€˜ π‘ˆ )
minvec.r ⊒ 𝑅 = ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
minvec.s ⊒ 𝑆 = inf ( 𝑅 , ℝ , < )
minvec.d ⊒ 𝐷 = ( ( dist β€˜ π‘ˆ ) β†Ύ ( 𝑋 Γ— 𝑋 ) )
minvec.f ⊒ 𝐹 = ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } )
minvec.p ⊒ 𝑃 = βˆͺ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) )
Assertion minveclem4b ( πœ‘ β†’ 𝑃 ∈ 𝑋 )

Proof

Step Hyp Ref Expression
1 minvec.x ⊒ 𝑋 = ( Base β€˜ π‘ˆ )
2 minvec.m ⊒ βˆ’ = ( -g β€˜ π‘ˆ )
3 minvec.n ⊒ 𝑁 = ( norm β€˜ π‘ˆ )
4 minvec.u ⊒ ( πœ‘ β†’ π‘ˆ ∈ β„‚PreHil )
5 minvec.y ⊒ ( πœ‘ β†’ π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) )
6 minvec.w ⊒ ( πœ‘ β†’ ( π‘ˆ β†Ύs π‘Œ ) ∈ CMetSp )
7 minvec.a ⊒ ( πœ‘ β†’ 𝐴 ∈ 𝑋 )
8 minvec.j ⊒ 𝐽 = ( TopOpen β€˜ π‘ˆ )
9 minvec.r ⊒ 𝑅 = ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
10 minvec.s ⊒ 𝑆 = inf ( 𝑅 , ℝ , < )
11 minvec.d ⊒ 𝐷 = ( ( dist β€˜ π‘ˆ ) β†Ύ ( 𝑋 Γ— 𝑋 ) )
12 minvec.f ⊒ 𝐹 = ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } )
13 minvec.p ⊒ 𝑃 = βˆͺ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) )
14 eqid ⊒ ( LSubSp β€˜ π‘ˆ ) = ( LSubSp β€˜ π‘ˆ )
15 1 14 lssss ⊒ ( π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) β†’ π‘Œ βŠ† 𝑋 )
16 5 15 syl ⊒ ( πœ‘ β†’ π‘Œ βŠ† 𝑋 )
17 1 2 3 4 5 6 7 8 9 10 11 12 13 minveclem4a ⊒ ( πœ‘ β†’ 𝑃 ∈ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ π‘Œ ) )
18 17 elin2d ⊒ ( πœ‘ β†’ 𝑃 ∈ π‘Œ )
19 16 18 sseldd ⊒ ( πœ‘ β†’ 𝑃 ∈ 𝑋 )