Metamath Proof Explorer


Theorem ressprdsds

Description: Restriction of a product metric. (Contributed by Mario Carneiro, 16-Sep-2015)

Ref Expression
Hypotheses ressprdsds.y
|- ( ph -> Y = ( S Xs_ ( x e. I |-> R ) ) )
ressprdsds.h
|- ( ph -> H = ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) )
ressprdsds.b
|- B = ( Base ` H )
ressprdsds.d
|- D = ( dist ` Y )
ressprdsds.e
|- E = ( dist ` H )
ressprdsds.s
|- ( ph -> S e. U )
ressprdsds.t
|- ( ph -> T e. V )
ressprdsds.i
|- ( ph -> I e. W )
ressprdsds.r
|- ( ( ph /\ x e. I ) -> R e. X )
ressprdsds.a
|- ( ( ph /\ x e. I ) -> A e. Z )
Assertion ressprdsds
|- ( ph -> E = ( D |` ( B X. B ) ) )

Proof

Step Hyp Ref Expression
1 ressprdsds.y
 |-  ( ph -> Y = ( S Xs_ ( x e. I |-> R ) ) )
2 ressprdsds.h
 |-  ( ph -> H = ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) )
3 ressprdsds.b
 |-  B = ( Base ` H )
4 ressprdsds.d
 |-  D = ( dist ` Y )
5 ressprdsds.e
 |-  E = ( dist ` H )
6 ressprdsds.s
 |-  ( ph -> S e. U )
7 ressprdsds.t
 |-  ( ph -> T e. V )
8 ressprdsds.i
 |-  ( ph -> I e. W )
9 ressprdsds.r
 |-  ( ( ph /\ x e. I ) -> R e. X )
10 ressprdsds.a
 |-  ( ( ph /\ x e. I ) -> A e. Z )
11 ovres
 |-  ( ( f e. B /\ g e. B ) -> ( f ( D |` ( B X. B ) ) g ) = ( f D g ) )
12 11 adantl
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( f ( D |` ( B X. B ) ) g ) = ( f D g ) )
13 eqid
 |-  ( R |`s A ) = ( R |`s A )
14 eqid
 |-  ( dist ` R ) = ( dist ` R )
15 13 14 ressds
 |-  ( A e. Z -> ( dist ` R ) = ( dist ` ( R |`s A ) ) )
16 10 15 syl
 |-  ( ( ph /\ x e. I ) -> ( dist ` R ) = ( dist ` ( R |`s A ) ) )
17 16 oveqd
 |-  ( ( ph /\ x e. I ) -> ( ( f ` x ) ( dist ` R ) ( g ` x ) ) = ( ( f ` x ) ( dist ` ( R |`s A ) ) ( g ` x ) ) )
18 17 mpteq2dva
 |-  ( ph -> ( x e. I |-> ( ( f ` x ) ( dist ` R ) ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) ( dist ` ( R |`s A ) ) ( g ` x ) ) ) )
19 18 adantr
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( x e. I |-> ( ( f ` x ) ( dist ` R ) ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) ( dist ` ( R |`s A ) ) ( g ` x ) ) ) )
20 19 rneqd
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ran ( x e. I |-> ( ( f ` x ) ( dist ` R ) ( g ` x ) ) ) = ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R |`s A ) ) ( g ` x ) ) ) )
21 20 uneq1d
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( ran ( x e. I |-> ( ( f ` x ) ( dist ` R ) ( g ` x ) ) ) u. { 0 } ) = ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R |`s A ) ) ( g ` x ) ) ) u. { 0 } ) )
22 21 supeq1d
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` R ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) = sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R |`s A ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) )
23 eqid
 |-  ( S Xs_ ( x e. I |-> R ) ) = ( S Xs_ ( x e. I |-> R ) )
24 eqid
 |-  ( Base ` ( S Xs_ ( x e. I |-> R ) ) ) = ( Base ` ( S Xs_ ( x e. I |-> R ) ) )
25 6 adantr
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> S e. U )
26 8 adantr
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> I e. W )
27 9 ralrimiva
 |-  ( ph -> A. x e. I R e. X )
28 27 adantr
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> A. x e. I R e. X )
29 eqid
 |-  ( Base ` R ) = ( Base ` R )
30 13 29 ressbasss
 |-  ( Base ` ( R |`s A ) ) C_ ( Base ` R )
31 30 a1i
 |-  ( ( ph /\ x e. I ) -> ( Base ` ( R |`s A ) ) C_ ( Base ` R ) )
32 31 ralrimiva
 |-  ( ph -> A. x e. I ( Base ` ( R |`s A ) ) C_ ( Base ` R ) )
33 ss2ixp
 |-  ( A. x e. I ( Base ` ( R |`s A ) ) C_ ( Base ` R ) -> X_ x e. I ( Base ` ( R |`s A ) ) C_ X_ x e. I ( Base ` R ) )
34 32 33 syl
 |-  ( ph -> X_ x e. I ( Base ` ( R |`s A ) ) C_ X_ x e. I ( Base ` R ) )
35 eqid
 |-  ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) = ( T Xs_ ( x e. I |-> ( R |`s A ) ) )
36 eqid
 |-  ( Base ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) = ( Base ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) )
37 ovex
 |-  ( R |`s A ) e. _V
38 37 rgenw
 |-  A. x e. I ( R |`s A ) e. _V
39 38 a1i
 |-  ( ph -> A. x e. I ( R |`s A ) e. _V )
40 eqid
 |-  ( Base ` ( R |`s A ) ) = ( Base ` ( R |`s A ) )
41 35 36 7 8 39 40 prdsbas3
 |-  ( ph -> ( Base ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) = X_ x e. I ( Base ` ( R |`s A ) ) )
42 23 24 6 8 27 29 prdsbas3
 |-  ( ph -> ( Base ` ( S Xs_ ( x e. I |-> R ) ) ) = X_ x e. I ( Base ` R ) )
43 34 41 42 3sstr4d
 |-  ( ph -> ( Base ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) C_ ( Base ` ( S Xs_ ( x e. I |-> R ) ) ) )
44 2 fveq2d
 |-  ( ph -> ( Base ` H ) = ( Base ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) )
45 3 44 syl5eq
 |-  ( ph -> B = ( Base ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) )
46 1 fveq2d
 |-  ( ph -> ( Base ` Y ) = ( Base ` ( S Xs_ ( x e. I |-> R ) ) ) )
47 43 45 46 3sstr4d
 |-  ( ph -> B C_ ( Base ` Y ) )
48 47 adantr
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> B C_ ( Base ` Y ) )
49 46 adantr
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( Base ` Y ) = ( Base ` ( S Xs_ ( x e. I |-> R ) ) ) )
50 48 49 sseqtrd
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> B C_ ( Base ` ( S Xs_ ( x e. I |-> R ) ) ) )
51 simprl
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> f e. B )
52 50 51 sseldd
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> f e. ( Base ` ( S Xs_ ( x e. I |-> R ) ) ) )
53 simprr
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> g e. B )
54 50 53 sseldd
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> g e. ( Base ` ( S Xs_ ( x e. I |-> R ) ) ) )
55 eqid
 |-  ( dist ` ( S Xs_ ( x e. I |-> R ) ) ) = ( dist ` ( S Xs_ ( x e. I |-> R ) ) )
56 23 24 25 26 28 52 54 14 55 prdsdsval2
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( f ( dist ` ( S Xs_ ( x e. I |-> R ) ) ) g ) = sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` R ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) )
57 7 adantr
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> T e. V )
58 38 a1i
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> A. x e. I ( R |`s A ) e. _V )
59 45 adantr
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> B = ( Base ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) )
60 51 59 eleqtrd
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> f e. ( Base ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) )
61 53 59 eleqtrd
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> g e. ( Base ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) )
62 eqid
 |-  ( dist ` ( R |`s A ) ) = ( dist ` ( R |`s A ) )
63 eqid
 |-  ( dist ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) = ( dist ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) )
64 35 36 57 26 58 60 61 62 63 prdsdsval2
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( f ( dist ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) g ) = sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R |`s A ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) )
65 22 56 64 3eqtr4d
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( f ( dist ` ( S Xs_ ( x e. I |-> R ) ) ) g ) = ( f ( dist ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) g ) )
66 1 fveq2d
 |-  ( ph -> ( dist ` Y ) = ( dist ` ( S Xs_ ( x e. I |-> R ) ) ) )
67 4 66 syl5eq
 |-  ( ph -> D = ( dist ` ( S Xs_ ( x e. I |-> R ) ) ) )
68 67 oveqdr
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( f D g ) = ( f ( dist ` ( S Xs_ ( x e. I |-> R ) ) ) g ) )
69 2 fveq2d
 |-  ( ph -> ( dist ` H ) = ( dist ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) )
70 5 69 syl5eq
 |-  ( ph -> E = ( dist ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) )
71 70 oveqdr
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( f E g ) = ( f ( dist ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) g ) )
72 65 68 71 3eqtr4d
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( f D g ) = ( f E g ) )
73 12 72 eqtr2d
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( f E g ) = ( f ( D |` ( B X. B ) ) g ) )
74 73 ralrimivva
 |-  ( ph -> A. f e. B A. g e. B ( f E g ) = ( f ( D |` ( B X. B ) ) g ) )
75 8 mptexd
 |-  ( ph -> ( x e. I |-> ( R |`s A ) ) e. _V )
76 eqid
 |-  ( x e. I |-> ( R |`s A ) ) = ( x e. I |-> ( R |`s A ) )
77 37 76 dmmpti
 |-  dom ( x e. I |-> ( R |`s A ) ) = I
78 77 a1i
 |-  ( ph -> dom ( x e. I |-> ( R |`s A ) ) = I )
79 35 7 75 36 78 63 prdsdsfn
 |-  ( ph -> ( dist ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) Fn ( ( Base ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) X. ( Base ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) ) )
80 45 sqxpeqd
 |-  ( ph -> ( B X. B ) = ( ( Base ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) X. ( Base ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) ) )
81 70 80 fneq12d
 |-  ( ph -> ( E Fn ( B X. B ) <-> ( dist ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) Fn ( ( Base ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) X. ( Base ` ( T Xs_ ( x e. I |-> ( R |`s A ) ) ) ) ) ) )
82 79 81 mpbird
 |-  ( ph -> E Fn ( B X. B ) )
83 8 mptexd
 |-  ( ph -> ( x e. I |-> R ) e. _V )
84 dmmptg
 |-  ( A. x e. I R e. X -> dom ( x e. I |-> R ) = I )
85 27 84 syl
 |-  ( ph -> dom ( x e. I |-> R ) = I )
86 23 6 83 24 85 55 prdsdsfn
 |-  ( ph -> ( dist ` ( S Xs_ ( x e. I |-> R ) ) ) Fn ( ( Base ` ( S Xs_ ( x e. I |-> R ) ) ) X. ( Base ` ( S Xs_ ( x e. I |-> R ) ) ) ) )
87 46 sqxpeqd
 |-  ( ph -> ( ( Base ` Y ) X. ( Base ` Y ) ) = ( ( Base ` ( S Xs_ ( x e. I |-> R ) ) ) X. ( Base ` ( S Xs_ ( x e. I |-> R ) ) ) ) )
88 67 87 fneq12d
 |-  ( ph -> ( D Fn ( ( Base ` Y ) X. ( Base ` Y ) ) <-> ( dist ` ( S Xs_ ( x e. I |-> R ) ) ) Fn ( ( Base ` ( S Xs_ ( x e. I |-> R ) ) ) X. ( Base ` ( S Xs_ ( x e. I |-> R ) ) ) ) ) )
89 86 88 mpbird
 |-  ( ph -> D Fn ( ( Base ` Y ) X. ( Base ` Y ) ) )
90 xpss12
 |-  ( ( B C_ ( Base ` Y ) /\ B C_ ( Base ` Y ) ) -> ( B X. B ) C_ ( ( Base ` Y ) X. ( Base ` Y ) ) )
91 47 47 90 syl2anc
 |-  ( ph -> ( B X. B ) C_ ( ( Base ` Y ) X. ( Base ` Y ) ) )
92 fnssres
 |-  ( ( D Fn ( ( Base ` Y ) X. ( Base ` Y ) ) /\ ( B X. B ) C_ ( ( Base ` Y ) X. ( Base ` Y ) ) ) -> ( D |` ( B X. B ) ) Fn ( B X. B ) )
93 89 91 92 syl2anc
 |-  ( ph -> ( D |` ( B X. B ) ) Fn ( B X. B ) )
94 eqfnov2
 |-  ( ( E Fn ( B X. B ) /\ ( D |` ( B X. B ) ) Fn ( B X. B ) ) -> ( E = ( D |` ( B X. B ) ) <-> A. f e. B A. g e. B ( f E g ) = ( f ( D |` ( B X. B ) ) g ) ) )
95 82 93 94 syl2anc
 |-  ( ph -> ( E = ( D |` ( B X. B ) ) <-> A. f e. B A. g e. B ( f E g ) = ( f ( D |` ( B X. B ) ) g ) ) )
96 74 95 mpbird
 |-  ( ph -> E = ( D |` ( B X. B ) ) )