Metamath Proof Explorer


Theorem txmetcn

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 txmetcn
|- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) -> ( F e. ( ( J tX K ) Cn L ) <-> ( F : ( X X. Y ) --> Z /\ A. x e. X A. y e. Y A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) 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 1 mopntopon
 |-  ( C e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
5 2 mopntopon
 |-  ( D e. ( *Met ` Y ) -> K e. ( TopOn ` Y ) )
6 txtopon
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
7 4 5 6 syl2an
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
8 7 3adant3
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
9 3 mopntopon
 |-  ( E e. ( *Met ` Z ) -> L e. ( TopOn ` Z ) )
10 9 3ad2ant3
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) -> L e. ( TopOn ` Z ) )
11 cncnp
 |-  ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ L e. ( TopOn ` Z ) ) -> ( F e. ( ( J tX K ) Cn L ) <-> ( F : ( X X. Y ) --> Z /\ A. t e. ( X X. Y ) F e. ( ( ( J tX K ) CnP L ) ` t ) ) ) )
12 8 10 11 syl2anc
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) -> ( F e. ( ( J tX K ) Cn L ) <-> ( F : ( X X. Y ) --> Z /\ A. t e. ( X X. Y ) F e. ( ( ( J tX K ) CnP L ) ` t ) ) ) )
13 fveq2
 |-  ( t = <. x , y >. -> ( ( ( J tX K ) CnP L ) ` t ) = ( ( ( J tX K ) CnP L ) ` <. x , y >. ) )
14 13 eleq2d
 |-  ( t = <. x , y >. -> ( F e. ( ( ( J tX K ) CnP L ) ` t ) <-> F e. ( ( ( J tX K ) CnP L ) ` <. x , y >. ) ) )
15 14 ralxp
 |-  ( A. t e. ( X X. Y ) F e. ( ( ( J tX K ) CnP L ) ` t ) <-> A. x e. X A. y e. Y F e. ( ( ( J tX K ) CnP L ) ` <. x , y >. ) )
16 simplr
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ F : ( X X. Y ) --> Z ) /\ ( x e. X /\ y e. Y ) ) -> F : ( X X. Y ) --> Z )
17 1 2 3 txmetcnp
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( x e. X /\ y e. Y ) ) -> ( F e. ( ( ( J tX K ) CnP L ) ` <. x , y >. ) <-> ( F : ( X X. Y ) --> Z /\ A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) ) )
18 17 adantlr
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ F : ( X X. Y ) --> Z ) /\ ( x e. X /\ y e. Y ) ) -> ( F e. ( ( ( J tX K ) CnP L ) ` <. x , y >. ) <-> ( F : ( X X. Y ) --> Z /\ A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) ) )
19 16 18 mpbirand
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ F : ( X X. Y ) --> Z ) /\ ( x e. X /\ y e. Y ) ) -> ( F e. ( ( ( J tX K ) CnP L ) ` <. x , y >. ) <-> A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) )
20 19 2ralbidva
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ F : ( X X. Y ) --> Z ) -> ( A. x e. X A. y e. Y F e. ( ( ( J tX K ) CnP L ) ` <. x , y >. ) <-> A. x e. X A. y e. Y A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) )
21 15 20 syl5bb
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ F : ( X X. Y ) --> Z ) -> ( A. t e. ( X X. Y ) F e. ( ( ( J tX K ) CnP L ) ` t ) <-> A. x e. X A. y e. Y A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) )
22 21 pm5.32da
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) -> ( ( F : ( X X. Y ) --> Z /\ A. t e. ( X X. Y ) F e. ( ( ( J tX K ) CnP L ) ` t ) ) <-> ( F : ( X X. Y ) --> Z /\ A. x e. X A. y e. Y A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) ) )
23 12 22 bitrd
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) -> ( F e. ( ( J tX K ) Cn L ) <-> ( F : ( X X. Y ) --> Z /\ A. x e. X A. y e. Y A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) ) )