Metamath Proof Explorer

Theorem qndenserrnbl

Description: n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses qndenserrnbl.i 
|- ( ph -> I e. Fin )
qndenserrnbl.x 
|- ( ph -> X e. ( RR ^m I ) )
qndenserrnbl.d 
|- D = ( dist ` ( RR^ ` I ) )
qndenserrnbl.e 
|- ( ph -> E e. RR+ )
Assertion qndenserrnbl 
|- ( ph -> E. y e. ( QQ ^m I ) y e. ( X ( ball ` D ) E ) )

Proof

Step Hyp Ref Expression
1 qndenserrnbl.i 
 |-  ( ph -> I e. Fin )
2 qndenserrnbl.x 
 |-  ( ph -> X e. ( RR ^m I ) )
3 qndenserrnbl.d 
 |-  D = ( dist ` ( RR^ ` I ) )
4 qndenserrnbl.e 
 |-  ( ph -> E e. RR+ )
5 0ex 
 |-  (/) e. _V
6 5 snid 
 |-  (/) e. { (/) }
7 6 a1i 
 |-  ( ( ph /\ I = (/) ) -> (/) e. { (/) } )
8 oveq2 
 |-  ( I = (/) -> ( QQ ^m I ) = ( QQ ^m (/) ) )
9 qex 
 |-  QQ e. _V
10 mapdm0 
 |-  ( QQ e. _V -> ( QQ ^m (/) ) = { (/) } )
11 9 10 ax-mp 
 |-  ( QQ ^m (/) ) = { (/) }
12 11 a1i 
 |-  ( I = (/) -> ( QQ ^m (/) ) = { (/) } )
13 8 12 eqtr2d 
 |-  ( I = (/) -> { (/) } = ( QQ ^m I ) )
14 13 adantl 
 |-  ( ( ph /\ I = (/) ) -> { (/) } = ( QQ ^m I ) )
15 7 14 eleqtrd 
 |-  ( ( ph /\ I = (/) ) -> (/) e. ( QQ ^m I ) )
16 3 rrxmetfi 
 |-  ( I e. Fin -> D e. ( Met ` ( RR ^m I ) ) )
17 1 16 syl 
 |-  ( ph -> D e. ( Met ` ( RR ^m I ) ) )
18 metxmet 
 |-  ( D e. ( Met ` ( RR ^m I ) ) -> D e. ( *Met ` ( RR ^m I ) ) )
19 17 18 syl 
 |-  ( ph -> D e. ( *Met ` ( RR ^m I ) ) )
20 19 adantr 
 |-  ( ( ph /\ I = (/) ) -> D e. ( *Met ` ( RR ^m I ) ) )
21 2 adantr 
 |-  ( ( ph /\ I = (/) ) -> X e. ( RR ^m I ) )
22 oveq2 
 |-  ( I = (/) -> ( RR ^m I ) = ( RR ^m (/) ) )
23 reex 
 |-  RR e. _V
24 mapdm0 
 |-  ( RR e. _V -> ( RR ^m (/) ) = { (/) } )
25 23 24 ax-mp 
 |-  ( RR ^m (/) ) = { (/) }
26 25 a1i 
 |-  ( I = (/) -> ( RR ^m (/) ) = { (/) } )
27 22 26 eqtrd 
 |-  ( I = (/) -> ( RR ^m I ) = { (/) } )
28 27 adantl 
 |-  ( ( ph /\ I = (/) ) -> ( RR ^m I ) = { (/) } )
29 21 28 eleqtrd 
 |-  ( ( ph /\ I = (/) ) -> X e. { (/) } )
30 elsng 
 |-  ( X e. ( RR ^m I ) -> ( X e. { (/) } <-> X = (/) ) )
31 2 30 syl 
 |-  ( ph -> ( X e. { (/) } <-> X = (/) ) )
32 31 adantr 
 |-  ( ( ph /\ I = (/) ) -> ( X e. { (/) } <-> X = (/) ) )
33 29 32 mpbid 
 |-  ( ( ph /\ I = (/) ) -> X = (/) )
34 33 eqcomd 
 |-  ( ( ph /\ I = (/) ) -> (/) = X )
35 34 21 eqeltrd 
 |-  ( ( ph /\ I = (/) ) -> (/) e. ( RR ^m I ) )
36 4 rpxrd 
 |-  ( ph -> E e. RR* )
37 4 rpgt0d 
 |-  ( ph -> 0 < E )
38 36 37 jca 
 |-  ( ph -> ( E e. RR* /\ 0 < E ) )
39 38 adantr 
 |-  ( ( ph /\ I = (/) ) -> ( E e. RR* /\ 0 < E ) )
40 xblcntr 
 |-  ( ( D e. ( *Met ` ( RR ^m I ) ) /\ (/) e. ( RR ^m I ) /\ ( E e. RR* /\ 0 < E ) ) -> (/) e. ( (/) ( ball ` D ) E ) )
41 20 35 39 40 syl3anc 
 |-  ( ( ph /\ I = (/) ) -> (/) e. ( (/) ( ball ` D ) E ) )
42 34 oveq1d 
 |-  ( ( ph /\ I = (/) ) -> ( (/) ( ball ` D ) E ) = ( X ( ball ` D ) E ) )
43 41 42 eleqtrd 
 |-  ( ( ph /\ I = (/) ) -> (/) e. ( X ( ball ` D ) E ) )
44 eleq1 
 |-  ( y = (/) -> ( y e. ( X ( ball ` D ) E ) <-> (/) e. ( X ( ball ` D ) E ) ) )
45 44 rspcev 
 |-  ( ( (/) e. ( QQ ^m I ) /\ (/) e. ( X ( ball ` D ) E ) ) -> E. y e. ( QQ ^m I ) y e. ( X ( ball ` D ) E ) )
46 15 43 45 syl2anc 
 |-  ( ( ph /\ I = (/) ) -> E. y e. ( QQ ^m I ) y e. ( X ( ball ` D ) E ) )
47 1 adantr 
 |-  ( ( ph /\ -. I = (/) ) -> I e. Fin )
48 neqne 
 |-  ( -. I = (/) -> I =/= (/) )
49 48 adantl 
 |-  ( ( ph /\ -. I = (/) ) -> I =/= (/) )
50 2 adantr 
 |-  ( ( ph /\ -. I = (/) ) -> X e. ( RR ^m I ) )
51 4 adantr 
 |-  ( ( ph /\ -. I = (/) ) -> E e. RR+ )
52 47 49 50 3 51 qndenserrnbllem 
 |-  ( ( ph /\ -. I = (/) ) -> E. y e. ( QQ ^m I ) y e. ( X ( ball ` D ) E ) )
53 46 52 pm2.61dan 
 |-  ( ph -> E. y e. ( QQ ^m I ) y e. ( X ( ball ` D ) E ) )