Theorem minveclem5

Description: Lemma for minvec . Discharge the assumptions in minveclem4 . (Contributed by Mario Carneiro, 9-May-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 ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) )
Assertion	minveclem5	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )

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		oveq2	⊢ ( 𝑠 = 𝑟 → ( ( 𝑆 ↑ 2 ) + 𝑠 ) = ( ( 𝑆 ↑ 2 ) + 𝑟 ) )
13	12	breq2d	⊢ ( 𝑠 = 𝑟 → ( ( ( 𝐴 𝐷 𝑧 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑠 ) ↔ ( ( 𝐴 𝐷 𝑧 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) )
14	13	rabbidv	⊢ ( 𝑠 = 𝑟 → { 𝑧 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑧 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑠 ) } = { 𝑧 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑧 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } )
15		oveq2	⊢ ( 𝑧 = 𝑦 → ( 𝐴 𝐷 𝑧 ) = ( 𝐴 𝐷 𝑦 ) )
16	15	oveq1d	⊢ ( 𝑧 = 𝑦 → ( ( 𝐴 𝐷 𝑧 ) ↑ 2 ) = ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) )
17	16	breq1d	⊢ ( 𝑧 = 𝑦 → ( ( ( 𝐴 𝐷 𝑧 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ↔ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ) )
18	17	cbvrabv	⊢ { 𝑧 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑧 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } = { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) }
19	14 18	eqtrdi	⊢ ( 𝑠 = 𝑟 → { 𝑧 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑧 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑠 ) } = { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } )
20	19	cbvmptv	⊢ ( 𝑠 ∈ ℝ+ ↦ { 𝑧 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑧 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑠 ) } ) = ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } )
21	20	rneqi	⊢ ran ( 𝑠 ∈ ℝ+ ↦ { 𝑧 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑧 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑠 ) } ) = ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } )
22		eqid	⊢ ∪ ( 𝐽 fLim ( 𝑋 filGen ran ( 𝑠 ∈ ℝ+ ↦ { 𝑧 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑧 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑠 ) } ) ) ) = ∪ ( 𝐽 fLim ( 𝑋 filGen ran ( 𝑠 ∈ ℝ+ ↦ { 𝑧 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑧 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑠 ) } ) ) )
23		eqid	⊢ ( ( ( ( ( 𝐴 𝐷 ∪ ( 𝐽 fLim ( 𝑋 filGen ran ( 𝑠 ∈ ℝ+ ↦ { 𝑧 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑧 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑠 ) } ) ) ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) = ( ( ( ( ( 𝐴 𝐷 ∪ ( 𝐽 fLim ( 𝑋 filGen ran ( 𝑠 ∈ ℝ+ ↦ { 𝑧 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑧 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑠 ) } ) ) ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) )
24	1 2 3 4 5 6 7 8 9 10 11 21 22 23	minveclem4	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )