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 eqtrid ⊒ ( ( πœ‘ ∧ π‘₯ ∈ π‘Œ ) β†’ ( 𝐴 𝐷 π‘₯ ) = ( 𝐴 ( 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 addridd ⊒ ( ( πœ‘ ∧ π‘₯ ∈ π‘Œ ) β†’ ( ( 𝑆 ↑ 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 bitrid ⊒ ( ( πœ‘ ∧ π‘₯ ∈ π‘Œ ) β†’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ π‘₯ ) ) ≀ 𝑆 ↔ βˆ€ 𝑀 ∈ 𝑅 ( 𝑁 β€˜ ( 𝐴 βˆ’ π‘₯ ) ) ≀ 𝑀 ) )
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 ) ↔ βˆ€ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 βˆ’ π‘₯ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) )