Metamath Proof Explorer

Theorem tmsxpsval

Description: Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tmsxps.p 
|- P = ( dist ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) )
tmsxps.1 
|- ( ph -> M e. ( *Met ` X ) )
tmsxps.2 
|- ( ph -> N e. ( *Met ` Y ) )
tmsxpsval.a 
|- ( ph -> A e. X )
tmsxpsval.b 
|- ( ph -> B e. Y )
tmsxpsval.c 
|- ( ph -> C e. X )
tmsxpsval.d 
|- ( ph -> D e. Y )
Assertion tmsxpsval 
|- ( ph -> ( <. A , B >. P <. C , D >. ) = sup ( { ( A M C ) , ( B N D ) } , RR* , < ) )

Proof

Step Hyp Ref Expression
1 tmsxps.p 
 |-  P = ( dist ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) )
2 tmsxps.1 
 |-  ( ph -> M e. ( *Met ` X ) )
3 tmsxps.2 
 |-  ( ph -> N e. ( *Met ` Y ) )
4 tmsxpsval.a 
 |-  ( ph -> A e. X )
5 tmsxpsval.b 
 |-  ( ph -> B e. Y )
6 tmsxpsval.c 
 |-  ( ph -> C e. X )
7 tmsxpsval.d 
 |-  ( ph -> D e. Y )
8 eqid 
 |-  ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) = ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) )
9 eqid 
 |-  ( Base ` ( toMetSp ` M ) ) = ( Base ` ( toMetSp ` M ) )
10 eqid 
 |-  ( Base ` ( toMetSp ` N ) ) = ( Base ` ( toMetSp ` N ) )
11 eqid 
 |-  ( toMetSp ` M ) = ( toMetSp ` M )
12 11 tmsxms 
 |-  ( M e. ( *Met ` X ) -> ( toMetSp ` M ) e. *MetSp )
13 2 12 syl 
 |-  ( ph -> ( toMetSp ` M ) e. *MetSp )
14 eqid 
 |-  ( toMetSp ` N ) = ( toMetSp ` N )
15 14 tmsxms 
 |-  ( N e. ( *Met ` Y ) -> ( toMetSp ` N ) e. *MetSp )
16 3 15 syl 
 |-  ( ph -> ( toMetSp ` N ) e. *MetSp )
17 eqid 
 |-  ( ( dist ` ( toMetSp ` M ) ) |` ( ( Base ` ( toMetSp ` M ) ) X. ( Base ` ( toMetSp ` M ) ) ) ) = ( ( dist ` ( toMetSp ` M ) ) |` ( ( Base ` ( toMetSp ` M ) ) X. ( Base ` ( toMetSp ` M ) ) ) )
18 eqid 
 |-  ( ( dist ` ( toMetSp ` N ) ) |` ( ( Base ` ( toMetSp ` N ) ) X. ( Base ` ( toMetSp ` N ) ) ) ) = ( ( dist ` ( toMetSp ` N ) ) |` ( ( Base ` ( toMetSp ` N ) ) X. ( Base ` ( toMetSp ` N ) ) ) )
19 11 tmsds 
 |-  ( M e. ( *Met ` X ) -> M = ( dist ` ( toMetSp ` M ) ) )
20 2 19 syl 
 |-  ( ph -> M = ( dist ` ( toMetSp ` M ) ) )
21 11 tmsbas 
 |-  ( M e. ( *Met ` X ) -> X = ( Base ` ( toMetSp ` M ) ) )
22 2 21 syl 
 |-  ( ph -> X = ( Base ` ( toMetSp ` M ) ) )
23 22 fveq2d 
 |-  ( ph -> ( *Met ` X ) = ( *Met ` ( Base ` ( toMetSp ` M ) ) ) )
24 2 20 23 3eltr3d 
 |-  ( ph -> ( dist ` ( toMetSp ` M ) ) e. ( *Met ` ( Base ` ( toMetSp ` M ) ) ) )
25 ssid 
 |-  ( Base ` ( toMetSp ` M ) ) C_ ( Base ` ( toMetSp ` M ) )
26 xmetres2 
 |-  ( ( ( dist ` ( toMetSp ` M ) ) e. ( *Met ` ( Base ` ( toMetSp ` M ) ) ) /\ ( Base ` ( toMetSp ` M ) ) C_ ( Base ` ( toMetSp ` M ) ) ) -> ( ( dist ` ( toMetSp ` M ) ) |` ( ( Base ` ( toMetSp ` M ) ) X. ( Base ` ( toMetSp ` M ) ) ) ) e. ( *Met ` ( Base ` ( toMetSp ` M ) ) ) )
27 24 25 26 sylancl 
 |-  ( ph -> ( ( dist ` ( toMetSp ` M ) ) |` ( ( Base ` ( toMetSp ` M ) ) X. ( Base ` ( toMetSp ` M ) ) ) ) e. ( *Met ` ( Base ` ( toMetSp ` M ) ) ) )
28 14 tmsds 
 |-  ( N e. ( *Met ` Y ) -> N = ( dist ` ( toMetSp ` N ) ) )
29 3 28 syl 
 |-  ( ph -> N = ( dist ` ( toMetSp ` N ) ) )
30 14 tmsbas 
 |-  ( N e. ( *Met ` Y ) -> Y = ( Base ` ( toMetSp ` N ) ) )
31 3 30 syl 
 |-  ( ph -> Y = ( Base ` ( toMetSp ` N ) ) )
