Metamath Proof Explorer

Theorem ioorrnopn

Description: The indexed product of open intervals is an open set in ( RR^X ) . (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses ioorrnopn.x 
|- ( ph -> X e. Fin )
ioorrnopn.a 
|- ( ph -> A : X --> RR )
ioorrnopn.b 
|- ( ph -> B : X --> RR )
Assertion ioorrnopn 
|- ( ph -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )

Proof

Step Hyp Ref Expression
1 ioorrnopn.x 
 |-  ( ph -> X e. Fin )
2 ioorrnopn.a 
 |-  ( ph -> A : X --> RR )
3 ioorrnopn.b 
 |-  ( ph -> B : X --> RR )
4 p0ex 
 |-  { (/) } e. _V
5 4 prid2 
 |-  { (/) } e. { (/) , { (/) } }
6 5 a1i 
 |-  ( X = (/) -> { (/) } e. { (/) , { (/) } } )
7 ixpeq1 
 |-  ( X = (/) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) = X_ i e. (/) ( ( A ` i ) (,) ( B ` i ) ) )
8 ixp0x 
 |-  X_ i e. (/) ( ( A ` i ) (,) ( B ` i ) ) = { (/) }
9 8 a1i 
 |-  ( X = (/) -> X_ i e. (/) ( ( A ` i ) (,) ( B ` i ) ) = { (/) } )
10 7 9 eqtrd 
 |-  ( X = (/) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) = { (/) } )
11 2fveq3 
 |-  ( X = (/) -> ( TopOpen ` ( RR^ ` X ) ) = ( TopOpen ` ( RR^ ` (/) ) ) )
12 rrxtopn0b 
 |-  ( TopOpen ` ( RR^ ` (/) ) ) = { (/) , { (/) } }
13 12 a1i 
 |-  ( X = (/) -> ( TopOpen ` ( RR^ ` (/) ) ) = { (/) , { (/) } } )
14 11 13 eqtrd 
 |-  ( X = (/) -> ( TopOpen ` ( RR^ ` X ) ) = { (/) , { (/) } } )
15 10 14 eleq12d 
 |-  ( X = (/) -> ( X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) <-> { (/) } e. { (/) , { (/) } } ) )
16 6 15 mpbird 
 |-  ( X = (/) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )
17 16 adantl 
 |-  ( ( ph /\ X = (/) ) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )
18 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
19 18 adantl 
 |-  ( ( ph /\ -. X = (/) ) -> X =/= (/) )
20 fveq2 
 |-  ( i = j -> ( A ` i ) = ( A ` j ) )
21 fveq2 
 |-  ( i = j -> ( B ` i ) = ( B ` j ) )
22 20 21 oveq12d 
 |-  ( i = j -> ( ( A ` i ) (,) ( B ` i ) ) = ( ( A ` j ) (,) ( B ` j ) ) )
23 22 cbvixpv 
 |-  X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) = X_ j e. X ( ( A ` j ) (,) ( B ` j ) )
24 23 eleq2i 
 |-  ( f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) <-> f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) )
25 24 biimpi 
 |-  ( f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) -> f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) )
26 25 adantl 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) -> f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) )
27 1 ad2antrr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) -> X e. Fin )
28 24 27 sylan2br 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> X e. Fin )
29 simplr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) -> X =/= (/) )
30 24 29 sylan2br 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> X =/= (/) )
31 2 ad2antrr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) -> A : X --> RR )
32 24 31 sylan2br 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> A : X --> RR )
33 3 ad2antrr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) -> B : X --> RR )
34 24 33 sylan2br 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> B : X --> RR )
35 simpr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) -> f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )
36 24 35 sylan2br 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )
37 eqid 
 |-  ran ( i e. X |-> if ( ( ( B ` i ) - ( f ` i ) ) <_ ( ( f ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( f ` i ) ) , ( ( f ` i ) - ( A ` i ) ) ) ) = ran ( i e. X |-> if ( ( ( B ` i ) - ( f ` i ) ) <_ ( ( f ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( f ` i ) ) , ( ( f ` i ) - ( A ` i ) ) ) )
38 fveq2 
 |-  ( j = i -> ( B ` j ) = ( B ` i ) )
39 fveq2 
 |-  ( j = i -> ( f ` j ) = ( f ` i ) )
40 38 39 oveq12d 
 |-  ( j = i -> ( ( B ` j ) - ( f ` j ) ) = ( ( B ` i ) - ( f ` i ) ) )
41 fveq2 
 |-  ( j = i -> ( A ` j ) = ( A ` i ) )
42 39 41 oveq12d 
 |-  ( j = i -> ( ( f ` j ) - ( A ` j ) ) = ( ( f ` i ) - ( A ` i ) ) )
43 40 42 breq12d 
 |-  ( j = i -> ( ( ( B ` j ) - ( f ` j ) ) <_ ( ( f ` j ) - ( A ` j ) ) <-> ( ( B ` i ) - ( f ` i ) ) <_ ( ( f ` i ) - ( A ` i ) ) ) )
44 43 40 42 ifbieq12d 
 |-  ( j = i -> if ( ( ( B ` j ) - ( f ` j ) ) <_ ( ( f ` j ) - ( A ` j ) ) , ( ( B ` j ) - ( f ` j ) ) , ( ( f ` j ) - ( A ` j ) ) ) = if ( ( ( B ` i ) - ( f ` i ) ) <_ ( ( f ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( f ` i ) ) , ( ( f ` i ) - ( A ` i ) ) ) )
45 44 cbvmptv 
 |-  ( j e. X |-> if ( ( ( B ` j ) - ( f ` j ) ) <_ ( ( f ` j ) - ( A ` j ) ) , ( ( B ` j ) - ( f ` j ) ) , ( ( f ` j ) - ( A ` j ) ) ) ) = ( i e. X |-> if ( ( ( B ` i ) - ( f ` i ) ) <_ ( ( f ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( f ` i ) ) , ( ( f ` i ) - ( A ` i ) ) ) )
46 45 rneqi 
 |-  ran ( j e. X |-> if ( ( ( B ` j ) - ( f ` j ) ) <_ ( ( f ` j ) - ( A ` j ) ) , ( ( B ` j ) - ( f ` j ) ) , ( ( f ` j ) - ( A ` j ) ) ) ) = ran ( i e. X |-> if ( ( ( B ` i ) - ( f ` i ) ) <_ ( ( f ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( f ` i ) ) , ( ( f ` i ) - ( A ` i ) ) ) )
47 46 infeq1i 
 |-  inf ( ran ( j e. X |-> if ( ( ( B ` j ) - ( f ` j ) ) <_ ( ( f ` j ) - ( A ` j ) ) , ( ( B ` j ) - ( f ` j ) ) , ( ( f ` j ) - ( A ` j ) ) ) ) , RR , < ) = inf ( ran ( i e. X |-> if ( ( ( B ` i ) - ( f ` i ) ) <_ ( ( f ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( f ` i ) ) , ( ( f ` i ) - ( A ` i ) ) ) ) , RR , < )
48 eqid 
 |-  ( f ( ball ` ( a e. ( RR ^m X ) , b e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( a ` k ) - ( b ` k ) ) ^ 2 ) ) ) ) inf ( ran ( j e. X |-> if ( ( ( B ` j ) - ( f ` j ) ) <_ ( ( f ` j ) - ( A ` j ) ) , ( ( B ` j ) - ( f ` j ) ) , ( ( f ` j ) - ( A ` j ) ) ) ) , RR , < ) ) = ( f ( ball ` ( a e. ( RR ^m X ) , b e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( a ` k ) - ( b ` k ) ) ^ 2 ) ) ) ) inf ( ran ( j e. X |-> if ( ( ( B ` j ) - ( f ` j ) ) <_ ( ( f ` j ) - ( A ` j ) ) , ( ( B ` j ) - ( f ` j ) ) , ( ( f ` j ) - ( A ` j ) ) ) ) , RR , < ) )
49 fveq1 
 |-  ( a = g -> ( a ` k ) = ( g ` k ) )
50 49 oveq1d 
 |-  ( a = g -> ( ( a ` k ) - ( b ` k ) ) = ( ( g ` k ) - ( b ` k ) ) )
51 50 oveq1d 
 |-  ( a = g -> ( ( ( a ` k ) - ( b ` k ) ) ^ 2 ) = ( ( ( g ` k ) - ( b ` k ) ) ^ 2 ) )
52 51 sumeq2sdv 
 |-  ( a = g -> sum_ k e. X ( ( ( a ` k ) - ( b ` k ) ) ^ 2 ) = sum_ k e. X ( ( ( g ` k ) - ( b ` k ) ) ^ 2 ) )
53 52 fveq2d 
 |-  ( a = g -> ( sqrt ` sum_ k e. X ( ( ( a ` k ) - ( b ` k ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. X ( ( ( g ` k ) - ( b ` k ) ) ^ 2 ) ) )
54 fveq1 
 |-  ( b = h -> ( b ` k ) = ( h ` k ) )
55 54 oveq2d 
 |-  ( b = h -> ( ( g ` k ) - ( b ` k ) ) = ( ( g ` k ) - ( h ` k ) ) )
56 55 oveq1d 
 |-  ( b = h -> ( ( ( g ` k ) - ( b ` k ) ) ^ 2 ) = ( ( ( g ` k ) - ( h ` k ) ) ^ 2 ) )
57 56 sumeq2sdv 
 |-  ( b = h -> sum_ k e. X ( ( ( g ` k ) - ( b ` k ) ) ^ 2 ) = sum_ k e. X ( ( ( g ` k ) - ( h ` k ) ) ^ 2 ) )
58 57 fveq2d 
 |-  ( b = h -> ( sqrt ` sum_ k e. X ( ( ( g ` k ) - ( b ` k ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. X ( ( ( g ` k ) - ( h ` k ) ) ^ 2 ) ) )
59 53 58 cbvmpov 
 |-  ( a e. ( RR ^m X ) , b e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( a ` k ) - ( b ` k ) ) ^ 2 ) ) ) = ( g e. ( RR ^m X ) , h e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( g ` k ) - ( h ` k ) ) ^ 2 ) ) )
60 28 30 32 34 36 37 47 48 59 ioorrnopnlem 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> E. v e. ( TopOpen ` ( RR^ ` X ) ) ( f e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) )
61 26 60 syldan 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) -> E. v e. ( TopOpen ` ( RR^ ` X ) ) ( f e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) )
62 61 ralrimiva 
 |-  ( ( ph /\ X =/= (/) ) -> A. f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) E. v e. ( TopOpen ` ( RR^ ` X ) ) ( f e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) )
63 eqid 
 |-  ( TopOpen ` ( RR^ ` X ) ) = ( TopOpen ` ( RR^ ` X ) )
64 63 rrxtop 
 |-  ( X e. Fin -> ( TopOpen ` ( RR^ ` X ) ) e. Top )
65 1 64 syl 
 |-  ( ph -> ( TopOpen ` ( RR^ ` X ) ) e. Top )
66 65 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> ( TopOpen ` ( RR^ ` X ) ) e. Top )
67 eltop2 
 |-  ( ( TopOpen ` ( RR^ ` X ) ) e. Top -> ( X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) <-> A. f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) E. v e. ( TopOpen ` ( RR^ ` X ) ) ( f e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) ) )
68 66 67 syl 
 |-  ( ( ph /\ X =/= (/) ) -> ( X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) <-> A. f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) E. v e. ( TopOpen ` ( RR^ ` X ) ) ( f e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) ) )
69 62 68 mpbird 
 |-  ( ( ph /\ X =/= (/) ) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )
70 19 69 syldan 
 |-  ( ( ph /\ -. X = (/) ) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )
71 17 70 pm2.61dan 
 |-  ( ph -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )