Metamath Proof Explorer

Theorem minveclem6

Description: Lemma for minvec . Any minimal point is less than S away from A . (Contributed by Mario Carneiro, 9-May-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 ( 𝑅 , ℝ , < )
minvec.d ⊢ 𝐷 = ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) )
Assertion minveclem6 ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )

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 11 oveqi ⊢ ( 𝐴 𝐷 𝑥 ) = ( 𝐴 ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) 𝑥 )
13 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝐴 ∈ 𝑋 )
14 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
15 1 14 lssss ⊢ ( 𝑌 ∈ ( LSubSp ‘ 𝑈 ) → 𝑌 ⊆ 𝑋 )
16 5 15 syl ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
17 16 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑋 )
18 13 17 ovresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐴 ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) 𝑥 ) = ( 𝐴 ( dist ‘ 𝑈 ) 𝑥 ) )
19 12 18 syl5eq ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐴 𝐷 𝑥 ) = ( 𝐴 ( dist ‘ 𝑈 ) 𝑥 ) )
20 cphngp ⊢ ( 𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp )
21 4 20 syl ⊢ ( 𝜑 → 𝑈 ∈ NrmGrp )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑈 ∈ NrmGrp )
23 eqid ⊢ ( dist ‘ 𝑈 ) = ( dist ‘ 𝑈 )
24 3 1 2 23 ngpds ⊢ ( ( 𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 ( dist ‘ 𝑈 ) 𝑥 ) = ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) )
25 22 13 17 24 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐴 ( dist ‘ 𝑈 ) 𝑥 ) = ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) )
26 19 25 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐴 𝐷 𝑥 ) = ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) )
27 26 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ↑ 2 ) )
28 1 2 3 4 5 6 7 8 9 minveclem1 ⊢ ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
30 29 simp1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑅 ⊆ ℝ )
31 29 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑅 ≠ ∅ )
32 0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 0 ∈ ℝ )
33 29 simp3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 )
34 breq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤 ) )
35 34 ralbidv ⊢ ( 𝑥 = 0 → ( ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
36 35 rspcev ⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
37 32 33 36 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
38 infrecl ⊢ ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
39 30 31 37 38 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
40 10 39 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑆 ∈ ℝ )
41 40 resqcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑆 ↑ 2 ) ∈ ℝ )
42 41 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑆 ↑ 2 ) ∈ ℂ )
43 42 addid1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑆 ↑ 2 ) + 0 ) = ( 𝑆 ↑ 2 ) )
44 27 43 breq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ( ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ↑ 2 ) ≤ ( 𝑆 ↑ 2 ) ) )
45 cphlmod ⊢ ( 𝑈 ∈ ℂPreHil → 𝑈 ∈ LMod )
46 4 45 syl ⊢ ( 𝜑 → 𝑈 ∈ LMod )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑈 ∈ LMod )
48 1 2 lmodvsubcl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 − 𝑥 ) ∈ 𝑋 )
49 47 13 17 48 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐴 − 𝑥 ) ∈ 𝑋 )
50 1 3 nmcl ⊢ ( ( 𝑈 ∈ NrmGrp ∧ ( 𝐴 − 𝑥 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ∈ ℝ )
51 22 49 50 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ∈ ℝ )
52 1 3 nmge0 ⊢ ( ( 𝑈 ∈ NrmGrp ∧ ( 𝐴 − 𝑥 ) ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) )
53 22 49 52 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 0 ≤ ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) )
54 infregelb ⊢ ( ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) ∧ 0 ∈ ℝ ) → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
55 30 31 37 32 54 syl31anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
56 33 55 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 0 ≤ inf ( 𝑅 , ℝ , < ) )
57 56 10 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 0 ≤ 𝑆 )
58 51 40 53 57 le2sqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ 𝑆 ↔ ( ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ↑ 2 ) ≤ ( 𝑆 ↑ 2 ) ) )
59 10 breq2i ⊢ ( ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ 𝑆 ↔ ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ inf ( 𝑅 , ℝ , < ) )
60 infregelb ⊢ ( ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) ∧ ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ∈ ℝ ) → ( ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ 𝑤 ) )
61 30 31 37 51 60 syl31anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ 𝑤 ) )
62 59 61 syl5bb ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ 𝑆 ↔ ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ 𝑤 ) )
63 44 58 62 3bitr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ 𝑤 ) )
64 9 raleqi ⊢ ( ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ 𝑤 ↔ ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ 𝑤 )
65 fvex ⊢ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ V
66 65 rgenw ⊢ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ V
67 eqid ⊢ ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
68 breq2 ⊢ ( 𝑤 = ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) → ( ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ 𝑤 ↔ ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )
69 67 68 ralrnmptw ⊢ ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ V → ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )
70 66 69 ax-mp ⊢ ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
71 64 70 bitri ⊢ ( ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
72 63 71 bitrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )