Metamath Proof Explorer


Theorem prdsbl

Description: A ball in the product metric for finite index set is the Cartesian product of balls in all coordinates. For infinite index set this is no longer true; instead the correct statement is that a *closed ball* is the product of closed balls in each coordinate (where closed ball means a set of the form in blcld ) - for a counterexample the point p in RR ^ NN whose n -th coordinate is 1 - 1 / n is in X_ n e. NN ball ( 0 , 1 ) but is not in the 1 -ball of the product (since d ( 0 , p ) = 1 ).

The last assumption, 0 < A , is needed only in the case I = (/) , when the right side evaluates to { (/) } and the left evaluates to (/) if A <_ 0 and { (/) } if 0 < A . (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses prdsbl.y
|- Y = ( S Xs_ ( x e. I |-> R ) )
prdsbl.b
|- B = ( Base ` Y )
prdsbl.v
|- V = ( Base ` R )
prdsbl.e
|- E = ( ( dist ` R ) |` ( V X. V ) )
prdsbl.d
|- D = ( dist ` Y )
prdsbl.s
|- ( ph -> S e. W )
prdsbl.i
|- ( ph -> I e. Fin )
prdsbl.r
|- ( ( ph /\ x e. I ) -> R e. Z )
prdsbl.m
|- ( ( ph /\ x e. I ) -> E e. ( *Met ` V ) )
prdsbl.p
|- ( ph -> P e. B )
prdsbl.a
|- ( ph -> A e. RR* )
prdsbl.g
|- ( ph -> 0 < A )
Assertion prdsbl
|- ( ph -> ( P ( ball ` D ) A ) = X_ x e. I ( ( P ` x ) ( ball ` E ) A ) )

Proof

Step Hyp Ref Expression
1 prdsbl.y
 |-  Y = ( S Xs_ ( x e. I |-> R ) )
2 prdsbl.b
 |-  B = ( Base ` Y )
3 prdsbl.v
 |-  V = ( Base ` R )
4 prdsbl.e
 |-  E = ( ( dist ` R ) |` ( V X. V ) )
5 prdsbl.d
 |-  D = ( dist ` Y )
6 prdsbl.s
 |-  ( ph -> S e. W )
7 prdsbl.i
 |-  ( ph -> I e. Fin )
8 prdsbl.r
 |-  ( ( ph /\ x e. I ) -> R e. Z )
9 prdsbl.m
 |-  ( ( ph /\ x e. I ) -> E e. ( *Met ` V ) )
10 prdsbl.p
 |-  ( ph -> P e. B )
11 prdsbl.a
 |-  ( ph -> A e. RR* )
12 prdsbl.g
 |-  ( ph -> 0 < A )
13 8 ralrimiva
 |-  ( ph -> A. x e. I R e. Z )
14 1 2 6 7 13 3 prdsbas3
 |-  ( ph -> B = X_ x e. I V )
15 14 eleq2d
 |-  ( ph -> ( f e. B <-> f e. X_ x e. I V ) )
16 15 biimpa
 |-  ( ( ph /\ f e. B ) -> f e. X_ x e. I V )
17 ixpfn
 |-  ( f e. X_ x e. I V -> f Fn I )
18 vex
 |-  f e. _V
19 18 elixp
 |-  ( f e. X_ x e. I ( ( P ` x ) ( ball ` E ) A ) <-> ( f Fn I /\ A. x e. I ( f ` x ) e. ( ( P ` x ) ( ball ` E ) A ) ) )
20 19 baib
 |-  ( f Fn I -> ( f e. X_ x e. I ( ( P ` x ) ( ball ` E ) A ) <-> A. x e. I ( f ` x ) e. ( ( P ` x ) ( ball ` E ) A ) ) )
21 16 17 20 3syl
 |-  ( ( ph /\ f e. B ) -> ( f e. X_ x e. I ( ( P ` x ) ( ball ` E ) A ) <-> A. x e. I ( f ` x ) e. ( ( P ` x ) ( ball ` E ) A ) ) )
22 9 adantlr
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> E e. ( *Met ` V ) )
23 11 ad2antrr
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> A e. RR* )
24 1 2 6 7 13 3 10 prdsbascl
 |-  ( ph -> A. x e. I ( P ` x ) e. V )
25 24 adantr
 |-  ( ( ph /\ f e. B ) -> A. x e. I ( P ` x ) e. V )
26 25 r19.21bi
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> ( P ` x ) e. V )
27 6 adantr
 |-  ( ( ph /\ f e. B ) -> S e. W )
28 7 adantr
 |-  ( ( ph /\ f e. B ) -> I e. Fin )
29 13 adantr
 |-  ( ( ph /\ f e. B ) -> A. x e. I R e. Z )
30 simpr
 |-  ( ( ph /\ f e. B ) -> f e. B )
31 1 2 27 28 29 3 30 prdsbascl
 |-  ( ( ph /\ f e. B ) -> A. x e. I ( f ` x ) e. V )
32 31 r19.21bi
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> ( f ` x ) e. V )
33 elbl2
 |-  ( ( ( E e. ( *Met ` V ) /\ A e. RR* ) /\ ( ( P ` x ) e. V /\ ( f ` x ) e. V ) ) -> ( ( f ` x ) e. ( ( P ` x ) ( ball ` E ) A ) <-> ( ( P ` x ) E ( f ` x ) ) < A ) )
34 22 23 26 32 33 syl22anc
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> ( ( f ` x ) e. ( ( P ` x ) ( ball ` E ) A ) <-> ( ( P ` x ) E ( f ` x ) ) < A ) )
35 34 ralbidva
 |-  ( ( ph /\ f e. B ) -> ( A. x e. I ( f ` x ) e. ( ( P ` x ) ( ball ` E ) A ) <-> A. x e. I ( ( P ` x ) E ( f ` x ) ) < A ) )
36 xmetcl
 |-  ( ( E e. ( *Met ` V ) /\ ( P ` x ) e. V /\ ( f ` x ) e. V ) -> ( ( P ` x ) E ( f ` x ) ) e. RR* )
37 22 26 32 36 syl3anc
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> ( ( P ` x ) E ( f ` x ) ) e. RR* )
38 37 ralrimiva
 |-  ( ( ph /\ f e. B ) -> A. x e. I ( ( P ` x ) E ( f ` x ) ) e. RR* )
39 eqid
 |-  ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) = ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) )
40 breq1
 |-  ( z = ( ( P ` x ) E ( f ` x ) ) -> ( z < A <-> ( ( P ` x ) E ( f ` x ) ) < A ) )
41 39 40 ralrnmptw
 |-  ( A. x e. I ( ( P ` x ) E ( f ` x ) ) e. RR* -> ( A. z e. ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) z < A <-> A. x e. I ( ( P ` x ) E ( f ` x ) ) < A ) )
42 38 41 syl
 |-  ( ( ph /\ f e. B ) -> ( A. z e. ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) z < A <-> A. x e. I ( ( P ` x ) E ( f ` x ) ) < A ) )
43 12 adantr
 |-  ( ( ph /\ f e. B ) -> 0 < A )
44 c0ex
 |-  0 e. _V
45 breq1
 |-  ( z = 0 -> ( z < A <-> 0 < A ) )
46 44 45 ralsn
 |-  ( A. z e. { 0 } z < A <-> 0 < A )
47 43 46 sylibr
 |-  ( ( ph /\ f e. B ) -> A. z e. { 0 } z < A )
48 ralunb
 |-  ( A. z e. ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) z < A <-> ( A. z e. ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) z < A /\ A. z e. { 0 } z < A ) )
49 10 adantr
 |-  ( ( ph /\ f e. B ) -> P e. B )
50 1 2 27 28 29 49 30 3 4 5 prdsdsval3
 |-  ( ( ph /\ f e. B ) -> ( P D f ) = sup ( ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) , RR* , < ) )
51 xrltso
 |-  < Or RR*
52 51 a1i
 |-  ( ( ph /\ f e. B ) -> < Or RR* )
53 39 rnmpt
 |-  ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) = { y | E. x e. I y = ( ( P ` x ) E ( f ` x ) ) }
54 abrexfi
 |-  ( I e. Fin -> { y | E. x e. I y = ( ( P ` x ) E ( f ` x ) ) } e. Fin )
55 53 54 eqeltrid
 |-  ( I e. Fin -> ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) e. Fin )
56 28 55 syl
 |-  ( ( ph /\ f e. B ) -> ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) e. Fin )
57 snfi
 |-  { 0 } e. Fin
58 unfi
 |-  ( ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) e. Fin /\ { 0 } e. Fin ) -> ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) e. Fin )
59 56 57 58 sylancl
 |-  ( ( ph /\ f e. B ) -> ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) e. Fin )
60 ssun2
 |-  { 0 } C_ ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } )
61 44 snss
 |-  ( 0 e. ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) <-> { 0 } C_ ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) )
62 60 61 mpbir
 |-  0 e. ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } )
63 ne0i
 |-  ( 0 e. ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) -> ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) =/= (/) )
64 62 63 mp1i
 |-  ( ( ph /\ f e. B ) -> ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) =/= (/) )
65 37 fmpttd
 |-  ( ( ph /\ f e. B ) -> ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) : I --> RR* )
66 65 frnd
 |-  ( ( ph /\ f e. B ) -> ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) C_ RR* )
67 0xr
 |-  0 e. RR*
68 67 a1i
 |-  ( ( ph /\ f e. B ) -> 0 e. RR* )
69 68 snssd
 |-  ( ( ph /\ f e. B ) -> { 0 } C_ RR* )
70 66 69 unssd
 |-  ( ( ph /\ f e. B ) -> ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) C_ RR* )
71 fisupcl
 |-  ( ( < Or RR* /\ ( ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) e. Fin /\ ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) =/= (/) /\ ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) C_ RR* ) ) -> sup ( ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) , RR* , < ) e. ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) )
72 52 59 64 70 71 syl13anc
 |-  ( ( ph /\ f e. B ) -> sup ( ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) , RR* , < ) e. ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) )
73 50 72 eqeltrd
 |-  ( ( ph /\ f e. B ) -> ( P D f ) e. ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) )
74 breq1
 |-  ( z = ( P D f ) -> ( z < A <-> ( P D f ) < A ) )
75 74 rspcv
 |-  ( ( P D f ) e. ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) -> ( A. z e. ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) z < A -> ( P D f ) < A ) )
76 73 75 syl
 |-  ( ( ph /\ f e. B ) -> ( A. z e. ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) z < A -> ( P D f ) < A ) )
77 48 76 syl5bir
 |-  ( ( ph /\ f e. B ) -> ( ( A. z e. ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) z < A /\ A. z e. { 0 } z < A ) -> ( P D f ) < A ) )
78 47 77 mpan2d
 |-  ( ( ph /\ f e. B ) -> ( A. z e. ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) z < A -> ( P D f ) < A ) )
79 42 78 sylbird
 |-  ( ( ph /\ f e. B ) -> ( A. x e. I ( ( P ` x ) E ( f ` x ) ) < A -> ( P D f ) < A ) )
80 ssun1
 |-  ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) C_ ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } )
81 ovex
 |-  ( ( P ` x ) E ( f ` x ) ) e. _V
82 81 elabrex
 |-  ( x e. I -> ( ( P ` x ) E ( f ` x ) ) e. { y | E. x e. I y = ( ( P ` x ) E ( f ` x ) ) } )
83 82 adantl
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> ( ( P ` x ) E ( f ` x ) ) e. { y | E. x e. I y = ( ( P ` x ) E ( f ` x ) ) } )
84 83 53 eleqtrrdi
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> ( ( P ` x ) E ( f ` x ) ) e. ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) )
85 80 84 sselid
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> ( ( P ` x ) E ( f ` x ) ) e. ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) )
86 supxrub
 |-  ( ( ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) C_ RR* /\ ( ( P ` x ) E ( f ` x ) ) e. ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) ) -> ( ( P ` x ) E ( f ` x ) ) <_ sup ( ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) , RR* , < ) )
87 70 85 86 syl2an2r
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> ( ( P ` x ) E ( f ` x ) ) <_ sup ( ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) , RR* , < ) )
88 50 adantr
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> ( P D f ) = sup ( ( ran ( x e. I |-> ( ( P ` x ) E ( f ` x ) ) ) u. { 0 } ) , RR* , < ) )
89 87 88 breqtrrd
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> ( ( P ` x ) E ( f ` x ) ) <_ ( P D f ) )
90 1 2 3 4 5 6 7 8 9 prdsxmet
 |-  ( ph -> D e. ( *Met ` B ) )
91 90 ad2antrr
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> D e. ( *Met ` B ) )
92 10 ad2antrr
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> P e. B )
93 30 adantr
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> f e. B )
94 xmetcl
 |-  ( ( D e. ( *Met ` B ) /\ P e. B /\ f e. B ) -> ( P D f ) e. RR* )
95 91 92 93 94 syl3anc
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> ( P D f ) e. RR* )
96 xrlelttr
 |-  ( ( ( ( P ` x ) E ( f ` x ) ) e. RR* /\ ( P D f ) e. RR* /\ A e. RR* ) -> ( ( ( ( P ` x ) E ( f ` x ) ) <_ ( P D f ) /\ ( P D f ) < A ) -> ( ( P ` x ) E ( f ` x ) ) < A ) )
97 37 95 23 96 syl3anc
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> ( ( ( ( P ` x ) E ( f ` x ) ) <_ ( P D f ) /\ ( P D f ) < A ) -> ( ( P ` x ) E ( f ` x ) ) < A ) )
98 89 97 mpand
 |-  ( ( ( ph /\ f e. B ) /\ x e. I ) -> ( ( P D f ) < A -> ( ( P ` x ) E ( f ` x ) ) < A ) )
99 98 ralrimdva
 |-  ( ( ph /\ f e. B ) -> ( ( P D f ) < A -> A. x e. I ( ( P ` x ) E ( f ` x ) ) < A ) )
100 79 99 impbid
 |-  ( ( ph /\ f e. B ) -> ( A. x e. I ( ( P ` x ) E ( f ` x ) ) < A <-> ( P D f ) < A ) )
101 21 35 100 3bitrrd
 |-  ( ( ph /\ f e. B ) -> ( ( P D f ) < A <-> f e. X_ x e. I ( ( P ` x ) ( ball ` E ) A ) ) )
102 101 pm5.32da
 |-  ( ph -> ( ( f e. B /\ ( P D f ) < A ) <-> ( f e. B /\ f e. X_ x e. I ( ( P ` x ) ( ball ` E ) A ) ) ) )
103 elbl
 |-  ( ( D e. ( *Met ` B ) /\ P e. B /\ A e. RR* ) -> ( f e. ( P ( ball ` D ) A ) <-> ( f e. B /\ ( P D f ) < A ) ) )
104 90 10 11 103 syl3anc
 |-  ( ph -> ( f e. ( P ( ball ` D ) A ) <-> ( f e. B /\ ( P D f ) < A ) ) )
105 24 r19.21bi
 |-  ( ( ph /\ x e. I ) -> ( P ` x ) e. V )
106 11 adantr
 |-  ( ( ph /\ x e. I ) -> A e. RR* )
107 blssm
 |-  ( ( E e. ( *Met ` V ) /\ ( P ` x ) e. V /\ A e. RR* ) -> ( ( P ` x ) ( ball ` E ) A ) C_ V )
108 9 105 106 107 syl3anc
 |-  ( ( ph /\ x e. I ) -> ( ( P ` x ) ( ball ` E ) A ) C_ V )
109 108 ralrimiva
 |-  ( ph -> A. x e. I ( ( P ` x ) ( ball ` E ) A ) C_ V )
110 ss2ixp
 |-  ( A. x e. I ( ( P ` x ) ( ball ` E ) A ) C_ V -> X_ x e. I ( ( P ` x ) ( ball ` E ) A ) C_ X_ x e. I V )
111 109 110 syl
 |-  ( ph -> X_ x e. I ( ( P ` x ) ( ball ` E ) A ) C_ X_ x e. I V )
112 111 14 sseqtrrd
 |-  ( ph -> X_ x e. I ( ( P ` x ) ( ball ` E ) A ) C_ B )
113 112 sseld
 |-  ( ph -> ( f e. X_ x e. I ( ( P ` x ) ( ball ` E ) A ) -> f e. B ) )
114 113 pm4.71rd
 |-  ( ph -> ( f e. X_ x e. I ( ( P ` x ) ( ball ` E ) A ) <-> ( f e. B /\ f e. X_ x e. I ( ( P ` x ) ( ball ` E ) A ) ) ) )
115 102 104 114 3bitr4d
 |-  ( ph -> ( f e. ( P ( ball ` D ) A ) <-> f e. X_ x e. I ( ( P ` x ) ( ball ` E ) A ) ) )
116 115 eqrdv
 |-  ( ph -> ( P ( ball ` D ) A ) = X_ x e. I ( ( P ` x ) ( ball ` E ) A ) )