Metamath Proof Explorer

Theorem minveclem6

Description: Lemma for minvec . Any minimal point is less than S away from A . (Contributed by Mario Carneiro, 9-May-2014) (Revised by Mario Carneiro, 15-Oct-2015) (Revised by AV, 3-Oct-2020)

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 ) ) )
minvec.s 
|- S = inf ( R , RR , < )
minvec.d 
|- D = ( ( dist ` U ) |` ( X X. X ) )
Assertion minveclem6 
|- ( ( ph /\ x e. Y ) -> ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) )

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 minvec.s 
 |-  S = inf ( R , RR , < )
11 minvec.d 
 |-  D = ( ( dist ` U ) |` ( X X. X ) )
12 11 oveqi 
 |-  ( A D x ) = ( A ( ( dist ` U ) |` ( X X. X ) ) x )
13 7 adantr 
 |-  ( ( ph /\ x e. Y ) -> A e. X )
14 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
15 1 14 lssss 
 |-  ( Y e. ( LSubSp ` U ) -> Y C_ X )
16 5 15 syl 
 |-  ( ph -> Y C_ X )
17 16 sselda 
 |-  ( ( ph /\ x e. Y ) -> x e. X )
18 13 17 ovresd 
 |-  ( ( ph /\ x e. Y ) -> ( A ( ( dist ` U ) |` ( X X. X ) ) x ) = ( A ( dist ` U ) x ) )
19 12 18 syl5eq 
 |-  ( ( ph /\ x e. Y ) -> ( A D x ) = ( A ( dist ` U ) x ) )
20 cphngp 
 |-  ( U e. CPreHil -> U e. NrmGrp )
21 4 20 syl 
 |-  ( ph -> U e. NrmGrp )
22 21 adantr 
 |-  ( ( ph /\ x e. Y ) -> U e. NrmGrp )
23 eqid 
 |-  ( dist ` U ) = ( dist ` U )
24 3 1 2 23 ngpds 
 |-  ( ( U e. NrmGrp /\ A e. X /\ x e. X ) -> ( A ( dist ` U ) x ) = ( N ` ( A .- x ) ) )
25 22 13 17 24 syl3anc 
 |-  ( ( ph /\ x e. Y ) -> ( A ( dist ` U ) x ) = ( N ` ( A .- x ) ) )
26 19 25 eqtrd 
 |-  ( ( ph /\ x e. Y ) -> ( A D x ) = ( N ` ( A .- x ) ) )
27 26 oveq1d 
 |-  ( ( ph /\ x e. Y ) -> ( ( A D x ) ^ 2 ) = ( ( N ` ( A .- x ) ) ^ 2 ) )
28 1 2 3 4 5 6 7 8 9 minveclem1 
 |-  ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )
29 28 adantr 
 |-  ( ( ph /\ x e. Y ) -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )
30 29 simp1d 
 |-  ( ( ph /\ x e. Y ) -> R C_ RR )
31 29 simp2d 
 |-  ( ( ph /\ x e. Y ) -> R =/= (/) )
32 0red 
 |-  ( ( ph /\ x e. Y ) -> 0 e. RR )
33 29 simp3d 
 |-  ( ( ph /\ x e. Y ) -> A. w e. R 0 <_ w )
34 breq1 
 |-  ( x = 0 -> ( x <_ w <-> 0 <_ w ) )
35 34 ralbidv 
 |-  ( x = 0 -> ( A. w e. R x <_ w <-> A. w e. R 0 <_ w ) )
36 35 rspcev 
 |-  ( ( 0 e. RR /\ A. w e. R 0 <_ w ) -> E. x e. RR A. w e. R x <_ w )
37 32 33 36 syl2anc 
 |-  ( ( ph /\ x e. Y ) -> E. x e. RR A. w e. R x <_ w )
38 infrecl 
 |-  ( ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) -> inf ( R , RR , < ) e. RR )
39 30 31 37 38 syl3anc 
 |-  ( ( ph /\ x e. Y ) -> inf ( R , RR , < ) e. RR )
40 10 39 eqeltrid 
 |-  ( ( ph /\ x e. Y ) -> S e. RR )
41 40 resqcld 
 |-  ( ( ph /\ x e. Y ) -> ( S ^ 2 ) e. RR )
42 41 recnd 
 |-  ( ( ph /\ x e. Y ) -> ( S ^ 2 ) e. CC )
43 42 addid1d 
 |-  ( ( ph /\ x e. Y ) -> ( ( S ^ 2 ) + 0 ) = ( S ^ 2 ) )
44 27 43 breq12d 
 |-  ( ( ph /\ x e. Y ) -> ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> ( ( N ` ( A .- x ) ) ^ 2 ) <_ ( S ^ 2 ) ) )
45 cphlmod 
 |-  ( U e. CPreHil -> U e. LMod )
46 4 45 syl 
 |-  ( ph -> U e. LMod )
47 46 adantr 
 |-  ( ( ph /\ x e. Y ) -> U e. LMod )
48 1 2 lmodvsubcl 
 |-  ( ( U e. LMod /\ A e. X /\ x e. X ) -> ( A .- x ) e. X )
49 47 13 17 48 syl3anc 
 |-  ( ( ph /\ x e. Y ) -> ( A .- x ) e. X )
50 1 3 nmcl 
 |-  ( ( U e. NrmGrp /\ ( A .- x ) e. X ) -> ( N ` ( A .- x ) ) e. RR )
51 22 49 50 syl2anc 
 |-  ( ( ph /\ x e. Y ) -> ( N ` ( A .- x ) ) e. RR )
52 1 3 nmge0 
 |-  ( ( U e. NrmGrp /\ ( A .- x ) e. X ) -> 0 <_ ( N ` ( A .- x ) ) )
53 22 49 52 syl2anc 
 |-  ( ( ph /\ x e. Y ) -> 0 <_ ( N ` ( A .- x ) ) )
54 infregelb 
 |-  ( ( ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) /\ 0 e. RR ) -> ( 0 <_ inf ( R , RR , < ) <-> A. w e. R 0 <_ w ) )
55 30 31 37 32 54 syl31anc 
 |-  ( ( ph /\ x e. Y ) -> ( 0 <_ inf ( R , RR , < ) <-> A. w e. R 0 <_ w ) )
56 33 55 mpbird 
 |-  ( ( ph /\ x e. Y ) -> 0 <_ inf ( R , RR , < ) )
57 56 10 breqtrrdi 
 |-  ( ( ph /\ x e. Y ) -> 0 <_ S )
58 51 40 53 57 le2sqd 
 |-  ( ( ph /\ x e. Y ) -> ( ( N ` ( A .- x ) ) <_ S <-> ( ( N ` ( A .- x ) ) ^ 2 ) <_ ( S ^ 2 ) ) )
59 10 breq2i 
 |-  ( ( N ` ( A .- x ) ) <_ S <-> ( N ` ( A .- x ) ) <_ inf ( R , RR , < ) )
60 infregelb 
 |-  ( ( ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) /\ ( N ` ( A .- x ) ) e. RR ) -> ( ( N ` ( A .- x ) ) <_ inf ( R , RR , < ) <-> A. w e. R ( N ` ( A .- x ) ) <_ w ) )
61 30 31 37 51 60 syl31anc 
 |-  ( ( ph /\ x e. Y ) -> ( ( N ` ( A .- x ) ) <_ inf ( R , RR , < ) <-> A. w e. R ( N ` ( A .- x ) ) <_ w ) )
62 59 61 syl5bb 
 |-  ( ( ph /\ x e. Y ) -> ( ( N ` ( A .- x ) ) <_ S <-> A. w e. R ( N ` ( A .- x ) ) <_ w ) )
63 44 58 62 3bitr2d 
 |-  ( ( ph /\ x e. Y ) -> ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. w e. R ( N ` ( A .- x ) ) <_ w ) )
64 9 raleqi 
 |-  ( A. w e. R ( N ` ( A .- x ) ) <_ w <-> A. w e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) ( N ` ( A .- x ) ) <_ w )
65 fvex 
 |-  ( N ` ( A .- y ) ) e. _V
66 65 rgenw 
 |-  A. y e. Y ( N ` ( A .- y ) ) e. _V
67 eqid 
 |-  ( y e. Y |-> ( N ` ( A .- y ) ) ) = ( y e. Y |-> ( N ` ( A .- y ) ) )
68 breq2 
 |-  ( w = ( N ` ( A .- y ) ) -> ( ( N ` ( A .- x ) ) <_ w <-> ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) )
69 67 68 ralrnmptw 
 |-  ( A. y e. Y ( N ` ( A .- y ) ) e. _V -> ( A. w e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) ( N ` ( A .- x ) ) <_ w <-> A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) )
70 66 69 ax-mp 
 |-  ( A. w e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) ( N ` ( A .- x ) ) <_ w <-> A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) )
71 64 70 bitri 
 |-  ( A. w e. R ( N ` ( A .- x ) ) <_ w <-> A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) )
72 63 71 bitrdi 
 |-  ( ( ph /\ x e. Y ) -> ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) )