prdsmet

Description: The product metric is a metric when the index set is finite. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Hypotheses	prdsmet.y	$⊢ Y = S ⨉_{𝑠} (x \in I ⟼ R)$
	prdsmet.b	$⊢ B = {Base}_{Y}$
	prdsmet.v	$⊢ V = {Base}_{R}$
	prdsmet.e	$⊢ E = {dist (R) ↾}_{(V \times V)}$
	prdsmet.d	$⊢ D = dist (Y)$
	prdsmet.s	$⊢ φ \to S \in W$
	prdsmet.i	$⊢ φ \to I \in Fin$
	prdsmet.r	$⊢ (φ \land x \in I) \to R \in Z$
	prdsmet.m	$⊢ (φ \land x \in I) \to E \in Met (V)$
Assertion	prdsmet	$⊢ φ \to D \in Met (B)$

Proof

Step	Hyp	Ref	Expression
1		prdsmet.y	$⊢ Y = S ⨉_{𝑠} (x \in I ⟼ R)$
2		prdsmet.b	$⊢ B = {Base}_{Y}$
3		prdsmet.v	$⊢ V = {Base}_{R}$
4		prdsmet.e	$⊢ E = {dist (R) ↾}_{(V \times V)}$
5		prdsmet.d	$⊢ D = dist (Y)$
6		prdsmet.s	$⊢ φ \to S \in W$
7		prdsmet.i	$⊢ φ \to I \in Fin$
8		prdsmet.r	$⊢ (φ \land x \in I) \to R \in Z$
9		prdsmet.m	$⊢ (φ \land x \in I) \to E \in Met (V)$
10		metxmet	$⊢ E \in Met (V) \to E \in ∞Met (V)$
11	9 10	syl	$⊢ (φ \land x \in I) \to E \in ∞Met (V)$
12	1 2 3 4 5 6 7 8 11	prdsxmet	$⊢ φ \to D \in ∞Met (B)$
13	1 2 3 4 5 6 7 8 11	prdsdsf	$⊢ φ \to D : B \times B ⟶ [0, +∞]$
14	13	ffnd	$⊢ φ \to D Fn (B \times B)$
15	6	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to S \in W$
16	7	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to I \in Fin$
17	8	ralrimiva	$⊢ φ \to \forall x \in I R \in Z$
18	17	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I R \in Z$
19		simprl	$⊢ (φ \land (f \in B \land g \in B)) \to f \in B$
20		simprr	$⊢ (φ \land (f \in B \land g \in B)) \to g \in B$
21	1 2 15 16 18 19 20 3 4 5	prdsdsval3	$⊢ (φ \land (f \in B \land g \in B)) \to f D g = sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <)$
22	1 2 15 16 18 3 19	prdsbascl	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I f (x) \in V$
23	1 2 15 16 18 3 20	prdsbascl	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I g (x) \in V$
24		r19.26	$⊢ \forall x \in I (f (x) \in V \land g (x) \in V) \leftrightarrow (\forall x \in I f (x) \in V \land \forall x \in I g (x) \in V)$
25		metcl	$⊢ (E \in Met (V) \land f (x) \in V \land g (x) \in V) \to f (x) E g (x) \in ℝ$
26	25	3expib	$⊢ E \in Met (V) \to ((f (x) \in V \land g (x) \in V) \to f (x) E g (x) \in ℝ)$
27	9 26	syl	$⊢ (φ \land x \in I) \to ((f (x) \in V \land g (x) \in V) \to f (x) E g (x) \in ℝ)$
28	27	ralimdva	$⊢ φ \to (\forall x \in I (f (x) \in V \land g (x) \in V) \to \forall x \in I f (x) E g (x) \in ℝ)$
29	28	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to (\forall x \in I (f (x) \in V \land g (x) \in V) \to \forall x \in I f (x) E g (x) \in ℝ)$
30	24 29	syl5bir	$⊢ (φ \land (f \in B \land g \in B)) \to ((\forall x \in I f (x) \in V \land \forall x \in I g (x) \in V) \to \forall x \in I f (x) E g (x) \in ℝ)$
31	22 23 30	mp2and	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I f (x) E g (x) \in ℝ$
32		eqid	$⊢ (x \in I ⟼ f (x) E g (x)) = (x \in I ⟼ f (x) E g (x))$
33	32	fmpt	$⊢ \forall x \in I f (x) E g (x) \in ℝ \leftrightarrow (x \in I ⟼ f (x) E g (x)) : I ⟶ ℝ$
34	31 33	sylib	$⊢ (φ \land (f \in B \land g \in B)) \to (x \in I ⟼ f (x) E g (x)) : I ⟶ ℝ$
35	34	frnd	$⊢ (φ \land (f \in B \land g \in B)) \to ran (x \in I ⟼ f (x) E g (x)) \subseteq ℝ$
36		0red	$⊢ (φ \land (f \in B \land g \in B)) \to 0 \in ℝ$
37	36	snssd	$⊢ (φ \land (f \in B \land g \in B)) \to \{0\} \subseteq ℝ$
38	35 37	unssd	$⊢ (φ \land (f \in B \land g \in B)) \to ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \subseteq ℝ$
39		xrltso	$⊢ < Or ℝ^{*}$
40	39	a1i	$⊢ (φ \land (f \in B \land g \in B)) \to < Or ℝ^{*}$
41		mptfi	$⊢ I \in Fin \to (x \in I ⟼ f (x) E g (x)) \in Fin$
42		rnfi	$⊢ (x \in I ⟼ f (x) E g (x)) \in Fin \to ran (x \in I ⟼ f (x) E g (x)) \in Fin$
43	16 41 42	3syl	$⊢ (φ \land (f \in B \land g \in B)) \to ran (x \in I ⟼ f (x) E g (x)) \in Fin$
44		snfi	$⊢ \{0\} \in Fin$
45		unfi	$⊢ (ran (x \in I ⟼ f (x) E g (x)) \in Fin \land \{0\} \in Fin) \to ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \in Fin$
46	43 44 45	sylancl	$⊢ (φ \land (f \in B \land g \in B)) \to ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \in Fin$
47		ssun2	$⊢ \{0\} \subseteq ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}$
48		c0ex	$⊢ 0 \in V$
49	48	snss	$⊢ 0 \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) \leftrightarrow \{0\} \subseteq ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}$
50	47 49	mpbir	$⊢ 0 \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\})$
51		ne0i	$⊢ 0 \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) \to ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \neq \emptyset$
52	50 51	mp1i	$⊢ (φ \land (f \in B \land g \in B)) \to ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \neq \emptyset$
53		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
54	38 53	sstrdi	$⊢ (φ \land (f \in B \land g \in B)) \to ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \subseteq ℝ^{*}$
55		fisupcl	$⊢ (< Or ℝ^{} \land (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \in Fin \land ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \neq \emptyset \land ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \subseteq ℝ^{})) \to sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <) \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\})$
56	40 46 52 54 55	syl13anc	$⊢ (φ \land (f \in B \land g \in B)) \to sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <) \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\})$
57	38 56	sseldd	$⊢ (φ \land (f \in B \land g \in B)) \to sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <) \in ℝ$
58	21 57	eqeltrd	$⊢ (φ \land (f \in B \land g \in B)) \to f D g \in ℝ$
59	58	ralrimivva	$⊢ φ \to \forall f \in B \forall g \in B f D g \in ℝ$
60		ffnov	$⊢ D : B \times B ⟶ ℝ \leftrightarrow (D Fn (B \times B) \land \forall f \in B \forall g \in B f D g \in ℝ)$
61	14 59 60	sylanbrc	$⊢ φ \to D : B \times B ⟶ ℝ$
62		ismet2	$⊢ D \in Met (B) \leftrightarrow (D \in ∞Met (B) \land D : B \times B ⟶ ℝ)$
63	12 61 62	sylanbrc	$⊢ φ \to D \in Met (B)$

Metamath Proof Explorer

Theorem prdsmet

Proof