Metamath Proof Explorer

Theorem 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 ⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
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 ⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
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 syl5bir ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ( ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) → ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ ) )
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 ‘ 𝐵 ) )