Metamath Proof Explorer

Theorem tmsxpsval2

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 tmsxpsval2 
|- ( ph -> ( <. A , B >. P <. C , D >. ) = if ( ( A M C ) <_ ( B N D ) , ( B N D ) , ( A M C ) ) )

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 1 2 3 4 5 6 7 tmsxpsval 
 |-  ( ph -> ( <. A , B >. P <. C , D >. ) = sup ( { ( A M C ) , ( B N D ) } , RR* , < ) )
9 xrltso 
 |-  < Or RR*
10 xmetcl 
 |-  ( ( M e. ( *Met ` X ) /\ A e. X /\ C e. X ) -> ( A M C ) e. RR* )
11 2 4 6 10 syl3anc 
 |-  ( ph -> ( A M C ) e. RR* )
12 xmetcl 
 |-  ( ( N e. ( *Met ` Y ) /\ B e. Y /\ D e. Y ) -> ( B N D ) e. RR* )
13 3 5 7 12 syl3anc 
 |-  ( ph -> ( B N D ) e. RR* )
14 suppr 
 |-  ( ( < Or RR* /\ ( A M C ) e. RR* /\ ( B N D ) e. RR* ) -> sup ( { ( A M C ) , ( B N D ) } , RR* , < ) = if ( ( B N D ) < ( A M C ) , ( A M C ) , ( B N D ) ) )
15 9 11 13 14 mp3an2i 
 |-  ( ph -> sup ( { ( A M C ) , ( B N D ) } , RR* , < ) = if ( ( B N D ) < ( A M C ) , ( A M C ) , ( B N D ) ) )
16 xrltnle 
 |-  ( ( ( B N D ) e. RR* /\ ( A M C ) e. RR* ) -> ( ( B N D ) < ( A M C ) <-> -. ( A M C ) <_ ( B N D ) ) )
17 13 11 16 syl2anc 
 |-  ( ph -> ( ( B N D ) < ( A M C ) <-> -. ( A M C ) <_ ( B N D ) ) )
18 17 ifbid 
 |-  ( ph -> if ( ( B N D ) < ( A M C ) , ( A M C ) , ( B N D ) ) = if ( -. ( A M C ) <_ ( B N D ) , ( A M C ) , ( B N D ) ) )
19 ifnot 
 |-  if ( -. ( A M C ) <_ ( B N D ) , ( A M C ) , ( B N D ) ) = if ( ( A M C ) <_ ( B N D ) , ( B N D ) , ( A M C ) )
20 18 19 eqtrdi 
 |-  ( ph -> if ( ( B N D ) < ( A M C ) , ( A M C ) , ( B N D ) ) = if ( ( A M C ) <_ ( B N D ) , ( B N D ) , ( A M C ) ) )
21 8 15 20 3eqtrd 
 |-  ( ph -> ( <. A , B >. P <. C , D >. ) = if ( ( A M C ) <_ ( B N D ) , ( B N D ) , ( A M C ) ) )