Metamath Proof Explorer

Theorem txmetcnp

Description: Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses metcn.2 
|- J = ( MetOpen ` C )
metcn.4 
|- K = ( MetOpen ` D )
txmetcnp.4 
|- L = ( MetOpen ` E )
Assertion txmetcnp 
|- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> ( F e. ( ( ( J tX K ) CnP L ) ` <. A , B >. ) <-> ( F : ( X X. Y ) --> Z /\ A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( A C u ) < w /\ ( B D v ) < w ) -> ( ( A F B ) E ( u F v ) ) < z ) ) ) )

Proof

Step Hyp Ref Expression
1 metcn.2 
 |-  J = ( MetOpen ` C )
2 metcn.4 
 |-  K = ( MetOpen ` D )
3 txmetcnp.4 
 |-  L = ( MetOpen ` E )
4 eqid 
 |-  ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) = ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) )
5 simpl1 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> C e. ( *Met ` X ) )
6 simpl2 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> D e. ( *Met ` Y ) )
7 4 5 6 tmsxps 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) e. ( *Met ` ( X X. Y ) ) )
8 simpl3 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> E e. ( *Met ` Z ) )
9 opelxpi 
 |-  ( ( A e. X /\ B e. Y ) -> <. A , B >. e. ( X X. Y ) )
10 9 adantl 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> <. A , B >. e. ( X X. Y ) )
11 eqid 
 |-  ( MetOpen ` ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) ) = ( MetOpen ` ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) )
12 11 3 metcnp 
 |-  ( ( ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) e. ( *Met ` ( X X. Y ) ) /\ E e. ( *Met ` Z ) /\ <. A , B >. e. ( X X. Y ) ) -> ( F e. ( ( ( MetOpen ` ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) ) CnP L ) ` <. A , B >. ) <-> ( F : ( X X. Y ) --> Z /\ A. z e. RR+ E. w e. RR+ A. x e. ( X X. Y ) ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) x ) < w -> ( ( F ` <. A , B >. ) E ( F ` x ) ) < z ) ) ) )
13 7 8 10 12 syl3anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> ( F e. ( ( ( MetOpen ` ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) ) CnP L ) ` <. A , B >. ) <-> ( F : ( X X. Y ) --> Z /\ A. z e. RR+ E. w e. RR+ A. x e. ( X X. Y ) ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) x ) < w -> ( ( F ` <. A , B >. ) E ( F ` x ) ) < z ) ) ) )
14 4 5 6 1 2 11 tmsxpsmopn 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> ( MetOpen ` ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) ) = ( J tX K ) )
15 14 oveq1d 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> ( ( MetOpen ` ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) ) CnP L ) = ( ( J tX K ) CnP L ) )
16 15 fveq1d 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> ( ( ( MetOpen ` ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) ) CnP L ) ` <. A , B >. ) = ( ( ( J tX K ) CnP L ) ` <. A , B >. ) )
17 16 eleq2d 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> ( F e. ( ( ( MetOpen ` ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) ) CnP L ) ` <. A , B >. ) <-> F e. ( ( ( J tX K ) CnP L ) ` <. A , B >. ) ) )
18 oveq2 
 |-  ( x = <. u , v >. -> ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) x ) = ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) <. u , v >. ) )
19 18 breq1d 
 |-  ( x = <. u , v >. -> ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) x ) < w <-> ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) <. u , v >. ) < w ) )
20 df-ov 
 |-  ( A F B ) = ( F ` <. A , B >. )
21 20 oveq1i 
 |-  ( ( A F B ) E ( F ` x ) ) = ( ( F ` <. A , B >. ) E ( F ` x ) )
22 fveq2 
 |-  ( x = <. u , v >. -> ( F ` x ) = ( F ` <. u , v >. ) )
23 df-ov 
 |-  ( u F v ) = ( F ` <. u , v >. )
24 22 23 eqtr4di 
 |-  ( x = <. u , v >. -> ( F ` x ) = ( u F v ) )
25 24 oveq2d 
 |-  ( x = <. u , v >. -> ( ( A F B ) E ( F ` x ) ) = ( ( A F B ) E ( u F v ) ) )
26 21 25 eqtr3id 
 |-  ( x = <. u , v >. -> ( ( F ` <. A , B >. ) E ( F ` x ) ) = ( ( A F B ) E ( u F v ) ) )
27 26 breq1d 
 |-  ( x = <. u , v >. -> ( ( ( F ` <. A , B >. ) E ( F ` x ) ) < z <-> ( ( A F B ) E ( u F v ) ) < z ) )
28 19 27 imbi12d 
 |-  ( x = <. u , v >. -> ( ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) x ) < w -> ( ( F ` <. A , B >. ) E ( F ` x ) ) < z ) <-> ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) <. u , v >. ) < w -> ( ( A F B ) E ( u F v ) ) < z ) ) )
29 28 ralxp 
 |-  ( A. x e. ( X X. Y ) ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) x ) < w -> ( ( F ` <. A , B >. ) E ( F ` x ) ) < z ) <-> A. u e. X A. v e. Y ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) <. u , v >. ) < w -> ( ( A F B ) E ( u F v ) ) < z ) )
30 5 ad2antrr 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ ( w e. RR+ /\ ( u e. X /\ v e. Y ) ) ) -> C e. ( *Met ` X ) )
31 6 ad2antrr 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ ( w e. RR+ /\ ( u e. X /\ v e. Y ) ) ) -> D e. ( *Met ` Y ) )
32 simpllr 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ ( w e. RR+ /\ ( u e. X /\ v e. Y ) ) ) -> ( A e. X /\ B e. Y ) )
33 32 simpld 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ ( w e. RR+ /\ ( u e. X /\ v e. Y ) ) ) -> A e. X )
34 32 simprd 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ ( w e. RR+ /\ ( u e. X /\ v e. Y ) ) ) -> B e. Y )
35 simprrl 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ ( w e. RR+ /\ ( u e. X /\ v e. Y ) ) ) -> u e. X )
36 simprrr 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ ( w e. RR+ /\ ( u e. X /\ v e. Y ) ) ) -> v e. Y )
37 4 30 31 33 34 35 36 tmsxpsval2 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ ( w e. RR+ /\ ( u e. X /\ v e. Y ) ) ) -> ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) <. u , v >. ) = if ( ( A C u ) <_ ( B D v ) , ( B D v ) , ( A C u ) ) )
38 37 breq1d 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ ( w e. RR+ /\ ( u e. X /\ v e. Y ) ) ) -> ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) <. u , v >. ) < w <-> if ( ( A C u ) <_ ( B D v ) , ( B D v ) , ( A C u ) ) < w ) )
39 xmetcl 
 |-  ( ( C e. ( *Met ` X ) /\ A e. X /\ u e. X ) -> ( A C u ) e. RR* )
40 30 33 35 39 syl3anc 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ ( w e. RR+ /\ ( u e. X /\ v e. Y ) ) ) -> ( A C u ) e. RR* )
41 xmetcl 
 |-  ( ( D e. ( *Met ` Y ) /\ B e. Y /\ v e. Y ) -> ( B D v ) e. RR* )
42 31 34 36 41 syl3anc 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ ( w e. RR+ /\ ( u e. X /\ v e. Y ) ) ) -> ( B D v ) e. RR* )
43 rpxr 
 |-  ( w e. RR+ -> w e. RR* )
44 43 ad2antrl 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ ( w e. RR+ /\ ( u e. X /\ v e. Y ) ) ) -> w e. RR* )
45 xrmaxlt 
 |-  ( ( ( A C u ) e. RR* /\ ( B D v ) e. RR* /\ w e. RR* ) -> ( if ( ( A C u ) <_ ( B D v ) , ( B D v ) , ( A C u ) ) < w <-> ( ( A C u ) < w /\ ( B D v ) < w ) ) )
46 40 42 44 45 syl3anc 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ ( w e. RR+ /\ ( u e. X /\ v e. Y ) ) ) -> ( if ( ( A C u ) <_ ( B D v ) , ( B D v ) , ( A C u ) ) < w <-> ( ( A C u ) < w /\ ( B D v ) < w ) ) )
47 38 46 bitrd 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ ( w e. RR+ /\ ( u e. X /\ v e. Y ) ) ) -> ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) <. u , v >. ) < w <-> ( ( A C u ) < w /\ ( B D v ) < w ) ) )
48 47 imbi1d 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ ( w e. RR+ /\ ( u e. X /\ v e. Y ) ) ) -> ( ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) <. u , v >. ) < w -> ( ( A F B ) E ( u F v ) ) < z ) <-> ( ( ( A C u ) < w /\ ( B D v ) < w ) -> ( ( A F B ) E ( u F v ) ) < z ) ) )
49 48 anassrs 
 |-  ( ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ w e. RR+ ) /\ ( u e. X /\ v e. Y ) ) -> ( ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) <. u , v >. ) < w -> ( ( A F B ) E ( u F v ) ) < z ) <-> ( ( ( A C u ) < w /\ ( B D v ) < w ) -> ( ( A F B ) E ( u F v ) ) < z ) ) )
50 49 2ralbidva 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ w e. RR+ ) -> ( A. u e. X A. v e. Y ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) <. u , v >. ) < w -> ( ( A F B ) E ( u F v ) ) < z ) <-> A. u e. X A. v e. Y ( ( ( A C u ) < w /\ ( B D v ) < w ) -> ( ( A F B ) E ( u F v ) ) < z ) ) )
51 29 50 syl5bb 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) /\ w e. RR+ ) -> ( A. x e. ( X X. Y ) ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) x ) < w -> ( ( F ` <. A , B >. ) E ( F ` x ) ) < z ) <-> A. u e. X A. v e. Y ( ( ( A C u ) < w /\ ( B D v ) < w ) -> ( ( A F B ) E ( u F v ) ) < z ) ) )
52 51 rexbidva 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) -> ( E. w e. RR+ A. x e. ( X X. Y ) ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) x ) < w -> ( ( F ` <. A , B >. ) E ( F ` x ) ) < z ) <-> E. w e. RR+ A. u e. X A. v e. Y ( ( ( A C u ) < w /\ ( B D v ) < w ) -> ( ( A F B ) E ( u F v ) ) < z ) ) )
53 52 ralbidv 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) /\ F : ( X X. Y ) --> Z ) -> ( A. z e. RR+ E. w e. RR+ A. x e. ( X X. Y ) ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) x ) < w -> ( ( F ` <. A , B >. ) E ( F ` x ) ) < z ) <-> A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( A C u ) < w /\ ( B D v ) < w ) -> ( ( A F B ) E ( u F v ) ) < z ) ) )
54 53 pm5.32da 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> ( ( F : ( X X. Y ) --> Z /\ A. z e. RR+ E. w e. RR+ A. x e. ( X X. Y ) ( ( <. A , B >. ( dist ` ( ( toMetSp ` C ) Xs. ( toMetSp ` D ) ) ) x ) < w -> ( ( F ` <. A , B >. ) E ( F ` x ) ) < z ) ) <-> ( F : ( X X. Y ) --> Z /\ A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( A C u ) < w /\ ( B D v ) < w ) -> ( ( A F B ) E ( u F v ) ) < z ) ) ) )
55 13 17 54 3bitr3d 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> ( F e. ( ( ( J tX K ) CnP L ) ` <. A , B >. ) <-> ( F : ( X X. Y ) --> Z /\ A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( A C u ) < w /\ ( B D v ) < w ) -> ( ( A F B ) E ( u F v ) ) < z ) ) ) )