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 | |
|
minvec.m | |
||
minvec.n | |
||
minvec.u | |
||
minvec.y | |
||
minvec.w | |
||
minvec.a | |
||
minvec.j | |
||
minvec.r | |
||
Assertion | minveclem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | minvec.x | |
|
2 | minvec.m | |
|
3 | minvec.n | |
|
4 | minvec.u | |
|
5 | minvec.y | |
|
6 | minvec.w | |
|
7 | minvec.a | |
|
8 | minvec.j | |
|
9 | minvec.r | |
|
10 | cphngp | |
|
11 | 4 10 | syl | |
12 | cphlmod | |
|
13 | 4 12 | syl | |
14 | 13 | adantr | |
15 | 7 | adantr | |
16 | eqid | |
|
17 | 1 16 | lssss | |
18 | 5 17 | syl | |
19 | 18 | sselda | |
20 | 1 2 | lmodvsubcl | |
21 | 14 15 19 20 | syl3anc | |
22 | 1 3 | nmcl | |
23 | 11 21 22 | syl2an2r | |
24 | 23 | fmpttd | |
25 | 24 | frnd | |
26 | 9 25 | eqsstrid | |
27 | 16 | lssn0 | |
28 | 5 27 | syl | |
29 | 9 | eqeq1i | |
30 | dm0rn0 | |
|
31 | fvex | |
|
32 | eqid | |
|
33 | 31 32 | dmmpti | |
34 | 33 | eqeq1i | |
35 | 29 30 34 | 3bitr2i | |
36 | 35 | necon3bii | |
37 | 28 36 | sylibr | |
38 | 1 3 | nmge0 | |
39 | 11 21 38 | syl2an2r | |
40 | 39 | ralrimiva | |
41 | 31 | rgenw | |
42 | breq2 | |
|
43 | 32 42 | ralrnmptw | |
44 | 41 43 | ax-mp | |
45 | 40 44 | sylibr | |
46 | 9 | raleqi | |
47 | 45 46 | sylibr | |
48 | 26 37 47 | 3jca | |