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 
|- Y = ( S Xs_ ( x e. I |-> R ) )
prdsmet.b 
|- B = ( Base ` Y )
prdsmet.v 
|- V = ( Base ` R )
prdsmet.e 
|- E = ( ( dist ` R ) |` ( V X. V ) )
prdsmet.d 
|- D = ( dist ` Y )
prdsmet.s 
|- ( ph -> S e. W )
prdsmet.i 
|- ( ph -> I e. Fin )
prdsmet.r 
|- ( ( ph /\ x e. I ) -> R e. Z )
prdsmet.m 
|- ( ( ph /\ x e. I ) -> E e. ( Met ` V ) )
Assertion prdsmet 
|- ( ph -> D e. ( Met ` B ) )

Proof

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