minvecolem4c

Description: Lemma for minveco . The infimum of the distances to A is a real number. (Contributed by Mario Carneiro, 16-Jun-2014) (Revised by AV, 4-Oct-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	minveco.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	minveco.m	⊢ 𝑀 = ( −_𝑣 ‘ 𝑈 )
	minveco.n	⊢ 𝑁 = ( norm_CV ‘ 𝑈 )
	minveco.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	minveco.u	⊢ ( 𝜑 → 𝑈 ∈ CPreHil_OLD )
	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	minvecolem4c	⊢ ( 𝜑 → 𝑆 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		minveco.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		minveco.m	⊢ 𝑀 = ( −_𝑣 ‘ 𝑈 )
3		minveco.n	⊢ 𝑁 = ( norm_CV ‘ 𝑈 )
4		minveco.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
5		minveco.u	⊢ ( 𝜑 → 𝑈 ∈ CPreHil_OLD )
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	1 2 3 4 5 6 7 8 9 10	minvecolem1	⊢ ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
15	14	simp1d	⊢ ( 𝜑 → 𝑅 ⊆ ℝ )
16	14	simp2d	⊢ ( 𝜑 → 𝑅 ≠ ∅ )
17		0re	⊢ 0 ∈ ℝ
18	14	simp3d	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 )
19		breq1	⊢ ( 𝑥 = 0 → ( 𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤 ) )
20	19	ralbidv	⊢ ( 𝑥 = 0 → ( ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
21	20	rspcev	⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
22	17 18 21	sylancr	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
23		infrecl	⊢ ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
24	15 16 22 23	syl3anc	⊢ ( 𝜑 → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
25	11 24	eqeltrid	⊢ ( 𝜑 → 𝑆 ∈ ℝ )

Metamath Proof Explorer

Theorem minvecolem4c

Proof