This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem minvecolem6

Description: Lemma for minveco . Any minimal point is less than S away from A . (Contributed by Mario Carneiro, 9-May-2014) (Revised by AV, 4-Oct-2020) (New usage is discouraged.)

Ref Expression
Hypotheses minveco.x ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
minveco.m ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
minveco.n ⊢ 𝑁 = ( normCV ‘ 𝑈 )
minveco.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
minveco.u ⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
minveco.w ⊢ ( 𝜑 → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
minveco.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
minveco.d ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
minveco.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
minveco.r ⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
minveco.s ⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
Assertion minvecolem6 ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 minveco.x ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 minveco.m ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3 minveco.n ⊢ 𝑁 = ( normCV ‘ 𝑈 )
4 minveco.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
5 minveco.u ⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
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 phnv ⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )
13 5 12 syl ⊢ ( 𝜑 → 𝑈 ∈ NrmCVec )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑈 ∈ NrmCVec )
15 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝐴 ∈ 𝑋 )
16 inss1 ⊢ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) ⊆ ( SubSp ‘ 𝑈 )
17 16 6 sselid ⊢ ( 𝜑 → 𝑊 ∈ ( SubSp ‘ 𝑈 ) )
18 eqid ⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
19 1 4 18 sspba ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → 𝑌 ⊆ 𝑋 )
20 13 17 19 syl2anc ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
21 20 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑋 )
22 1 2 3 8 imsdval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 𝐷 𝑥 ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) )
23 14 15 21 22 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐴 𝐷 𝑥 ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) )
24 23 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ↑ 2 ) )
25 1 2 3 4 5 6 7 8 9 10 minvecolem1 ⊢ ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
27 26 simp1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑅 ⊆ ℝ )
28 26 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑅 ≠ ∅ )
29 0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 0 ∈ ℝ )
30 26 simp3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 )
31 breq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤 ) )
32 31 ralbidv ⊢ ( 𝑥 = 0 → ( ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
33 32 rspcev ⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
34 29 30 33 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
35 infrecl ⊢ ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
36 27 28 34 35 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
37 11 36 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑆 ∈ ℝ )
38 37 resqcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑆 ↑ 2 ) ∈ ℝ )
39 38 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑆 ↑ 2 ) ∈ ℂ )
40 39 addridd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑆 ↑ 2 ) + 0 ) = ( 𝑆 ↑ 2 ) )
41 24 40 breq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ↑ 2 ) ≤ ( 𝑆 ↑ 2 ) ) )
42 1 2 nvmcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 𝑀 𝑥 ) ∈ 𝑋 )
43 14 15 21 42 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐴 𝑀 𝑥 ) ∈ 𝑋 )
44 1 3 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝑀 𝑥 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ∈ ℝ )
45 14 43 44 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ∈ ℝ )
46 1 3 nvge0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝑀 𝑥 ) ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) )
47 14 43 46 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 0 ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) )
48 infregelb ⊢ ( ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) ∧ 0 ∈ ℝ ) → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
49 27 28 34 29 48 syl31anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
50 30 49 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 0 ≤ inf ( 𝑅 , ℝ , < ) )
51 50 11 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 0 ≤ 𝑆 )
52 45 37 47 51 le2sqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑆 ↔ ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ↑ 2 ) ≤ ( 𝑆 ↑ 2 ) ) )
53 11 breq2i ⊢ ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑆 ↔ ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ inf ( 𝑅 , ℝ , < ) )
54 infregelb ⊢ ( ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) ∧ ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ∈ ℝ ) → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ) )
55 27 28 34 45 54 syl31anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ) )
56 53 55 bitrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑆 ↔ ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ) )
57 41 52 56 3bitr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ) )
58 10 raleqi ⊢ ( ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ↔ ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 )
59 fvex ⊢ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ V
60 59 rgenw ⊢ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ V
61 eqid ⊢ ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
62 breq2 ⊢ ( 𝑤 = ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ↔ ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
63 61 62 ralrnmptw ⊢ ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ V → ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
64 60 63 ax-mp ⊢ ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
65 58 64 bitri ⊢ ( ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
66 57 65 bitrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )