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 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 β€˜ 𝐡 ) )