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 bilani 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) -> f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) )
26 1 ad2antrr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) -> X e. Fin )
27 24 26 sylan2br 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> X e. Fin )
28 simplr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) -> X =/= (/) )
29 24 28 sylan2br 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> X =/= (/) )
30 2 ad2antrr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) -> A : X --> RR )
31 24 30 sylan2br 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> A : X --> RR )
32 3 ad2antrr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) -> B : X --> RR )
33 24 32 sylan2br 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> B : X --> RR )
34 24 bilanri 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )
35 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 ) ) ) )
36 fveq2 
 |-  ( j = i -> ( B ` j ) = ( B ` i ) )
37 fveq2 
 |-  ( j = i -> ( f ` j ) = ( f ` i ) )
38 36 37 oveq12d 
 |-  ( j = i -> ( ( B ` j ) - ( f ` j ) ) = ( ( B ` i ) - ( f ` i ) ) )
39 fveq2 
 |-  ( j = i -> ( A ` j ) = ( A ` i ) )
40 37 39 oveq12d 
 |-  ( j = i -> ( ( f ` j ) - ( A ` j ) ) = ( ( f ` i ) - ( A ` i ) ) )
41 38 40 breq12d 
 |-  ( j = i -> ( ( ( B ` j ) - ( f ` j ) ) <_ ( ( f ` j ) - ( A ` j ) ) <-> ( ( B ` i ) - ( f ` i ) ) <_ ( ( f ` i ) - ( A ` i ) ) ) )
42 41 38 40 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 ) ) ) )
43 42 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 ) ) ) )
44 43 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 ) ) ) )
45 44 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 , < )
46 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 , < ) )
47 fveq1 
 |-  ( a = g -> ( a ` k ) = ( g ` k ) )
48 47 oveq1d 
 |-  ( a = g -> ( ( a ` k ) - ( b ` k ) ) = ( ( g ` k ) - ( b ` k ) ) )
49 48 oveq1d 
 |-  ( a = g -> ( ( ( a ` k ) - ( b ` k ) ) ^ 2 ) = ( ( ( g ` k ) - ( b ` k ) ) ^ 2 ) )
50 49 sumeq2sdv 
 |-  ( a = g -> sum_ k e. X ( ( ( a ` k ) - ( b ` k ) ) ^ 2 ) = sum_ k e. X ( ( ( g ` k ) - ( b ` k ) ) ^ 2 ) )
51 50 fveq2d 
 |-  ( a = g -> ( sqrt ` sum_ k e. X ( ( ( a ` k ) - ( b ` k ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. X ( ( ( g ` k ) - ( b ` k ) ) ^ 2 ) ) )
52 fveq1 
 |-  ( b = h -> ( b ` k ) = ( h ` k ) )
53 52 oveq2d 
 |-  ( b = h -> ( ( g ` k ) - ( b ` k ) ) = ( ( g ` k ) - ( h ` k ) ) )
54 53 oveq1d 
 |-  ( b = h -> ( ( ( g ` k ) - ( b ` k ) ) ^ 2 ) = ( ( ( g ` k ) - ( h ` k ) ) ^ 2 ) )
55 54 sumeq2sdv 
 |-  ( b = h -> sum_ k e. X ( ( ( g ` k ) - ( b ` k ) ) ^ 2 ) = sum_ k e. X ( ( ( g ` k ) - ( h ` k ) ) ^ 2 ) )
56 55 fveq2d 
 |-  ( b = h -> ( sqrt ` sum_ k e. X ( ( ( g ` k ) - ( b ` k ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. X ( ( ( g ` k ) - ( h ` k ) ) ^ 2 ) ) )
57 51 56 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 ) ) )
58 27 29 31 33 34 35 45 46 57 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 ) ) ) )
59 25 58 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 ) ) ) )
60 59 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 ) ) ) )
61 eqid 
 |-  ( TopOpen ` ( RR^ ` X ) ) = ( TopOpen ` ( RR^ ` X ) )
62 61 rrxtop 
 |-  ( X e. Fin -> ( TopOpen ` ( RR^ ` X ) ) e. Top )
63 1 62 syl 
 |-  ( ph -> ( TopOpen ` ( RR^ ` X ) ) e. Top )
64 63 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> ( TopOpen ` ( RR^ ` X ) ) e. Top )
65 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 ) ) ) ) )
66 64 65 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 ) ) ) ) )
67 60 66 mpbird 
 |-  ( ( ph /\ X =/= (/) ) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )
68 19 67 syldan 
 |-  ( ( ph /\ -. X = (/) ) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )
69 17 68 pm2.61dan 
 |-  ( ph -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )