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 
|- X = ( BaseSet ` U )
minveco.m 
|- M = ( -v ` U )
minveco.n 
|- N = ( normCV ` U )
minveco.y 
|- Y = ( BaseSet ` W )
minveco.u 
|- ( ph -> U e. CPreHilOLD )
minveco.w 
|- ( ph -> W e. ( ( SubSp ` U ) i^i CBan ) )
minveco.a 
|- ( ph -> A e. X )
minveco.d 
|- D = ( IndMet ` U )
minveco.j 
|- J = ( MetOpen ` D )
minveco.r 
|- R = ran ( y e. Y |-> ( N ` ( A M y ) ) )
Assertion minvecolem1 
|- ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )

Proof

Step Hyp Ref Expression
1 minveco.x 
 |-  X = ( BaseSet ` U )
2 minveco.m 
 |-  M = ( -v ` U )
3 minveco.n 
 |-  N = ( normCV ` U )
4 minveco.y 
 |-  Y = ( BaseSet ` W )
5 minveco.u 
 |-  ( ph -> U e. CPreHilOLD )
6 minveco.w 
 |-  ( ph -> W e. ( ( SubSp ` U ) i^i CBan ) )
7 minveco.a 
 |-  ( ph -> A e. X )
8 minveco.d 
 |-  D = ( IndMet ` U )
9 minveco.j 
 |-  J = ( MetOpen ` D )
10 minveco.r 
 |-  R = ran ( y e. Y |-> ( N ` ( A M y ) ) )
11 phnv 
 |-  ( U e. CPreHilOLD -> U e. NrmCVec )
12 5 11 syl 
 |-  ( ph -> U e. NrmCVec )
13 12 adantr 
 |-  ( ( ph /\ y e. Y ) -> U e. NrmCVec )
14 7 adantr 
 |-  ( ( ph /\ y e. Y ) -> A e. X )
15 elin 
 |-  ( W e. ( ( SubSp ` U ) i^i CBan ) <-> ( W e. ( SubSp ` U ) /\ W e. CBan ) )
16 6 15 sylib 
 |-  ( ph -> ( W e. ( SubSp ` U ) /\ W e. CBan ) )
17 16 simpld 
 |-  ( ph -> W e. ( SubSp ` U ) )
18 eqid 
 |-  ( SubSp ` U ) = ( SubSp ` U )
19 1 4 18 sspba 
 |-  ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) -> Y C_ X )
20 12 17 19 syl2anc 
 |-  ( ph -> Y C_ X )
21 20 sselda 
 |-  ( ( ph /\ y e. Y ) -> y e. X )
22 1 2 nvmcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ y e. X ) -> ( A M y ) e. X )
23 13 14 21 22 syl3anc 
 |-  ( ( ph /\ y e. Y ) -> ( A M y ) e. X )
24 1 3 nvcl 
 |-  ( ( U e. NrmCVec /\ ( A M y ) e. X ) -> ( N ` ( A M y ) ) e. RR )
25 13 23 24 syl2anc 
 |-  ( ( ph /\ y e. Y ) -> ( N ` ( A M y ) ) e. RR )
26 25 fmpttd 
 |-  ( ph -> ( y e. Y |-> ( N ` ( A M y ) ) ) : Y --> RR )
27 26 frnd 
 |-  ( ph -> ran ( y e. Y |-> ( N ` ( A M y ) ) ) C_ RR )
28 10 27 eqsstrid 
 |-  ( ph -> R C_ RR )
29 16 simprd 
 |-  ( ph -> W e. CBan )
30 bnnv 
 |-  ( W e. CBan -> W e. NrmCVec )
31 eqid 
 |-  ( 0vec ` W ) = ( 0vec ` W )
32 4 31 nvzcl 
 |-  ( W e. NrmCVec -> ( 0vec ` W ) e. Y )
33 29 30 32 3syl 
 |-  ( ph -> ( 0vec ` W ) e. Y )
34 fvex 
 |-  ( N ` ( A M y ) ) e. _V
35 eqid 
 |-  ( y e. Y |-> ( N ` ( A M y ) ) ) = ( y e. Y |-> ( N ` ( A M y ) ) )
36 34 35 dmmpti 
 |-  dom ( y e. Y |-> ( N ` ( A M y ) ) ) = Y
37 33 36 eleqtrrdi 
 |-  ( ph -> ( 0vec ` W ) e. dom ( y e. Y |-> ( N ` ( A M y ) ) ) )
38 37 ne0d 
 |-  ( ph -> dom ( y e. Y |-> ( N ` ( A M y ) ) ) =/= (/) )
39 dm0rn0 
 |-  ( dom ( y e. Y |-> ( N ` ( A M y ) ) ) = (/) <-> ran ( y e. Y |-> ( N ` ( A M y ) ) ) = (/) )
40 10 eqeq1i 
 |-  ( R = (/) <-> ran ( y e. Y |-> ( N ` ( A M y ) ) ) = (/) )
41 39 40 bitr4i 
 |-  ( dom ( y e. Y |-> ( N ` ( A M y ) ) ) = (/) <-> R = (/) )
42 41 necon3bii 
 |-  ( dom ( y e. Y |-> ( N ` ( A M y ) ) ) =/= (/) <-> R =/= (/) )
43 38 42 sylib 
 |-  ( ph -> R =/= (/) )
44 1 3 nvge0 
 |-  ( ( U e. NrmCVec /\ ( A M y ) e. X ) -> 0 <_ ( N ` ( A M y ) ) )
45 13 23 44 syl2anc 
 |-  ( ( ph /\ y e. Y ) -> 0 <_ ( N ` ( A M y ) ) )
46 45 ralrimiva 
 |-  ( ph -> A. y e. Y 0 <_ ( N ` ( A M y ) ) )
47 34 rgenw 
 |-  A. y e. Y ( N ` ( A M y ) ) e. _V
48 breq2 
 |-  ( w = ( N ` ( A M y ) ) -> ( 0 <_ w <-> 0 <_ ( N ` ( A M y ) ) ) )
49 35 48 ralrnmptw 
 |-  ( A. y e. Y ( N ` ( A M y ) ) e. _V -> ( A. w e. ran ( y e. Y |-> ( N ` ( A M y ) ) ) 0 <_ w <-> A. y e. Y 0 <_ ( N ` ( A M y ) ) ) )
50 47 49 ax-mp 
 |-  ( A. w e. ran ( y e. Y |-> ( N ` ( A M y ) ) ) 0 <_ w <-> A. y e. Y 0 <_ ( N ` ( A M y ) ) )
51 46 50 sylibr 
 |-  ( ph -> A. w e. ran ( y e. Y |-> ( N ` ( A M y ) ) ) 0 <_ w )
52 10 raleqi 
 |-  ( A. w e. R 0 <_ w <-> A. w e. ran ( y e. Y |-> ( N ` ( A M y ) ) ) 0 <_ w )
53 51 52 sylibr 
 |-  ( ph -> A. w e. R 0 <_ w )
54 28 43 53 3jca 
 |-  ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )