Theorem minveclem4c

Description: Lemma for minvec . The infimum of the distances to A is a real number. (Contributed by Mario Carneiro, 16-Jun-2014) (Revised by Mario Carneiro, 15-Oct-2015) (Revised by AV, 3-Oct-2020)

	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 ( 𝑅 , ℝ , < )
Assertion	minveclem4c	⊢ ( 𝜑 → 𝑆 ∈ ℝ )

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	1 2 3 4 5 6 7 8 9	minveclem1	⊢ ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
12	11	simp1d	⊢ ( 𝜑 → 𝑅 ⊆ ℝ )
13	11	simp2d	⊢ ( 𝜑 → 𝑅 ≠ ∅ )
14		0re	⊢ 0 ∈ ℝ
15	11	simp3d	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 )
16		breq1	⊢ ( 𝑦 = 0 → ( 𝑦 ≤ 𝑤 ↔ 0 ≤ 𝑤 ) )
17	16	ralbidv	⊢ ( 𝑦 = 0 → ( ∀ 𝑤 ∈ 𝑅 𝑦 ≤ 𝑤 ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
18	17	rspcev	⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑦 ≤ 𝑤 )
19	14 15 18	sylancr	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑦 ≤ 𝑤 )
20		infrecl	⊢ ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑦 ≤ 𝑤 ) → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
21	12 13 19 20	syl3anc	⊢ ( 𝜑 → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
22	10 21	eqeltrid	⊢ ( 𝜑 → 𝑆 ∈ ℝ )