Metamath Proof Explorer

Theorem minveclem3

Description: Lemma for minvec . The filter formed by taking elements successively closer to the infimum is Cauchy. (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 ) ) )
minvec.s 
|- S = inf ( R , RR , < )
minvec.d 
|- D = ( ( dist ` U ) |` ( X X. X ) )
minvec.f 
|- F = ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
Assertion minveclem3 
|- ( ph -> ( Y filGen F ) e. ( CauFil ` ( D |` ( Y X. 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 minvec.f 
 |-  F = ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
13 simpr 
 |-  ( ( ph /\ s e. RR+ ) -> s e. RR+ )
14 2z 
 |-  2 e. ZZ
15 rpexpcl 
 |-  ( ( s e. RR+ /\ 2 e. ZZ ) -> ( s ^ 2 ) e. RR+ )
16 13 14 15 sylancl 
 |-  ( ( ph /\ s e. RR+ ) -> ( s ^ 2 ) e. RR+ )
17 16 rphalfcld 
 |-  ( ( ph /\ s e. RR+ ) -> ( ( s ^ 2 ) / 2 ) e. RR+ )
18 4nn 
 |-  4 e. NN
19 nnrp 
 |-  ( 4 e. NN -> 4 e. RR+ )
20 18 19 ax-mp 
 |-  4 e. RR+
21 rpdivcl 
 |-  ( ( ( ( s ^ 2 ) / 2 ) e. RR+ /\ 4 e. RR+ ) -> ( ( ( s ^ 2 ) / 2 ) / 4 ) e. RR+ )
22 17 20 21 sylancl 
 |-  ( ( ph /\ s e. RR+ ) -> ( ( ( s ^ 2 ) / 2 ) / 4 ) e. RR+ )
23 5 adantr 
 |-  ( ( ph /\ s e. RR+ ) -> Y e. ( LSubSp ` U ) )
24 rabexg 
 |-  ( Y e. ( LSubSp ` U ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } e. _V )
25 23 24 syl 
 |-  ( ( ph /\ s e. RR+ ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } e. _V )
26 eqid 
 |-  ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) = ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
27 oveq2 
 |-  ( r = ( ( ( s ^ 2 ) / 2 ) / 4 ) -> ( ( S ^ 2 ) + r ) = ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) )
28 27 breq2d 
 |-  ( r = ( ( ( s ^ 2 ) / 2 ) / 4 ) -> ( ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) <-> ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) )
29 28 rabbidv 
 |-  ( r = ( ( ( s ^ 2 ) / 2 ) / 4 ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } = { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } )
30 26 29 elrnmpt1s 
 |-  ( ( ( ( ( s ^ 2 ) / 2 ) / 4 ) e. RR+ /\ { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } e. _V ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } e. ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) )
31 22 25 30 syl2anc 
 |-  ( ( ph /\ s e. RR+ ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } e. ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) )
32 31 12 eleqtrrdi 
 |-  ( ( ph /\ s e. RR+ ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } e. F )
33 oveq2 
 |-  ( y = u -> ( A D y ) = ( A D u ) )
34 33 oveq1d 
 |-  ( y = u -> ( ( A D y ) ^ 2 ) = ( ( A D u ) ^ 2 ) )
35 34 breq1d 
 |-  ( y = u -> ( ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) <-> ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) )
36 35 elrab 
 |-  ( u e. { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } <-> ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) )
37 oveq2 
 |-  ( y = v -> ( A D y ) = ( A D v ) )
38 37 oveq1d 
 |-  ( y = v -> ( ( A D y ) ^ 2 ) = ( ( A D v ) ^ 2 ) )
39 38 breq1d 
 |-  ( y = v -> ( ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) <-> ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) )
40 39 elrab 
 |-  ( v e. { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } <-> ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) )
41 36 40 anbi12i 
 |-  ( ( u e. { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } /\ v e. { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } ) <-> ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) )
42 simprll 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> u e. Y )
43 simprrl 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> v e. Y )
44 42 43 ovresd 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( u ( D |` ( Y X. Y ) ) v ) = ( u D v ) )
45 cphngp 
 |-  ( U e. CPreHil -> U e. NrmGrp )
46 ngpms 
 |-  ( U e. NrmGrp -> U e. MetSp )
47 1 11 msmet 
 |-  ( U e. MetSp -> D e. ( Met ` X ) )
48 4 45 46 47 4syl 
 |-  ( ph -> D e. ( Met ` X ) )
49 48 ad2antrr 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> D e. ( Met ` X ) )
50 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
51 1 50 lssss 
 |-  ( Y e. ( LSubSp ` U ) -> Y C_ X )
52 5 51 syl 
 |-  ( ph -> Y C_ X )
53 52 ad2antrr 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> Y C_ X )
54 53 42 sseldd 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> u e. X )
55 53 43 sseldd 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> v e. X )
56 metcl 
 |-  ( ( D e. ( Met ` X ) /\ u e. X /\ v e. X ) -> ( u D v ) e. RR )
