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