Metamath Proof Explorer

Theorem minveclem3b

Description: Lemma for minvec . The set of vectors within a fixed distance of the infimum forms a filter base. (Contributed 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 ) )
minvec.f 
|- F = ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
Assertion minveclem3b 
|- ( ph -> F e. ( fBas ` 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 ssrab2 
 |-  { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } C_ Y
14 5 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> Y e. ( LSubSp ` U ) )
15 elpw2g 
 |-  ( Y e. ( LSubSp ` U ) -> ( { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } e. ~P Y <-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } C_ Y ) )
16 14 15 syl 
 |-  ( ( ph /\ r e. RR+ ) -> ( { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } e. ~P Y <-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } C_ Y ) )
17 13 16 mpbiri 
 |-  ( ( ph /\ r e. RR+ ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } e. ~P Y )
18 17 fmpttd 
 |-  ( ph -> ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) : RR+ --> ~P Y )
19 18 frnd 
 |-  ( ph -> ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) C_ ~P Y )
20 12 19 eqsstrid 
 |-  ( ph -> F C_ ~P Y )
21 1rp 
 |-  1 e. RR+
22 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 ) } )
23 22 17 dmmptd 
 |-  ( ph -> dom ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) = RR+ )
24 21 23 eleqtrrid 
 |-  ( ph -> 1 e. dom ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) )
25 24 ne0d 
 |-  ( ph -> dom ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) =/= (/) )
26 dm0rn0 
 |-  ( dom ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) = (/) <-> ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) = (/) )
27 12 eqeq1i 
 |-  ( F = (/) <-> ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) = (/) )
28 26 27 bitr4i 
 |-  ( dom ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) = (/) <-> F = (/) )
29 28 necon3bii 
 |-  ( dom ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) =/= (/) <-> F =/= (/) )
30 25 29 sylib 
 |-  ( ph -> F =/= (/) )
31 1 2 3 4 5 6 7 8 9 10 minveclem4c 
 |-  ( ph -> S e. RR )
32 31 resqcld 
 |-  ( ph -> ( S ^ 2 ) e. RR )
33 ltaddrp 
 |-  ( ( ( S ^ 2 ) e. RR /\ r e. RR+ ) -> ( S ^ 2 ) < ( ( S ^ 2 ) + r ) )
34 32 33 sylan 
 |-  ( ( ph /\ r e. RR+ ) -> ( S ^ 2 ) < ( ( S ^ 2 ) + r ) )
35 32 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> ( S ^ 2 ) e. RR )
36 rpre 
 |-  ( r e. RR+ -> r e. RR )
37 36 adantl 
 |-  ( ( ph /\ r e. RR+ ) -> r e. RR )
38 35 37 readdcld 
 |-  ( ( ph /\ r e. RR+ ) -> ( ( S ^ 2 ) + r ) e. RR )
39 38 recnd 
 |-  ( ( ph /\ r e. RR+ ) -> ( ( S ^ 2 ) + r ) e. CC )
40 39 sqsqrtd 
 |-  ( ( ph /\ r e. RR+ ) -> ( ( sqrt ` ( ( S ^ 2 ) + r ) ) ^ 2 ) = ( ( S ^ 2 ) + r ) )
41 34 40 breqtrrd 
 |-  ( ( ph /\ r e. RR+ ) -> ( S ^ 2 ) < ( ( sqrt ` ( ( S ^ 2 ) + r ) ) ^ 2 ) )
42 1 2 3 4 5 6 7 8 9 minveclem1 
 |-  ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )
43 42 simp1d 
 |-  ( ph -> R C_ RR )
44 43 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> R C_ RR )
45 42 simp2d 
 |-  ( ph -> R =/= (/) )
46 45 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> R =/= (/) )
47 0re 
 |-  0 e. RR
48 42 simp3d 
 |-  ( ph -> A. w e. R 0 <_ w )
49 breq1 
 |-  ( y = 0 -> ( y <_ w <-> 0 <_ w ) )
50 49 ralbidv 
 |-  ( y = 0 -> ( A. w e. R y <_ w <-> A. w e. R 0 <_ w ) )
51 50 rspcev 
 |-  ( ( 0 e. RR /\ A. w e. R 0 <_ w ) -> E. y e. RR A. w e. R y <_ w )
52 47 48 51 sylancr 
 |-  ( ph -> E. y e. RR A. w e. R y <_ w )
53 52 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> E. y e. RR A. w e. R y <_ w )
54 infrecl 
 |-  ( ( R C_ RR /\ R =/= (/) /\ E. y e. RR A. w e. R y <_ w ) -> inf ( R , RR , < ) e. RR )
55 44 46 53 54 syl3anc 
 |-  ( ( ph /\ r e. RR+ ) -> inf ( R , RR , < ) e. RR )
56 10 55 eqeltrid 
 |-  ( ( ph /\ r e. RR+ ) -> S e. RR )
57 0red 
 |-  ( ( ph /\ r e. RR+ ) -> 0 e. RR )
58 56 sqge0d 
 |-  ( ( ph /\ r e. RR+ ) -> 0 <_ ( S ^ 2 ) )
59 57 35 38 58 34 lelttrd 
 |-  ( ( ph /\ r e. RR+ ) -> 0 < ( ( S ^ 2 ) + r ) )
60 57 38 59 ltled 
 |-  ( ( ph /\ r e. RR+ ) -> 0 <_ ( ( S ^ 2 ) + r ) )
61 38 60 resqrtcld 
 |-  ( ( ph /\ r e. RR+ ) -> ( sqrt ` ( ( S ^ 2 ) + r ) ) e. RR )
62 48 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> A. w e. R 0 <_ w )
63 infregelb 
 |-  ( ( ( R C_ RR /\ R =/= (/) /\ E. y e. RR A. w e. R y <_ w ) /\ 0 e. RR ) -> ( 0 <_ inf ( R , RR , < ) <-> A. w e. R 0 <_ w ) )
64 44 46 53 57 63 syl31anc 
 |-  ( ( ph /\ r e. RR+ ) -> ( 0 <_ inf ( R , RR , < ) <-> A. w e. R 0 <_ w ) )
65 62 64 mpbird 
 |-  ( ( ph /\ r e. RR+ ) -> 0 <_ inf ( R , RR , < ) )
66 65 10 breqtrrdi 
 |-  ( ( ph /\ r e. RR+ ) -> 0 <_ S )
67 38 60 sqrtge0d 
 |-  ( ( ph /\ r e. RR+ ) -> 0 <_ ( sqrt ` ( ( S ^ 2 ) + r ) ) )
68 56 61 66 67 lt2sqd 
 |-  ( ( ph /\ r e. RR+ ) -> ( S < ( sqrt ` ( ( S ^ 2 ) + r ) ) <-> ( S ^ 2 ) < ( ( sqrt ` ( ( S ^ 2 ) + r ) ) ^ 2 ) ) )
69 41 68 mpbird 
 |-  ( ( ph /\ r e. RR+ ) -> S < ( sqrt ` ( ( S ^ 2 ) + r ) ) )
70 56 61 ltnled 
 |-  ( ( ph /\ r e. RR+ ) -> ( S < ( sqrt ` ( ( S ^ 2 ) + r ) ) <-> -. ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ S ) )
71 69 70 mpbid 
 |-  ( ( ph /\ r e. RR+ ) -> -. ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ S )
72 10 breq2i 
 |-  ( ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ S <-> ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ inf ( R , RR , < ) )
73 infregelb 
 |-  ( ( ( R C_ RR /\ R =/= (/) /\ E. y e. RR A. w e. R y <_ w ) /\ ( sqrt ` ( ( S ^ 2 ) + r ) ) e. RR ) -> ( ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ inf ( R , RR , < ) <-> A. w e. R ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ w ) )
74 44 46 53 61 73 syl31anc 
 |-  ( ( ph /\ r e. RR+ ) -> ( ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ inf ( R , RR , < ) <-> A. w e. R ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ w ) )
75 9 raleqi 
 |-  ( A. w e. R ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ w <-> A. w e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ w )
76 fvex 
 |-  ( N ` ( A .- y ) ) e. _V
77 76 rgenw 
 |-  A. y e. Y ( N ` ( A .- y ) ) e. _V
78 eqid 
 |-  ( y e. Y |-> ( N ` ( A .- y ) ) ) = ( y e. Y |-> ( N ` ( A .- y ) ) )
79 breq2 
 |-  ( w = ( N ` ( A .- y ) ) -> ( ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ w <-> ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( N ` ( A .- y ) ) ) )
80 78 79 ralrnmptw 
 |-  ( A. y e. Y ( N ` ( A .- y ) ) e. _V -> ( A. w e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ w <-> A. y e. Y ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( N ` ( A .- y ) ) ) )
81 77 80 ax-mp 
 |-  ( A. w e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ w <-> A. y e. Y ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( N ` ( A .- y ) ) )
82 75 81 bitri 
 |-  ( A. w e. R ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ w <-> A. y e. Y ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( N ` ( A .- y ) ) )
83 74 82 bitrdi 
 |-  ( ( ph /\ r e. RR+ ) -> ( ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ inf ( R , RR , < ) <-> A. y e. Y ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( N ` ( A .- y ) ) ) )
84 72 83 syl5bb 
 |-  ( ( ph /\ r e. RR+ ) -> ( ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ S <-> A. y e. Y ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( N ` ( A .- y ) ) ) )
85 71 84 mtbid 
 |-  ( ( ph /\ r e. RR+ ) -> -. A. y e. Y ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( N ` ( A .- y ) ) )
86 rexnal 
 |-  ( E. y e. Y -. ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( N ` ( A .- y ) ) <-> -. A. y e. Y ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( N ` ( A .- y ) ) )
87 85 86 sylibr 
 |-  ( ( ph /\ r e. RR+ ) -> E. y e. Y -. ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( N ` ( A .- y ) ) )
88 61 adantr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( sqrt ` ( ( S ^ 2 ) + r ) ) e. RR )
89 cphngp 
 |-  ( U e. CPreHil -> U e. NrmGrp )
90 4 89 syl 
 |-  ( ph -> U e. NrmGrp )
91 ngpms 
 |-  ( U e. NrmGrp -> U e. MetSp )
92 1 11 msmet 
 |-  ( U e. MetSp -> D e. ( Met ` X ) )
93 90 91 92 3syl 
 |-  ( ph -> D e. ( Met ` X ) )
94 93 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> D e. ( Met ` X ) )
95 7 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> A e. X )
96 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
97 1 96 lssss 
 |-  ( Y e. ( LSubSp ` U ) -> Y C_ X )
98 14 97 syl 
 |-  ( ( ph /\ r e. RR+ ) -> Y C_ X )
99 98 sselda 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> y e. X )
100 metcl 
 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ y e. X ) -> ( A D y ) e. RR )
101 94 95 99 100 syl3anc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( A D y ) e. RR )
102 67 adantr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> 0 <_ ( sqrt ` ( ( S ^ 2 ) + r ) ) )
103 metge0 
 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ y e. X ) -> 0 <_ ( A D y ) )
104 94 95 99 103 syl3anc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> 0 <_ ( A D y ) )
105 88 101 102 104 le2sqd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( A D y ) <-> ( ( sqrt ` ( ( S ^ 2 ) + r ) ) ^ 2 ) <_ ( ( A D y ) ^ 2 ) ) )
106 11 oveqi 
 |-  ( A D y ) = ( A ( ( dist ` U ) |` ( X X. X ) ) y )
107 95 99 ovresd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( A ( ( dist ` U ) |` ( X X. X ) ) y ) = ( A ( dist ` U ) y ) )
108 106 107 syl5eq 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( A D y ) = ( A ( dist ` U ) y ) )
109 90 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> U e. NrmGrp )
110 eqid 
 |-  ( dist ` U ) = ( dist ` U )
111 3 1 2 110 ngpds 
 |-  ( ( U e. NrmGrp /\ A e. X /\ y e. X ) -> ( A ( dist ` U ) y ) = ( N ` ( A .- y ) ) )
112 109 95 99 111 syl3anc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( A ( dist ` U ) y ) = ( N ` ( A .- y ) ) )
113 108 112 eqtrd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( A D y ) = ( N ` ( A .- y ) ) )
114 113 breq2d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( A D y ) <-> ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( N ` ( A .- y ) ) ) )
115 40 adantr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( ( sqrt ` ( ( S ^ 2 ) + r ) ) ^ 2 ) = ( ( S ^ 2 ) + r ) )
116 115 breq1d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( ( ( sqrt ` ( ( S ^ 2 ) + r ) ) ^ 2 ) <_ ( ( A D y ) ^ 2 ) <-> ( ( S ^ 2 ) + r ) <_ ( ( A D y ) ^ 2 ) ) )
117 105 114 116 3bitr3d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( N ` ( A .- y ) ) <-> ( ( S ^ 2 ) + r ) <_ ( ( A D y ) ^ 2 ) ) )
118 117 notbid 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( -. ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( N ` ( A .- y ) ) <-> -. ( ( S ^ 2 ) + r ) <_ ( ( A D y ) ^ 2 ) ) )
119 38 adantr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( ( S ^ 2 ) + r ) e. RR )
120 101 resqcld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( ( A D y ) ^ 2 ) e. RR )
121 119 120 letrid 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( ( ( S ^ 2 ) + r ) <_ ( ( A D y ) ^ 2 ) \/ ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) ) )
122 121 ord 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( -. ( ( S ^ 2 ) + r ) <_ ( ( A D y ) ^ 2 ) -> ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) ) )
123 118 122 sylbid 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( -. ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( N ` ( A .- y ) ) -> ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) ) )
124 123 reximdva 
 |-  ( ( ph /\ r e. RR+ ) -> ( E. y e. Y -. ( sqrt ` ( ( S ^ 2 ) + r ) ) <_ ( N ` ( A .- y ) ) -> E. y e. Y ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) ) )
125 87 124 mpd 
 |-  ( ( ph /\ r e. RR+ ) -> E. y e. Y ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) )
126 rabn0 
 |-  ( { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } =/= (/) <-> E. y e. Y ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) )
127 125 126 sylibr 
 |-  ( ( ph /\ r e. RR+ ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } =/= (/) )
128 127 necomd 
 |-  ( ( ph /\ r e. RR+ ) -> (/) =/= { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
129 128 neneqd 
 |-  ( ( ph /\ r e. RR+ ) -> -. (/) = { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
130 129 nrexdv 
 |-  ( ph -> -. E. r e. RR+ (/) = { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
131 12 eleq2i 
 |-  ( (/) e. F <-> (/) e. ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) )
132 0ex 
 |-  (/) e. _V
133 22 elrnmpt 
 |-  ( (/) e. _V -> ( (/) e. ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) <-> E. r e. RR+ (/) = { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) )
134 132 133 ax-mp 
 |-  ( (/) e. ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) <-> E. r e. RR+ (/) = { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
135 131 134 bitri 
 |-  ( (/) e. F <-> E. r e. RR+ (/) = { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
136 130 135 sylnibr 
 |-  ( ph -> -. (/) e. F )
137 df-nel 
 |-  ( (/) e/ F <-> -. (/) e. F )
138 136 137 sylibr 
 |-  ( ph -> (/) e/ F )
139 56 adantr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> S e. RR )
140 139 resqcld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( S ^ 2 ) e. RR )
141 37 adantr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> r e. RR )
142 120 140 141 lesubadd2d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ y e. Y ) -> ( ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r <-> ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) ) )
143 142 rabbidva 
 |-  ( ( ph /\ r e. RR+ ) -> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } = { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
144 143 mpteq2dva 
 |-  ( ph -> ( 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 ) } ) )
145 144 rneqd 
 |-  ( ph -> ran ( r e. RR+ |-> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } ) = ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) )
146 12 145 eqtr4id 
 |-  ( ph -> F = ran ( r e. RR+ |-> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } ) )
147 146 eleq2d 
 |-  ( ph -> ( u e. F <-> u e. ran ( r e. RR+ |-> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } ) ) )
148 breq2 
 |-  ( r = s -> ( ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r <-> ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s ) )
149 148 rabbidv 
 |-  ( r = s -> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } )
150 149 cbvmptv 
 |-  ( r e. RR+ |-> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } ) = ( s e. RR+ |-> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } )
151 150 elrnmpt 
 |-  ( u e. _V -> ( u e. ran ( r e. RR+ |-> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } ) <-> E. s e. RR+ u = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } ) )
152 151 elv 
 |-  ( u e. ran ( r e. RR+ |-> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } ) <-> E. s e. RR+ u = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } )
153 147 152 bitrdi 
 |-  ( ph -> ( u e. F <-> E. s e. RR+ u = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } ) )
154 146 eleq2d 
 |-  ( ph -> ( v e. F <-> v e. ran ( r e. RR+ |-> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } ) ) )
155 breq2 
 |-  ( r = t -> ( ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r <-> ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t ) )
156 155 rabbidv 
 |-  ( r = t -> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } )
157 156 cbvmptv 
 |-  ( r e. RR+ |-> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } ) = ( t e. RR+ |-> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } )
158 157 elrnmpt 
 |-  ( v e. _V -> ( v e. ran ( r e. RR+ |-> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } ) <-> E. t e. RR+ v = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } ) )
159 158 elv 
 |-  ( v e. ran ( r e. RR+ |-> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } ) <-> E. t e. RR+ v = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } )
160 154 159 bitrdi 
 |-  ( ph -> ( v e. F <-> E. t e. RR+ v = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } ) )
161 153 160 anbi12d 
 |-  ( ph -> ( ( u e. F /\ v e. F ) <-> ( E. s e. RR+ u = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } /\ E. t e. RR+ v = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } ) ) )
162 reeanv 
 |-  ( E. s e. RR+ E. t e. RR+ ( u = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } /\ v = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } ) <-> ( E. s e. RR+ u = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } /\ E. t e. RR+ v = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } ) )
163 93 ad2antrr 
 |-  ( ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) /\ y e. Y ) -> D e. ( Met ` X ) )
164 7 ad2antrr 
 |-  ( ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) /\ y e. Y ) -> A e. X )
165 5 97 syl 
 |-  ( ph -> Y C_ X )
166 165 adantr 
 |-  ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) -> Y C_ X )
167 166 sselda 
 |-  ( ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) /\ y e. Y ) -> y e. X )
168 163 164 167 100 syl3anc 
 |-  ( ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) /\ y e. Y ) -> ( A D y ) e. RR )
169 168 resqcld 
 |-  ( ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) /\ y e. Y ) -> ( ( A D y ) ^ 2 ) e. RR )
170 32 ad2antrr 
 |-  ( ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) /\ y e. Y ) -> ( S ^ 2 ) e. RR )
171 169 170 resubcld 
 |-  ( ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) /\ y e. Y ) -> ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) e. RR )
172 simplrl 
 |-  ( ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) /\ y e. Y ) -> s e. RR+ )
173 172 rpred 
 |-  ( ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) /\ y e. Y ) -> s e. RR )
174 simplrr 
 |-  ( ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) /\ y e. Y ) -> t e. RR+ )
175 174 rpred 
 |-  ( ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) /\ y e. Y ) -> t e. RR )
176 lemin 
 |-  ( ( ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) e. RR /\ s e. RR /\ t e. RR ) -> ( ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ if ( s <_ t , s , t ) <-> ( ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s /\ ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t ) ) )
177 171 173 175 176 syl3anc 
 |-  ( ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) /\ y e. Y ) -> ( ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ if ( s <_ t , s , t ) <-> ( ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s /\ ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t ) ) )
178 177 rabbidva 
 |-  ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) -> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ if ( s <_ t , s , t ) } = { y e. Y | ( ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s /\ ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t ) } )
179 ifcl 
 |-  ( ( s e. RR+ /\ t e. RR+ ) -> if ( s <_ t , s , t ) e. RR+ )
180 5 adantr 
 |-  ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) -> Y e. ( LSubSp ` U ) )
181 rabexg 
 |-  ( Y e. ( LSubSp ` U ) -> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ if ( s <_ t , s , t ) } e. _V )
182 180 181 syl 
 |-  ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) -> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ if ( s <_ t , s , t ) } e. _V )
183 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 } )
184 breq2 
 |-  ( r = if ( s <_ t , s , t ) -> ( ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r <-> ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ if ( s <_ t , s , t ) ) )
185 184 rabbidv 
 |-  ( r = if ( s <_ t , s , t ) -> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ if ( s <_ t , s , t ) } )
186 183 185 elrnmpt1s 
 |-  ( ( if ( s <_ t , s , t ) e. RR+ /\ { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ if ( s <_ t , s , t ) } e. _V ) -> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ if ( s <_ t , s , t ) } e. ran ( r e. RR+ |-> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } ) )
187 179 182 186 syl2an2 
 |-  ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) -> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ if ( s <_ t , s , t ) } e. ran ( r e. RR+ |-> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } ) )
188 146 adantr 
 |-  ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) -> F = ran ( r e. RR+ |-> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ r } ) )
189 187 188 eleqtrrd 
 |-  ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) -> { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ if ( s <_ t , s , t ) } e. F )
190 178 189 eqeltrrd 
 |-  ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) -> { y e. Y | ( ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s /\ ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t ) } e. F )
191 ineq12 
 |-  ( ( u = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } /\ v = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } ) -> ( u i^i v ) = ( { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } i^i { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } ) )
192 inrab 
 |-  ( { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } i^i { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } ) = { y e. Y | ( ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s /\ ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t ) }
193 191 192 eqtrdi 
 |-  ( ( u = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } /\ v = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } ) -> ( u i^i v ) = { y e. Y | ( ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s /\ ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t ) } )
194 193 eleq1d 
 |-  ( ( u = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } /\ v = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } ) -> ( ( u i^i v ) e. F <-> { y e. Y | ( ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s /\ ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t ) } e. F ) )
195 190 194 syl5ibrcom 
 |-  ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) -> ( ( u = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } /\ v = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } ) -> ( u i^i v ) e. F ) )
196 vex 
 |-  u e. _V
197 196 inex1 
 |-  ( u i^i v ) e. _V
198 197 pwid 
 |-  ( u i^i v ) e. ~P ( u i^i v )
199 inelcm 
 |-  ( ( ( u i^i v ) e. F /\ ( u i^i v ) e. ~P ( u i^i v ) ) -> ( F i^i ~P ( u i^i v ) ) =/= (/) )
200 198 199 mpan2 
 |-  ( ( u i^i v ) e. F -> ( F i^i ~P ( u i^i v ) ) =/= (/) )
201 195 200 syl6 
 |-  ( ( ph /\ ( s e. RR+ /\ t e. RR+ ) ) -> ( ( u = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } /\ v = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } ) -> ( F i^i ~P ( u i^i v ) ) =/= (/) ) )
202 201 rexlimdvva 
 |-  ( ph -> ( E. s e. RR+ E. t e. RR+ ( u = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } /\ v = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } ) -> ( F i^i ~P ( u i^i v ) ) =/= (/) ) )
203 162 202 syl5bir 
 |-  ( ph -> ( ( E. s e. RR+ u = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ s } /\ E. t e. RR+ v = { y e. Y | ( ( ( A D y ) ^ 2 ) - ( S ^ 2 ) ) <_ t } ) -> ( F i^i ~P ( u i^i v ) ) =/= (/) ) )
204 161 203 sylbid 
 |-  ( ph -> ( ( u e. F /\ v e. F ) -> ( F i^i ~P ( u i^i v ) ) =/= (/) ) )
205 204 ralrimivv 
 |-  ( ph -> A. u e. F A. v e. F ( F i^i ~P ( u i^i v ) ) =/= (/) )
206 30 138 205 3jca 
 |-  ( ph -> ( F =/= (/) /\ (/) e/ F /\ A. u e. F A. v e. F ( F i^i ~P ( u i^i v ) ) =/= (/) ) )
207 isfbas 
 |-  ( Y e. ( LSubSp ` U ) -> ( F e. ( fBas ` Y ) <-> ( F C_ ~P Y /\ ( F =/= (/) /\ (/) e/ F /\ A. u e. F A. v e. F ( F i^i ~P ( u i^i v ) ) =/= (/) ) ) ) )
208 5 207 syl 
 |-  ( ph -> ( F e. ( fBas ` Y ) <-> ( F C_ ~P Y /\ ( F =/= (/) /\ (/) e/ F /\ A. u e. F A. v e. F ( F i^i ~P ( u i^i v ) ) =/= (/) ) ) ) )
209 20 206 208 mpbir2and 
 |-  ( ph -> F e. ( fBas ` Y ) )