This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid 
 |-  ( 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 eqtrid 
 |-  ( 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 eqtrid 
 |-  ( 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 ) ) )