Metamath Proof Explorer

Theorem prdsdsf

Description: The product metric is a function into the nonnegative extended reals. In general this means that it is not a metric but rather an *extended* metric (even when all the factors are metrics), but it will be a metric when restricted to regions where it does not take infinite values. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses prdsdsf.y 
|- Y = ( S Xs_ ( x e. I |-> R ) )
prdsdsf.b 
|- B = ( Base ` Y )
prdsdsf.v 
|- V = ( Base ` R )
prdsdsf.e 
|- E = ( ( dist ` R ) |` ( V X. V ) )
prdsdsf.d 
|- D = ( dist ` Y )
prdsdsf.s 
|- ( ph -> S e. W )
prdsdsf.i 
|- ( ph -> I e. X )
prdsdsf.r 
|- ( ( ph /\ x e. I ) -> R e. Z )
prdsdsf.m 
|- ( ( ph /\ x e. I ) -> E e. ( *Met ` V ) )
Assertion prdsdsf 
|- ( ph -> D : ( B X. B ) --> ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 prdsdsf.y 
 |-  Y = ( S Xs_ ( x e. I |-> R ) )
2 prdsdsf.b 
 |-  B = ( Base ` Y )
3 prdsdsf.v 
 |-  V = ( Base ` R )
4 prdsdsf.e 
 |-  E = ( ( dist ` R ) |` ( V X. V ) )
5 prdsdsf.d 
 |-  D = ( dist ` Y )
6 prdsdsf.s 
 |-  ( ph -> S e. W )
7 prdsdsf.i 
 |-  ( ph -> I e. X )
8 prdsdsf.r 
 |-  ( ( ph /\ x e. I ) -> R e. Z )
9 prdsdsf.m 
 |-  ( ( ph /\ x e. I ) -> E e. ( *Met ` V ) )
10 simpr 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ y e. I ) -> y e. I )
11 8 elexd 
 |-  ( ( ph /\ x e. I ) -> R e. _V )
12 11 ralrimiva 
 |-  ( ph -> A. x e. I R e. _V )
13 12 adantr 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> A. x e. I R e. _V )
14 nfcsb1v 
 |-  F/_ x [_ y / x ]_ R
15 14 nfel1 
 |-  F/ x [_ y / x ]_ R e. _V
16 csbeq1a 
 |-  ( x = y -> R = [_ y / x ]_ R )
17 16 eleq1d 
 |-  ( x = y -> ( R e. _V <-> [_ y / x ]_ R e. _V ) )
18 15 17 rspc 
 |-  ( y e. I -> ( A. x e. I R e. _V -> [_ y / x ]_ R e. _V ) )
19 13 18 mpan9 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ y e. I ) -> [_ y / x ]_ R e. _V )
20 eqid 
 |-  ( x e. I |-> R ) = ( x e. I |-> R )
21 20 fvmpts 
 |-  ( ( y e. I /\ [_ y / x ]_ R e. _V ) -> ( ( x e. I |-> R ) ` y ) = [_ y / x ]_ R )
22 10 19 21 syl2anc 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ y e. I ) -> ( ( x e. I |-> R ) ` y ) = [_ y / x ]_ R )
23 22 fveq2d 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ y e. I ) -> ( dist ` ( ( x e. I |-> R ) ` y ) ) = ( dist ` [_ y / x ]_ R ) )
24 23 oveqd 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ y e. I ) -> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) = ( ( f ` y ) ( dist ` [_ y / x ]_ R ) ( g ` y ) ) )
25 6 adantr 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> S e. W )
26 7 adantr 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> I e. X )
27 simprl 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> f e. B )
28 1 2 25 26 13 3 27 prdsbascl 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> A. x e. I ( f ` x ) e. V )
29 nfcsb1v 
 |-  F/_ x [_ y / x ]_ V
30 29 nfel2 
 |-  F/ x ( f ` y ) e. [_ y / x ]_ V
31 fveq2 
 |-  ( x = y -> ( f ` x ) = ( f ` y ) )
32 csbeq1a 
 |-  ( x = y -> V = [_ y / x ]_ V )
33 31 32 eleq12d 
 |-  ( x = y -> ( ( f ` x ) e. V <-> ( f ` y ) e. [_ y / x ]_ V ) )
34 30 33 rspc 
 |-  ( y e. I -> ( A. x e. I ( f ` x ) e. V -> ( f ` y ) e. [_ y / x ]_ V ) )
35 28 34 mpan9 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ y e. I ) -> ( f ` y ) e. [_ y / x ]_ V )
36 simprr 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> g e. B )
37 1 2 25 26 13 3 36 prdsbascl 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> A. x e. I ( g ` x ) e. V )
38 29 nfel2 
 |-  F/ x ( g ` y ) e. [_ y / x ]_ V
39 fveq2 
 |-  ( x = y -> ( g ` x ) = ( g ` y ) )
40 39 32 eleq12d 
 |-  ( x = y -> ( ( g ` x ) e. V <-> ( g ` y ) e. [_ y / x ]_ V ) )
41 38 40 rspc 
 |-  ( y e. I -> ( A. x e. I ( g ` x ) e. V -> ( g ` y ) e. [_ y / x ]_ V ) )
42 37 41 mpan9 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ y e. I ) -> ( g ` y ) e. [_ y / x ]_ V )
43 35 42 ovresd 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ y e. I ) -> ( ( f ` y ) ( ( dist ` [_ y / x ]_ R ) |` ( [_ y / x ]_ V X. [_ y / x ]_ V ) ) ( g ` y ) ) = ( ( f ` y ) ( dist ` [_ y / x ]_ R ) ( g ` y ) ) )
44 24 43 eqtr4d 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ y e. I ) -> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) = ( ( f ` y ) ( ( dist ` [_ y / x ]_ R ) |` ( [_ y / x ]_ V X. [_ y / x ]_ V ) ) ( g ` y ) ) )
45 9 ralrimiva 
 |-  ( ph -> A. x e. I E e. ( *Met ` V ) )
46 45 adantr 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> A. x e. I E e. ( *Met ` V ) )
47 nfcv 
 |-  F/_ x dist
48 47 14 nffv 
 |-  F/_ x ( dist ` [_ y / x ]_ R )
49 29 29 nfxp 
 |-  F/_ x ( [_ y / x ]_ V X. [_ y / x ]_ V )
50 48 49 nfres 
 |-  F/_ x ( ( dist ` [_ y / x ]_ R ) |` ( [_ y / x ]_ V X. [_ y / x ]_ V ) )
51 nfcv 
 |-  F/_ x *Met
52 51 29 nffv 
 |-  F/_ x ( *Met ` [_ y / x ]_ V )
53 50 52 nfel 
 |-  F/ x ( ( dist ` [_ y / x ]_ R ) |` ( [_ y / x ]_ V X. [_ y / x ]_ V ) ) e. ( *Met ` [_ y / x ]_ V )
54 16 fveq2d 
 |-  ( x = y -> ( dist ` R ) = ( dist ` [_ y / x ]_ R ) )
55 32 sqxpeqd 
 |-  ( x = y -> ( V X. V ) = ( [_ y / x ]_ V X. [_ y / x ]_ V ) )
56 54 55 reseq12d 
 |-  ( x = y -> ( ( dist ` R ) |` ( V X. V ) ) = ( ( dist ` [_ y / x ]_ R ) |` ( [_ y / x ]_ V X. [_ y / x ]_ V ) ) )
57 4 56 syl5eq 
 |-  ( x = y -> E = ( ( dist ` [_ y / x ]_ R ) |` ( [_ y / x ]_ V X. [_ y / x ]_ V ) ) )
58 32 fveq2d 
 |-  ( x = y -> ( *Met ` V ) = ( *Met ` [_ y / x ]_ V ) )
59 57 58 eleq12d 
 |-  ( x = y -> ( E e. ( *Met ` V ) <-> ( ( dist ` [_ y / x ]_ R ) |` ( [_ y / x ]_ V X. [_ y / x ]_ V ) ) e. ( *Met ` [_ y / x ]_ V ) ) )
60 53 59 rspc 
 |-  ( y e. I -> ( A. x e. I E e. ( *Met ` V ) -> ( ( dist ` [_ y / x ]_ R ) |` ( [_ y / x ]_ V X. [_ y / x ]_ V ) ) e. ( *Met ` [_ y / x ]_ V ) ) )
61 46 60 mpan9 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ y e. I ) -> ( ( dist ` [_ y / x ]_ R ) |` ( [_ y / x ]_ V X. [_ y / x ]_ V ) ) e. ( *Met ` [_ y / x ]_ V ) )
62 xmetcl 
 |-  ( ( ( ( dist ` [_ y / x ]_ R ) |` ( [_ y / x ]_ V X. [_ y / x ]_ V ) ) e. ( *Met ` [_ y / x ]_ V ) /\ ( f ` y ) e. [_ y / x ]_ V /\ ( g ` y ) e. [_ y / x ]_ V ) -> ( ( f ` y ) ( ( dist ` [_ y / x ]_ R ) |` ( [_ y / x ]_ V X. [_ y / x ]_ V ) ) ( g ` y ) ) e. RR* )
63 61 35 42 62 syl3anc 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ y e. I ) -> ( ( f ` y ) ( ( dist ` [_ y / x ]_ R ) |` ( [_ y / x ]_ V X. [_ y / x ]_ V ) ) ( g ` y ) ) e. RR* )
64 44 63 eqeltrd 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ y e. I ) -> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) e. RR* )
65 64 fmpttd 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) : I --> RR* )
66 65 frnd 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) C_ RR* )
67 0xr 
 |-  0 e. RR*
68 67 a1i 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> 0 e. RR* )
69 68 snssd 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> { 0 } C_ RR* )
70 66 69 unssd 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) C_ RR* )
71 supxrcl 
 |-  ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) C_ RR* -> sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) e. RR* )
72 70 71 syl 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) e. RR* )
73 ssun2 
 |-  { 0 } C_ ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } )
74 c0ex 
 |-  0 e. _V
75 74 snss 
 |-  ( 0 e. ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) <-> { 0 } C_ ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) )
76 73 75 mpbir 
 |-  0 e. ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } )
77 supxrub 
 |-  ( ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) C_ RR* /\ 0 e. ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) ) -> 0 <_ sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) )
78 70 76 77 sylancl 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> 0 <_ sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) )
79 elxrge0 
 |-  ( sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) e. ( 0 [,] +oo ) <-> ( sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) e. RR* /\ 0 <_ sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) ) )
80 72 78 79 sylanbrc 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) e. ( 0 [,] +oo ) )
81 80 ralrimivva 
 |-  ( ph -> A. f e. B A. g e. B sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) e. ( 0 [,] +oo ) )
82 eqid 
 |-  ( f e. B , g e. B |-> sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) ) = ( f e. B , g e. B |-> sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) )
83 82 fmpo 
 |-  ( A. f e. B A. g e. B sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) e. ( 0 [,] +oo ) <-> ( f e. B , g e. B |-> sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) ) : ( B X. B ) --> ( 0 [,] +oo ) )
84 81 83 sylib 
 |-  ( ph -> ( f e. B , g e. B |-> sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) ) : ( B X. B ) --> ( 0 [,] +oo ) )
85 7 mptexd 
 |-  ( ph -> ( x e. I |-> R ) e. _V )
86 8 ralrimiva 
 |-  ( ph -> A. x e. I R e. Z )
87 dmmptg 
 |-  ( A. x e. I R e. Z -> dom ( x e. I |-> R ) = I )
88 86 87 syl 
 |-  ( ph -> dom ( x e. I |-> R ) = I )
89 1 6 85 2 88 5 prdsds 
 |-  ( ph -> D = ( f e. B , g e. B |-> sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) ) )
90 89 feq1d 
 |-  ( ph -> ( D : ( B X. B ) --> ( 0 [,] +oo ) <-> ( f e. B , g e. B |-> sup ( ( ran ( y e. I |-> ( ( f ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( g ` y ) ) ) u. { 0 } ) , RR* , < ) ) : ( B X. B ) --> ( 0 [,] +oo ) ) )
91 84 90 mpbird 
 |-  ( ph -> D : ( B X. B ) --> ( 0 [,] +oo ) )