Metamath Proof Explorer

Theorem minveclem1

Description: Lemma for minvec . The set of all distances from points of Y to A are a nonempty set of nonnegative reals. (Contributed by Mario Carneiro, 8-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 ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
Assertion minveclem1 ( πœ‘ β†’ ( 𝑅 βŠ† ℝ ∧ 𝑅 β‰  βˆ… ∧ βˆ€ 𝑀 ∈ 𝑅 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 cphngp ⊒ ( π‘ˆ ∈ β„‚PreHil β†’ π‘ˆ ∈ NrmGrp )
11 4 10 syl ⊒ ( πœ‘ β†’ π‘ˆ ∈ NrmGrp )
12 cphlmod ⊒ ( π‘ˆ ∈ β„‚PreHil β†’ π‘ˆ ∈ LMod )
13 4 12 syl ⊒ ( πœ‘ β†’ π‘ˆ ∈ LMod )
14 13 adantr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ π‘ˆ ∈ LMod )
15 7 adantr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ 𝐴 ∈ 𝑋 )
16 eqid ⊒ ( LSubSp β€˜ π‘ˆ ) = ( LSubSp β€˜ π‘ˆ )
17 1 16 lssss ⊒ ( π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) β†’ π‘Œ βŠ† 𝑋 )
18 5 17 syl ⊒ ( πœ‘ β†’ π‘Œ βŠ† 𝑋 )
19 18 sselda ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑦 ∈ 𝑋 )
20 1 2 lmodvsubcl ⊒ ( ( π‘ˆ ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) β†’ ( 𝐴 βˆ’ 𝑦 ) ∈ 𝑋 )
21 14 15 19 20 syl3anc ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝐴 βˆ’ 𝑦 ) ∈ 𝑋 )
22 1 3 nmcl ⊒ ( ( π‘ˆ ∈ NrmGrp ∧ ( 𝐴 βˆ’ 𝑦 ) ∈ 𝑋 ) β†’ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ∈ ℝ )
23 11 21 22 syl2an2r ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ∈ ℝ )
24 23 fmpttd ⊒ ( πœ‘ β†’ ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) : π‘Œ ⟢ ℝ )
25 24 frnd ⊒ ( πœ‘ β†’ ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) βŠ† ℝ )
26 9 25 eqsstrid ⊒ ( πœ‘ β†’ 𝑅 βŠ† ℝ )
27 16 lssn0 ⊒ ( π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) β†’ π‘Œ β‰  βˆ… )
28 5 27 syl ⊒ ( πœ‘ β†’ π‘Œ β‰  βˆ… )
29 9 eqeq1i ⊒ ( 𝑅 = βˆ… ↔ ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) = βˆ… )
30 dm0rn0 ⊒ ( dom ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) = βˆ… ↔ ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) = βˆ… )
31 fvex ⊒ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ∈ V
32 eqid ⊒ ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) = ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
33 31 32 dmmpti ⊒ dom ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) = π‘Œ
34 33 eqeq1i ⊒ ( dom ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) = βˆ… ↔ π‘Œ = βˆ… )
35 29 30 34 3bitr2i ⊒ ( 𝑅 = βˆ… ↔ π‘Œ = βˆ… )
36 35 necon3bii ⊒ ( 𝑅 β‰  βˆ… ↔ π‘Œ β‰  βˆ… )
37 28 36 sylibr ⊒ ( πœ‘ β†’ 𝑅 β‰  βˆ… )
38 1 3 nmge0 ⊒ ( ( π‘ˆ ∈ NrmGrp ∧ ( 𝐴 βˆ’ 𝑦 ) ∈ 𝑋 ) β†’ 0 ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
39 11 21 38 syl2an2r ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ 0 ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
40 39 ralrimiva ⊒ ( πœ‘ β†’ βˆ€ 𝑦 ∈ π‘Œ 0 ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
41 31 rgenw ⊒ βˆ€ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ∈ V
42 breq2 ⊒ ( 𝑀 = ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) β†’ ( 0 ≀ 𝑀 ↔ 0 ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) )
43 32 42 ralrnmptw ⊒ ( βˆ€ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ∈ V β†’ ( βˆ€ 𝑀 ∈ ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) 0 ≀ 𝑀 ↔ βˆ€ 𝑦 ∈ π‘Œ 0 ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) )
44 41 43 ax-mp ⊒ ( βˆ€ 𝑀 ∈ ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) 0 ≀ 𝑀 ↔ βˆ€ 𝑦 ∈ π‘Œ 0 ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
45 40 44 sylibr ⊒ ( πœ‘ β†’ βˆ€ 𝑀 ∈ ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) 0 ≀ 𝑀 )
46 9 raleqi ⊒ ( βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ↔ βˆ€ 𝑀 ∈ ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) 0 ≀ 𝑀 )
47 45 46 sylibr ⊒ ( πœ‘ β†’ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 )
48 26 37 47 3jca ⊒ ( πœ‘ β†’ ( 𝑅 βŠ† ℝ ∧ 𝑅 β‰  βˆ… ∧ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) )