Metamath Proof Explorer

Theorem qndenserrnopnlem

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 qndenserrnopnlem.i 
|- ( ph -> I e. Fin )
qndenserrnopnlem.j 
|- J = ( TopOpen ` ( RR^ ` I ) )
qndenserrnopnlem.v 
|- ( ph -> V e. J )
qndenserrnopnlem.x 
|- ( ph -> X e. V )
qndenserrnopnlem.d 
|- D = ( dist ` ( RR^ ` I ) )
Assertion qndenserrnopnlem 
|- ( ph -> E. y e. ( QQ ^m I ) y e. V )

Proof

Step Hyp Ref Expression
1 qndenserrnopnlem.i 
 |-  ( ph -> I e. Fin )
2 qndenserrnopnlem.j 
 |-  J = ( TopOpen ` ( RR^ ` I ) )
3 qndenserrnopnlem.v 
 |-  ( ph -> V e. J )
4 qndenserrnopnlem.x 
 |-  ( ph -> X e. V )
5 qndenserrnopnlem.d 
 |-  D = ( dist ` ( RR^ ` I ) )
6 5 rrxmetfi 
 |-  ( I e. Fin -> D e. ( Met ` ( RR ^m I ) ) )
7 1 6 syl 
 |-  ( ph -> D e. ( Met ` ( RR ^m I ) ) )
8 metxmet 
 |-  ( D e. ( Met ` ( RR ^m I ) ) -> D e. ( *Met ` ( RR ^m I ) ) )
9 7 8 syl 
 |-  ( ph -> D e. ( *Met ` ( RR ^m I ) ) )
10 3 2 eleqtrdi 
 |-  ( ph -> V e. ( TopOpen ` ( RR^ ` I ) ) )
11 1 rrxtopnfi 
 |-  ( ph -> ( TopOpen ` ( RR^ ` I ) ) = ( MetOpen ` ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) ) )
12 5 a1i 
 |-  ( ph -> D = ( dist ` ( RR^ ` I ) ) )
13 eqid 
 |-  ( RR^ ` I ) = ( RR^ ` I )
14 eqid 
 |-  ( RR ^m I ) = ( RR ^m I )
15 13 14 rrxdsfi 
 |-  ( I e. Fin -> ( dist ` ( RR^ ` I ) ) = ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
16 1 15 syl 
 |-  ( ph -> ( dist ` ( RR^ ` I ) ) = ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
17 12 16 eqtr2d 
 |-  ( ph -> ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) = D )
18 17 fveq2d 
 |-  ( ph -> ( MetOpen ` ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) ) = ( MetOpen ` D ) )
19 11 18 eqtrd 
 |-  ( ph -> ( TopOpen ` ( RR^ ` I ) ) = ( MetOpen ` D ) )
20 10 19 eleqtrd 
 |-  ( ph -> V e. ( MetOpen ` D ) )
21 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
22 21 mopni2 
 |-  ( ( D e. ( *Met ` ( RR ^m I ) ) /\ V e. ( MetOpen ` D ) /\ X e. V ) -> E. e e. RR+ ( X ( ball ` D ) e ) C_ V )
23 9 20 4 22 syl3anc 
 |-  ( ph -> E. e e. RR+ ( X ( ball ` D ) e ) C_ V )
24 1 3ad2ant1 
 |-  ( ( ph /\ e e. RR+ /\ ( X ( ball ` D ) e ) C_ V ) -> I e. Fin )
25 rrxtps 
 |-  ( I e. Fin -> ( RR^ ` I ) e. TopSp )
26 1 25 syl 
 |-  ( ph -> ( RR^ ` I ) e. TopSp )
27 eqid 
 |-  ( Base ` ( RR^ ` I ) ) = ( Base ` ( RR^ ` I ) )
28 27 2 istps 
 |-  ( ( RR^ ` I ) e. TopSp <-> J e. ( TopOn ` ( Base ` ( RR^ ` I ) ) ) )
29 26 28 sylib 
 |-  ( ph -> J e. ( TopOn ` ( Base ` ( RR^ ` I ) ) ) )
30 1 13 27 rrxbasefi 
 |-  ( ph -> ( Base ` ( RR^ ` I ) ) = ( RR ^m I ) )
31 30 fveq2d 
 |-  ( ph -> ( TopOn ` ( Base ` ( RR^ ` I ) ) ) = ( TopOn ` ( RR ^m I ) ) )
32 29 31 eleqtrd 
 |-  ( ph -> J e. ( TopOn ` ( RR ^m I ) ) )
33 toponss 
 |-  ( ( J e. ( TopOn ` ( RR ^m I ) ) /\ V e. J ) -> V C_ ( RR ^m I ) )
34 32 3 33 syl2anc 
 |-  ( ph -> V C_ ( RR ^m I ) )
35 34 4 sseldd 
 |-  ( ph -> X e. ( RR ^m I ) )
36 35 3ad2ant1 
 |-  ( ( ph /\ e e. RR+ /\ ( X ( ball ` D ) e ) C_ V ) -> X e. ( RR ^m I ) )
37 simp2 
 |-  ( ( ph /\ e e. RR+ /\ ( X ( ball ` D ) e ) C_ V ) -> e e. RR+ )
38 24 36 5 37 qndenserrnbl 
 |-  ( ( ph /\ e e. RR+ /\ ( X ( ball ` D ) e ) C_ V ) -> E. y e. ( QQ ^m I ) y e. ( X ( ball ` D ) e ) )
39 ssel 
 |-  ( ( X ( ball ` D ) e ) C_ V -> ( y e. ( X ( ball ` D ) e ) -> y e. V ) )
40 39 adantr 
 |-  ( ( ( X ( ball ` D ) e ) C_ V /\ y e. ( QQ ^m I ) ) -> ( y e. ( X ( ball ` D ) e ) -> y e. V ) )
41 40 3ad2antl3 
 |-  ( ( ( ph /\ e e. RR+ /\ ( X ( ball ` D ) e ) C_ V ) /\ y e. ( QQ ^m I ) ) -> ( y e. ( X ( ball ` D ) e ) -> y e. V ) )
42 41 reximdva 
 |-  ( ( ph /\ e e. RR+ /\ ( X ( ball ` D ) e ) C_ V ) -> ( E. y e. ( QQ ^m I ) y e. ( X ( ball ` D ) e ) -> E. y e. ( QQ ^m I ) y e. V ) )
43 38 42 mpd 
 |-  ( ( ph /\ e e. RR+ /\ ( X ( ball ` D ) e ) C_ V ) -> E. y e. ( QQ ^m I ) y e. V )
44 43 3exp 
 |-  ( ph -> ( e e. RR+ -> ( ( X ( ball ` D ) e ) C_ V -> E. y e. ( QQ ^m I ) y e. V ) ) )
45 44 rexlimdv 
 |-  ( ph -> ( E. e e. RR+ ( X ( ball ` D ) e ) C_ V -> E. y e. ( QQ ^m I ) y e. V ) )
46 23 45 mpd 
 |-  ( ph -> E. y e. ( QQ ^m I ) y e. V )