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 ) ) |
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 ) ) |