32 31 fveq2d 
 |-  ( ph -> ( *Met ` Y ) = ( *Met ` ( Base ` ( toMetSp ` N ) ) ) )
33 3 29 32 3eltr3d 
 |-  ( ph -> ( dist ` ( toMetSp ` N ) ) e. ( *Met ` ( Base ` ( toMetSp ` N ) ) ) )
34 ssid 
 |-  ( Base ` ( toMetSp ` N ) ) C_ ( Base ` ( toMetSp ` N ) )
35 xmetres2 
 |-  ( ( ( dist ` ( toMetSp ` N ) ) e. ( *Met ` ( Base ` ( toMetSp ` N ) ) ) /\ ( Base ` ( toMetSp ` N ) ) C_ ( Base ` ( toMetSp ` N ) ) ) -> ( ( dist ` ( toMetSp ` N ) ) |` ( ( Base ` ( toMetSp ` N ) ) X. ( Base ` ( toMetSp ` N ) ) ) ) e. ( *Met ` ( Base ` ( toMetSp ` N ) ) ) )
36 33 34 35 sylancl 
 |-  ( ph -> ( ( dist ` ( toMetSp ` N ) ) |` ( ( Base ` ( toMetSp ` N ) ) X. ( Base ` ( toMetSp ` N ) ) ) ) e. ( *Met ` ( Base ` ( toMetSp ` N ) ) ) )
37 4 22 eleqtrd 
 |-  ( ph -> A e. ( Base ` ( toMetSp ` M ) ) )
38 5 31 eleqtrd 
 |-  ( ph -> B e. ( Base ` ( toMetSp ` N ) ) )
39 6 22 eleqtrd 
 |-  ( ph -> C e. ( Base ` ( toMetSp ` M ) ) )
40 7 31 eleqtrd 
 |-  ( ph -> D e. ( Base ` ( toMetSp ` N ) ) )
41 8 9 10 13 16 1 17 18 27 36 37 38 39 40 xpsdsval 
 |-  ( ph -> ( <. A , B >. P <. C , D >. ) = sup ( { ( A ( ( dist ` ( toMetSp ` M ) ) |` ( ( Base ` ( toMetSp ` M ) ) X. ( Base ` ( toMetSp ` M ) ) ) ) C ) , ( B ( ( dist ` ( toMetSp ` N ) ) |` ( ( Base ` ( toMetSp ` N ) ) X. ( Base ` ( toMetSp ` N ) ) ) ) D ) } , RR* , < ) )
42 37 39 ovresd 
 |-  ( ph -> ( A ( ( dist ` ( toMetSp ` M ) ) |` ( ( Base ` ( toMetSp ` M ) ) X. ( Base ` ( toMetSp ` M ) ) ) ) C ) = ( A ( dist ` ( toMetSp ` M ) ) C ) )
43 20 oveqd 
 |-  ( ph -> ( A M C ) = ( A ( dist ` ( toMetSp ` M ) ) C ) )
44 42 43 eqtr4d 
 |-  ( ph -> ( A ( ( dist ` ( toMetSp ` M ) ) |` ( ( Base ` ( toMetSp ` M ) ) X. ( Base ` ( toMetSp ` M ) ) ) ) C ) = ( A M C ) )
45 38 40 ovresd 
 |-  ( ph -> ( B ( ( dist ` ( toMetSp ` N ) ) |` ( ( Base ` ( toMetSp ` N ) ) X. ( Base ` ( toMetSp ` N ) ) ) ) D ) = ( B ( dist ` ( toMetSp ` N ) ) D ) )
46 29 oveqd 
 |-  ( ph -> ( B N D ) = ( B ( dist ` ( toMetSp ` N ) ) D ) )
47 45 46 eqtr4d 
 |-  ( ph -> ( B ( ( dist ` ( toMetSp ` N ) ) |` ( ( Base ` ( toMetSp ` N ) ) X. ( Base ` ( toMetSp ` N ) ) ) ) D ) = ( B N D ) )
48 44 47 preq12d 
 |-  ( ph -> { ( A ( ( dist ` ( toMetSp ` M ) ) |` ( ( Base ` ( toMetSp ` M ) ) X. ( Base ` ( toMetSp ` M ) ) ) ) C ) , ( B ( ( dist ` ( toMetSp ` N ) ) |` ( ( Base ` ( toMetSp ` N ) ) X. ( Base ` ( toMetSp ` N ) ) ) ) D ) } = { ( A M C ) , ( B N D ) } )
49 48 supeq1d 
 |-  ( ph -> sup ( { ( A ( ( dist ` ( toMetSp ` M ) ) |` ( ( Base ` ( toMetSp ` M ) ) X. ( Base ` ( toMetSp ` M ) ) ) ) C ) , ( B ( ( dist ` ( toMetSp ` N ) ) |` ( ( Base ` ( toMetSp ` N ) ) X. ( Base ` ( toMetSp ` N ) ) ) ) D ) } , RR* , < ) = sup ( { ( A M C ) , ( B N D ) } , RR* , < ) )
50 41 49 eqtrd 
 |-  ( ph -> ( <. A , B >. P <. C , D >. ) = sup ( { ( A M C ) , ( B N D ) } , RR* , < ) )