57 49 54 55 56 syl3anc 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( u D v ) e. RR )
58 57 resqcld 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( ( u D v ) ^ 2 ) e. RR )
59 17 adantr 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( ( s ^ 2 ) / 2 ) e. RR+ )
60 59 rpred 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( ( s ^ 2 ) / 2 ) e. RR )
61 16 adantr 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( s ^ 2 ) e. RR+ )
62 61 rpred 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( s ^ 2 ) e. RR )
63 4 ad2antrr 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> U e. CPreHil )
64 5 ad2antrr 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> Y e. ( LSubSp ` U ) )
65 6 ad2antrr 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( U |`s Y ) e. CMetSp )
66 7 ad2antrr 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> A e. X )
67 22 adantr 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( ( ( s ^ 2 ) / 2 ) / 4 ) e. RR+ )
68 67 rpred 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( ( ( s ^ 2 ) / 2 ) / 4 ) e. RR )
69 67 rpge0d 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> 0 <_ ( ( ( s ^ 2 ) / 2 ) / 4 ) )
70 simprlr 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) )
71 simprrr 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) )
72 1 2 3 63 64 65 66 8 9 10 11 68 69 42 43 70 71 minveclem2 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( ( u D v ) ^ 2 ) <_ ( 4 x. ( ( ( s ^ 2 ) / 2 ) / 4 ) ) )
73 59 rpcnd 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( ( s ^ 2 ) / 2 ) e. CC )
74 4cn 
 |-  4 e. CC
75 74 a1i 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> 4 e. CC )
76 4ne0 
 |-  4 =/= 0
77 76 a1i 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> 4 =/= 0 )
78 73 75 77 divcan2d 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( 4 x. ( ( ( s ^ 2 ) / 2 ) / 4 ) ) = ( ( s ^ 2 ) / 2 ) )
79 72 78 breqtrd 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( ( u D v ) ^ 2 ) <_ ( ( s ^ 2 ) / 2 ) )
80 rphalflt 
 |-  ( ( s ^ 2 ) e. RR+ -> ( ( s ^ 2 ) / 2 ) < ( s ^ 2 ) )
81 61 80 syl 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( ( s ^ 2 ) / 2 ) < ( s ^ 2 ) )
82 58 60 62 79 81 lelttrd 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( ( u D v ) ^ 2 ) < ( s ^ 2 ) )
83 rpre 
 |-  ( s e. RR+ -> s e. RR )
84 83 ad2antlr 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> s e. RR )
85 metge0 
 |-  ( ( D e. ( Met ` X ) /\ u e. X /\ v e. X ) -> 0 <_ ( u D v ) )
86 49 54 55 85 syl3anc 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> 0 <_ ( u D v ) )
87 rpge0 
 |-  ( s e. RR+ -> 0 <_ s )
88 87 ad2antlr 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> 0 <_ s )
89 57 84 86 88 lt2sqd 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( ( u D v ) < s <-> ( ( u D v ) ^ 2 ) < ( s ^ 2 ) ) )
90 82 89 mpbird 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( u D v ) < s )
91 44 90 eqbrtrd 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( ( u e. Y /\ ( ( A D u ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) /\ ( v e. Y /\ ( ( A D v ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) ) ) ) -> ( u ( D |` ( Y X. Y ) ) v ) < s )
92 41 91 sylan2b 
 |-  ( ( ( ph /\ s e. RR+ ) /\ ( u e. { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } /\ v e. { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } ) ) -> ( u ( D |` ( Y X. Y ) ) v ) < s )
93 92 ralrimivva 
 |-  ( ( ph /\ s e. RR+ ) -> A. u e. { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } A. v e. { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } ( u ( D |` ( Y X. Y ) ) v ) < s )
94 raleq 
 |-  ( w = { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } -> ( A. v e. w ( u ( D |` ( Y X. Y ) ) v ) < s <-> A. v e. { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } ( u ( D |` ( Y X. Y ) ) v ) < s ) )
95 94 raleqbi1dv 
 |-  ( w = { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } -> ( A. u e. w A. v e. w ( u ( D |` ( Y X. Y ) ) v ) < s <-> A. u e. { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } A. v e. { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } ( u ( D |` ( Y X. Y ) ) v ) < s ) )
96 95 rspcev 
 |-  ( ( { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } e. F /\ A. u e. { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } A. v e. { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( ( ( s ^ 2 ) / 2 ) / 4 ) ) } ( u ( D |` ( Y X. Y ) ) v ) < s ) -> E. w e. F A. u e. w A. v e. w ( u ( D |` ( Y X. Y ) ) v ) < s )
97 32 93 96 syl2anc 
 |-  ( ( ph /\ s e. RR+ ) -> E. w e. F A. u e. w A. v e. w ( u ( D |` ( Y X. Y ) ) v ) < s )
98 97 ralrimiva 
 |-  ( ph -> A. s e. RR+ E. w e. F A. u e. w A. v e. w ( u ( D |` ( Y X. Y ) ) v ) < s )
99 1 2 3 4 5 6 7 8 9 10 11 minveclem3a 
 |-  ( ph -> ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) )
100 cmetmet 
 |-  ( ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) -> ( D |` ( Y X. Y ) ) e. ( Met ` Y ) )
101 metxmet 
 |-  ( ( D |` ( Y X. Y ) ) e. ( Met ` Y ) -> ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) )
102 99 100 101 3syl 
 |-  ( ph -> ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) )
103 1 2 3 4 5 6 7 8 9 10 11 12 minveclem3b 
 |-  ( ph -> F e. ( fBas ` Y ) )
104 fgcfil 
 |-  ( ( ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) /\ F e. ( fBas ` Y ) ) -> ( ( Y filGen F ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) <-> A. s e. RR+ E. w e. F A. u e. w A. v e. w ( u ( D |` ( Y X. Y ) ) v ) < s ) )
105 102 103 104 syl2anc 
 |-  ( ph -> ( ( Y filGen F ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) <-> A. s e. RR+ E. w e. F A. u e. w A. v e. w ( u ( D |` ( Y X. Y ) ) v ) < s ) )
106 98 105 mpbird 
 |-  ( ph -> ( Y filGen F ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) )