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	⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )