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	⊢ 𝑌 = ( 𝑆 X_s ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
	prdsmet.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	prdsmet.v	⊢ 𝑉 = ( Base ‘ 𝑅 )
	prdsmet.e	⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
	prdsmet.d	⊢ 𝐷 = ( dist ‘ 𝑌 )
	prdsmet.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
	prdsmet.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	prdsmet.r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ 𝑍 )
	prdsmet.m	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( Met ‘ 𝑉 ) )
Assertion	prdsmet	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		prdsmet.y	⊢ 𝑌 = ( 𝑆 X_s ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
2		prdsmet.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		prdsmet.v	⊢ 𝑉 = ( Base ‘ 𝑅 )
4		prdsmet.e	⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
5		prdsmet.d	⊢ 𝐷 = ( dist ‘ 𝑌 )
6		prdsmet.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
7		prdsmet.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
8		prdsmet.r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ 𝑍 )
9		prdsmet.m	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( Met ‘ 𝑉 ) )
10		metxmet	⊢ ( 𝐸 ∈ ( Met ‘ 𝑉 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
11	9 10	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
12	1 2 3 4 5 6 7 8 11	prdsxmet	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )
13	1 2 3 4 5 6 7 8 11	prdsdsf	⊢ ( 𝜑 → 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ( 0 [,] +∞ ) )
14	13	ffnd	⊢ ( 𝜑 → 𝐷 Fn ( 𝐵 × 𝐵 ) )
15	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑆 ∈ 𝑊 )
16	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝐼 ∈ Fin )
17	8	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑍 )
18	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑍 )
19		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 ∈ 𝐵 )
20		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 ∈ 𝐵 )
21	1 2 15 16 18 19 20 3 4 5	prdsdsval3	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 𝐷 𝑔 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) )
22	1 2 15 16 18 3 19	prdsbascl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 )
23	1 2 15 16 18 3 20	prdsbascl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 )
24		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) ↔ ( ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) )
25		metcl	⊢ ( ( 𝐸 ∈ ( Met ‘ 𝑉 ) ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) → ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ )
26	25	3expib	⊢ ( 𝐸 ∈ ( Met ‘ 𝑉 ) → ( ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) → ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ ) )
27	9 26	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) → ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ ) )
28	27	ralimdva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) → ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ ) )
29	28	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) → ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ ) )
30	24 29	biimtrrid	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ( ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) → ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ ) )
31	22 23 30	mp2and	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ )
32		eqid	⊢ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) )
33	32	fmpt	⊢ ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ ↔ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) : 𝐼 ⟶ ℝ )
34	31 33	sylib	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) : 𝐼 ⟶ ℝ )
35	34	frnd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ⊆ ℝ )
36		0red	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 0 ∈ ℝ )
37	36	snssd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → { 0 } ⊆ ℝ )
38	35 37	unssd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ⊆ ℝ )
39		xrltso	⊢ < Or ℝ^*
40	39	a1i	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → < Or ℝ^* )
41		mptfi	⊢ ( 𝐼 ∈ Fin → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∈ Fin )
42		rnfi	⊢ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∈ Fin → ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∈ Fin )
43	16 41 42	3syl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∈ Fin )
44		snfi	⊢ { 0 } ∈ Fin
45		unfi	⊢ ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∈ Fin ∧ { 0 } ∈ Fin ) → ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ∈ Fin )
46	43 44 45	sylancl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ∈ Fin )
47		ssun2	⊢ { 0 } ⊆ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } )
48		c0ex	⊢ 0 ∈ V
49	48	snss	⊢ ( 0 ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ↔ { 0 } ⊆ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) )
50	47 49	mpbir	⊢ 0 ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } )
51		ne0i	⊢ ( 0 ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) → ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ≠ ∅ )
52	50 51	mp1i	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ≠ ∅ )
53		ressxr	⊢ ℝ ⊆ ℝ^*
54	38 53	sstrdi	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ⊆ ℝ^* )
55		fisupcl	⊢ ( ( < Or ℝ^* ∧ ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ∈ Fin ∧ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ≠ ∅ ∧ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ⊆ ℝ^* ) ) → sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) )
56	40 46 52 54 55	syl13anc	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) )
57	38 56	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ∈ ℝ )
58	21 57	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 𝐷 𝑔 ) ∈ ℝ )
59	58	ralrimivva	⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ( 𝑓 𝐷 𝑔 ) ∈ ℝ )
60		ffnov	⊢ ( 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ℝ ↔ ( 𝐷 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ( 𝑓 𝐷 𝑔 ) ∈ ℝ ) )
61	14 59 60	sylanbrc	⊢ ( 𝜑 → 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ℝ )
62		ismet2	⊢ ( 𝐷 ∈ ( Met ‘ 𝐵 ) ↔ ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ℝ ) )
63	12 61 62	sylanbrc	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝐵 ) )

Metamath Proof Explorer

Theorem prdsmet

Proof