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 X=BaseU
minvec.m -˙=-U
minvec.n N=normU
minvec.u φUCPreHil
minvec.y φYLSubSpU
minvec.w φU𝑠YCMetSp
minvec.a φAX
minvec.j J=TopOpenU
minvec.r R=ranyYNA-˙y
Assertion minveclem1 φRRwR0w

Proof

Step Hyp Ref Expression
1 minvec.x X=BaseU
2 minvec.m -˙=-U
3 minvec.n N=normU
4 minvec.u φUCPreHil
5 minvec.y φYLSubSpU
6 minvec.w φU𝑠YCMetSp
7 minvec.a φAX
8 minvec.j J=TopOpenU
9 minvec.r R=ranyYNA-˙y
10 cphngp UCPreHilUNrmGrp
11 4 10 syl φUNrmGrp
12 cphlmod UCPreHilULMod
13 4 12 syl φULMod
14 13 adantr φyYULMod
15 7 adantr φyYAX
16 eqid LSubSpU=LSubSpU
17 1 16 lssss YLSubSpUYX
18 5 17 syl φYX
19 18 sselda φyYyX
20 1 2 lmodvsubcl ULModAXyXA-˙yX
21 14 15 19 20 syl3anc φyYA-˙yX
22 1 3 nmcl UNrmGrpA-˙yXNA-˙y
23 11 21 22 syl2an2r φyYNA-˙y
24 23 fmpttd φyYNA-˙y:Y
25 24 frnd φranyYNA-˙y
26 9 25 eqsstrid φR
27 16 lssn0 YLSubSpUY
28 5 27 syl φY
29 9 eqeq1i R=ranyYNA-˙y=
30 dm0rn0 domyYNA-˙y=ranyYNA-˙y=
31 fvex NA-˙yV
32 eqid yYNA-˙y=yYNA-˙y
33 31 32 dmmpti domyYNA-˙y=Y
34 33 eqeq1i domyYNA-˙y=Y=
35 29 30 34 3bitr2i R=Y=
36 35 necon3bii RY
37 28 36 sylibr φR
38 1 3 nmge0 UNrmGrpA-˙yX0NA-˙y
39 11 21 38 syl2an2r φyY0NA-˙y
40 39 ralrimiva φyY0NA-˙y
41 31 rgenw yYNA-˙yV
42 breq2 w=NA-˙y0w0NA-˙y
43 32 42 ralrnmptw yYNA-˙yVwranyYNA-˙y0wyY0NA-˙y
44 41 43 ax-mp wranyYNA-˙y0wyY0NA-˙y
45 40 44 sylibr φwranyYNA-˙y0w
46 9 raleqi wR0wwranyYNA-˙y0w
47 45 46 sylibr φwR0w
48 26 37 47 3jca φRRwR0w