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 ⨉_{𝑠} (x \in I ⟼ R)$
	prdsbl.b	$⊢ B = {Base}_{Y}$
	prdsbl.v	$⊢ V = {Base}_{R}$
	prdsbl.e	$⊢ E = {dist (R) ↾}_{(V \times V)}$
	prdsbl.d	$⊢ D = dist (Y)$
	prdsbl.s	$⊢ φ \to S \in W$
	prdsbl.i	$⊢ φ \to I \in Fin$
	prdsbl.r	$⊢ (φ \land x \in I) \to R \in Z$
	prdsbl.m	$⊢ (φ \land x \in I) \to E \in ∞Met (V)$
	prdsbl.p	$⊢ φ \to P \in B$
	prdsbl.a	$⊢ φ \to A \in ℝ^{*}$
	prdsbl.g	$⊢ φ \to 0 < A$
Assertion	prdsbl	$⊢ φ \to P ball (D) A = \underset{x \in I}{⨉} (P (x) ball (E) A)$

Proof

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

Metamath Proof Explorer

Theorem prdsbl

Proof