Metamath Proof Explorer

Theorem minvecolem1

Description: Lemma for minveco . 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) (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 ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
Assertion minvecolem1 ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 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 phnv ⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )
12 5 11 syl ⊢ ( 𝜑 → 𝑈 ∈ NrmCVec )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑈 ∈ NrmCVec )
14 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ 𝑋 )
15 elin ⊢ ( 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) ↔ ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝑊 ∈ CBan ) )
16 6 15 sylib ⊢ ( 𝜑 → ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝑊 ∈ CBan ) )
17 16 simpld ⊢ ( 𝜑 → 𝑊 ∈ ( SubSp ‘ 𝑈 ) )
18 eqid ⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
19 1 4 18 sspba ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → 𝑌 ⊆ 𝑋 )
20 12 17 19 syl2anc ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
21 20 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑋 )
22 1 2 nvmcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐴 𝑀 𝑦 ) ∈ 𝑋 )
23 13 14 21 22 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝑀 𝑦 ) ∈ 𝑋 )
24 1 3 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝑀 𝑦 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ ℝ )
25 13 23 24 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ ℝ )
26 25 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) : 𝑌 ⟶ ℝ )
27 26 frnd ⊢ ( 𝜑 → ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) ⊆ ℝ )
28 10 27 eqsstrid ⊢ ( 𝜑 → 𝑅 ⊆ ℝ )
29 16 simprd ⊢ ( 𝜑 → 𝑊 ∈ CBan )
30 bnnv ⊢ ( 𝑊 ∈ CBan → 𝑊 ∈ NrmCVec )
31 eqid ⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
32 4 31 nvzcl ⊢ ( 𝑊 ∈ NrmCVec → ( 0vec ‘ 𝑊 ) ∈ 𝑌 )
33 29 30 32 3syl ⊢ ( 𝜑 → ( 0vec ‘ 𝑊 ) ∈ 𝑌 )
34 fvex ⊢ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ V
35 eqid ⊢ ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
36 34 35 dmmpti ⊢ dom ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) = 𝑌
37 33 36 eleqtrrdi ⊢ ( 𝜑 → ( 0vec ‘ 𝑊 ) ∈ dom ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
38 37 ne0d ⊢ ( 𝜑 → dom ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) ≠ ∅ )
39 dm0rn0 ⊢ ( dom ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) = ∅ ↔ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) = ∅ )
40 10 eqeq1i ⊢ ( 𝑅 = ∅ ↔ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) = ∅ )
41 39 40 bitr4i ⊢ ( dom ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) = ∅ ↔ 𝑅 = ∅ )
42 41 necon3bii ⊢ ( dom ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) ≠ ∅ ↔ 𝑅 ≠ ∅ )
43 38 42 sylib ⊢ ( 𝜑 → 𝑅 ≠ ∅ )
44 1 3 nvge0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝑀 𝑦 ) ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
45 13 23 44 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 0 ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
46 45 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑌 0 ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
47 34 rgenw ⊢ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ V
48 breq2 ⊢ ( 𝑤 = ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) → ( 0 ≤ 𝑤 ↔ 0 ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
49 35 48 ralrnmptw ⊢ ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ V → ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) 0 ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 0 ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
50 47 49 ax-mp ⊢ ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) 0 ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 0 ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
51 46 50 sylibr ⊢ ( 𝜑 → ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) 0 ≤ 𝑤 )
52 10 raleqi ⊢ ( ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ↔ ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) 0 ≤ 𝑤 )
53 51 52 sylibr ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 )
54 28 43 53 3jca ⊢ ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )