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 = ( Base ` U )
minvec.m 
|- .- = ( -g ` U )
minvec.n 
|- N = ( norm ` U )
minvec.u 
|- ( ph -> U e. CPreHil )
minvec.y 
|- ( ph -> Y e. ( LSubSp ` U ) )
minvec.w 
|- ( ph -> ( U |`s Y ) e. CMetSp )
minvec.a 
|- ( ph -> A e. X )
minvec.j 
|- J = ( TopOpen ` U )
minvec.r 
|- R = ran ( y e. Y |-> ( N ` ( A .- y ) ) )
Assertion minveclem1 
|- ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )

Proof

Step Hyp Ref Expression
1 minvec.x 
 |-  X = ( Base ` U )
2 minvec.m 
 |-  .- = ( -g ` U )
3 minvec.n 
 |-  N = ( norm ` U )
4 minvec.u 
 |-  ( ph -> U e. CPreHil )
5 minvec.y 
 |-  ( ph -> Y e. ( LSubSp ` U ) )
6 minvec.w 
 |-  ( ph -> ( U |`s Y ) e. CMetSp )
7 minvec.a 
 |-  ( ph -> A e. X )
8 minvec.j 
 |-  J = ( TopOpen ` U )
9 minvec.r 
 |-  R = ran ( y e. Y |-> ( N ` ( A .- y ) ) )
10 cphngp 
 |-  ( U e. CPreHil -> U e. NrmGrp )
11 4 10 syl 
 |-  ( ph -> U e. NrmGrp )
12 cphlmod 
 |-  ( U e. CPreHil -> U e. LMod )
13 4 12 syl 
 |-  ( ph -> U e. LMod )
14 13 adantr 
 |-  ( ( ph /\ y e. Y ) -> U e. LMod )
15 7 adantr 
 |-  ( ( ph /\ y e. Y ) -> A e. X )
16 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
17 1 16 lssss 
 |-  ( Y e. ( LSubSp ` U ) -> Y C_ X )
18 5 17 syl 
 |-  ( ph -> Y C_ X )
19 18 sselda 
 |-  ( ( ph /\ y e. Y ) -> y e. X )
20 1 2 lmodvsubcl 
 |-  ( ( U e. LMod /\ A e. X /\ y e. X ) -> ( A .- y ) e. X )
21 14 15 19 20 syl3anc 
 |-  ( ( ph /\ y e. Y ) -> ( A .- y ) e. X )
22 1 3 nmcl 
 |-  ( ( U e. NrmGrp /\ ( A .- y ) e. X ) -> ( N ` ( A .- y ) ) e. RR )
23 11 21 22 syl2an2r 
 |-  ( ( ph /\ y e. Y ) -> ( N ` ( A .- y ) ) e. RR )
24 23 fmpttd 
 |-  ( ph -> ( y e. Y |-> ( N ` ( A .- y ) ) ) : Y --> RR )
25 24 frnd 
 |-  ( ph -> ran ( y e. Y |-> ( N ` ( A .- y ) ) ) C_ RR )
26 9 25 eqsstrid 
 |-  ( ph -> R C_ RR )
27 16 lssn0 
 |-  ( Y e. ( LSubSp ` U ) -> Y =/= (/) )
28 5 27 syl 
 |-  ( ph -> Y =/= (/) )
29 9 eqeq1i 
 |-  ( R = (/) <-> ran ( y e. Y |-> ( N ` ( A .- y ) ) ) = (/) )
30 dm0rn0 
 |-  ( dom ( y e. Y |-> ( N ` ( A .- y ) ) ) = (/) <-> ran ( y e. Y |-> ( N ` ( A .- y ) ) ) = (/) )
31 fvex 
 |-  ( N ` ( A .- y ) ) e. _V
32 eqid 
 |-  ( y e. Y |-> ( N ` ( A .- y ) ) ) = ( y e. Y |-> ( N ` ( A .- y ) ) )
33 31 32 dmmpti 
 |-  dom ( y e. Y |-> ( N ` ( A .- y ) ) ) = Y
34 33 eqeq1i 
 |-  ( dom ( y e. Y |-> ( N ` ( A .- y ) ) ) = (/) <-> Y = (/) )
35 29 30 34 3bitr2i 
 |-  ( R = (/) <-> Y = (/) )
36 35 necon3bii 
 |-  ( R =/= (/) <-> Y =/= (/) )
37 28 36 sylibr 
 |-  ( ph -> R =/= (/) )
38 1 3 nmge0 
 |-  ( ( U e. NrmGrp /\ ( A .- y ) e. X ) -> 0 <_ ( N ` ( A .- y ) ) )
39 11 21 38 syl2an2r 
 |-  ( ( ph /\ y e. Y ) -> 0 <_ ( N ` ( A .- y ) ) )
40 39 ralrimiva 
 |-  ( ph -> A. y e. Y 0 <_ ( N ` ( A .- y ) ) )
41 31 rgenw 
 |-  A. y e. Y ( N ` ( A .- y ) ) e. _V
42 breq2 
 |-  ( w = ( N ` ( A .- y ) ) -> ( 0 <_ w <-> 0 <_ ( N ` ( A .- y ) ) ) )
43 32 42 ralrnmptw 
 |-  ( A. y e. Y ( N ` ( A .- y ) ) e. _V -> ( A. w e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) 0 <_ w <-> A. y e. Y 0 <_ ( N ` ( A .- y ) ) ) )
44 41 43 ax-mp 
 |-  ( A. w e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) 0 <_ w <-> A. y e. Y 0 <_ ( N ` ( A .- y ) ) )
45 40 44 sylibr 
 |-  ( ph -> A. w e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) 0 <_ w )
46 9 raleqi 
 |-  ( A. w e. R 0 <_ w <-> A. w e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) 0 <_ w )
47 45 46 sylibr 
 |-  ( ph -> A. w e. R 0 <_ w )
48 26 37 47 3jca 
 |-  ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )