Metamath Proof Explorer

Theorem hoiqssbl

Description: A n-dimensional ball contains a nonempty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hoiqssbl.x 
|- ( ph -> X e. Fin )
hoiqssbl.y 
|- ( ph -> Y e. ( RR ^m X ) )
hoiqssbl.e 
|- ( ph -> E e. RR+ )
Assertion hoiqssbl 
|- ( ph -> E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) ) )

Proof

Step Hyp Ref Expression
1 hoiqssbl.x 
 |-  ( ph -> X e. Fin )
2 hoiqssbl.y 
 |-  ( ph -> Y e. ( RR ^m X ) )
3 hoiqssbl.e 
 |-  ( ph -> E e. RR+ )
4 0ex 
 |-  (/) e. _V
5 4 snid 
 |-  (/) e. { (/) }
6 5 a1i 
 |-  ( ( ph /\ X = (/) ) -> (/) e. { (/) } )
7 2 adantr 
 |-  ( ( ph /\ X = (/) ) -> Y e. ( RR ^m X ) )
8 oveq2 
 |-  ( X = (/) -> ( RR ^m X ) = ( RR ^m (/) ) )
9 reex 
 |-  RR e. _V
10 mapdm0 
 |-  ( RR e. _V -> ( RR ^m (/) ) = { (/) } )
11 9 10 ax-mp 
 |-  ( RR ^m (/) ) = { (/) }
12 11 a1i 
 |-  ( X = (/) -> ( RR ^m (/) ) = { (/) } )
13 8 12 eqtrd 
 |-  ( X = (/) -> ( RR ^m X ) = { (/) } )
14 13 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( RR ^m X ) = { (/) } )
15 7 14 eleqtrd 
 |-  ( ( ph /\ X = (/) ) -> Y e. { (/) } )
16 0fin 
 |-  (/) e. Fin
17 eqid 
 |-  ( dist ` ( RR^ ` (/) ) ) = ( dist ` ( RR^ ` (/) ) )
18 17 rrxmetfi 
 |-  ( (/) e. Fin -> ( dist ` ( RR^ ` (/) ) ) e. ( Met ` ( RR ^m (/) ) ) )
19 16 18 ax-mp 
 |-  ( dist ` ( RR^ ` (/) ) ) e. ( Met ` ( RR ^m (/) ) )
20 metxmet 
 |-  ( ( dist ` ( RR^ ` (/) ) ) e. ( Met ` ( RR ^m (/) ) ) -> ( dist ` ( RR^ ` (/) ) ) e. ( *Met ` ( RR ^m (/) ) ) )
21 19 20 ax-mp 
 |-  ( dist ` ( RR^ ` (/) ) ) e. ( *Met ` ( RR ^m (/) ) )
22 21 a1i 
 |-  ( ( ph /\ X = (/) ) -> ( dist ` ( RR^ ` (/) ) ) e. ( *Met ` ( RR ^m (/) ) ) )
23 6 11 eleqtrrdi 
 |-  ( ( ph /\ X = (/) ) -> (/) e. ( RR ^m (/) ) )
24 3 adantr 
 |-  ( ( ph /\ X = (/) ) -> E e. RR+ )
25 blcntr 
 |-  ( ( ( dist ` ( RR^ ` (/) ) ) e. ( *Met ` ( RR ^m (/) ) ) /\ (/) e. ( RR ^m (/) ) /\ E e. RR+ ) -> (/) e. ( (/) ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) )
26 22 23 24 25 syl3anc 
 |-  ( ( ph /\ X = (/) ) -> (/) e. ( (/) ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) )
27 elsni 
 |-  ( Y e. { (/) } -> Y = (/) )
28 15 27 syl 
 |-  ( ( ph /\ X = (/) ) -> Y = (/) )
29 28 eqcomd 
 |-  ( ( ph /\ X = (/) ) -> (/) = Y )
30 29 oveq1d 
 |-  ( ( ph /\ X = (/) ) -> ( (/) ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) = ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) )
31 26 30 eleqtrd 
 |-  ( ( ph /\ X = (/) ) -> (/) e. ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) )
32 31 snssd 
 |-  ( ( ph /\ X = (/) ) -> { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) )
33 15 32 jca 
 |-  ( ( ph /\ X = (/) ) -> ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) )
34 biidd 
 |-  ( d = (/) -> ( ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) <-> ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) ) )
35 34 rspcev 
 |-  ( ( (/) e. { (/) } /\ ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) ) -> E. d e. { (/) } ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) )
36 6 33 35 syl2anc 
 |-  ( ( ph /\ X = (/) ) -> E. d e. { (/) } ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) )
37 biidd 
 |-  ( c = (/) -> ( E. d e. { (/) } ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) <-> E. d e. { (/) } ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) ) )
38 37 rspcev 
 |-  ( ( (/) e. { (/) } /\ E. d e. { (/) } ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) ) -> E. c e. { (/) } E. d e. { (/) } ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) )
39 6 36 38 syl2anc 
 |-  ( ( ph /\ X = (/) ) -> E. c e. { (/) } E. d e. { (/) } ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) )
40 oveq2 
 |-  ( X = (/) -> ( QQ ^m X ) = ( QQ ^m (/) ) )
41 qex 
 |-  QQ e. _V
42 mapdm0 
 |-  ( QQ e. _V -> ( QQ ^m (/) ) = { (/) } )
43 41 42 ax-mp 
 |-  ( QQ ^m (/) ) = { (/) }
44 43 a1i 
 |-  ( X = (/) -> ( QQ ^m (/) ) = { (/) } )
45 40 44 eqtr2d 
 |-  ( X = (/) -> { (/) } = ( QQ ^m X ) )
46 45 eqcomd 
 |-  ( X = (/) -> ( QQ ^m X ) = { (/) } )
47 46 eleq2d 
 |-  ( X = (/) -> ( c e. ( QQ ^m X ) <-> c e. { (/) } ) )
48 46 eleq2d 
 |-  ( X = (/) -> ( d e. ( QQ ^m X ) <-> d e. { (/) } ) )
49 48 anbi1d 
 |-  ( X = (/) -> ( ( d e. ( QQ ^m X ) /\ ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) ) <-> ( d e. { (/) } /\ ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) ) ) )
50 49 rexbidv2 
 |-  ( X = (/) -> ( E. d e. ( QQ ^m X ) ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) <-> E. d e. { (/) } ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) ) )
51 47 50 anbi12d 
 |-  ( X = (/) -> ( ( c e. ( QQ ^m X ) /\ E. d e. ( QQ ^m X ) ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) ) <-> ( c e. { (/) } /\ E. d e. { (/) } ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) ) ) )
52 51 rexbidv2 
 |-  ( X = (/) -> ( E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) <-> E. c e. { (/) } E. d e. { (/) } ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) ) )
53 52 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) <-> E. c e. { (/) } E. d e. { (/) } ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) ) )
54 39 53 mpbird 
 |-  ( ( ph /\ X = (/) ) -> E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) )
55 ixpeq1 
 |-  ( X = (/) -> X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) = X_ i e. (/) ( ( c ` i ) [,) ( d ` i ) ) )
56 ixp0x 
 |-  X_ i e. (/) ( ( c ` i ) [,) ( d ` i ) ) = { (/) }
57 56 a1i 
 |-  ( X = (/) -> X_ i e. (/) ( ( c ` i ) [,) ( d ` i ) ) = { (/) } )
58 55 57 eqtrd 
 |-  ( X = (/) -> X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) = { (/) } )
59 58 eleq2d 
 |-  ( X = (/) -> ( Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) <-> Y e. { (/) } ) )
60 2fveq3 
 |-  ( X = (/) -> ( dist ` ( RR^ ` X ) ) = ( dist ` ( RR^ ` (/) ) ) )
61 60 fveq2d 
 |-  ( X = (/) -> ( ball ` ( dist ` ( RR^ ` X ) ) ) = ( ball ` ( dist ` ( RR^ ` (/) ) ) ) )
62 61 oveqd 
 |-  ( X = (/) -> ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) = ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) )
63 58 62 sseq12d 
 |-  ( X = (/) -> ( X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) <-> { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) )
64 59 63 anbi12d 
 |-  ( X = (/) -> ( ( Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) ) <-> ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) ) )
65 64 rexbidv 
 |-  ( X = (/) -> ( E. d e. ( QQ ^m X ) ( Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) ) <-> E. d e. ( QQ ^m X ) ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) ) )
66 65 rexbidv 
 |-  ( X = (/) -> ( E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) ) <-> E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) ) )
67 66 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) ) <-> E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( Y e. { (/) } /\ { (/) } C_ ( Y ( ball ` ( dist ` ( RR^ ` (/) ) ) ) E ) ) ) )
68 54 67 mpbird 
 |-  ( ( ph /\ X = (/) ) -> E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) ) )
69 1 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> X e. Fin )
70 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
71 70 adantl 
 |-  ( ( ph /\ -. X = (/) ) -> X =/= (/) )
72 2 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> Y e. ( RR ^m X ) )
73 3 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> E e. RR+ )
74 69 71 72 73 hoiqssbllem3 
 |-  ( ( ph /\ -. X = (/) ) -> E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) ) )
75 68 74 pm2.61dan 
 |-  ( ph -> E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) ) )