P. 210 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20901-21000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prdsxmslem1 20901	Lemma for prdsms 20904. The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> S e. W )   &    |- ( ph -> I e. Fin )   &    |- D = ( dist ` Y )   &    |- B = ( Base ` Y )   &    |- ( ph -> R : I --> *MetSp )   =>    |- ( ph -> D e. ( *Met ` B ) )
Theorem	prdsxmslem2 20902*	Lemma for prdsxms 20903. The topology generated by the supremum metric is the same as the product topology, when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> S e. W )   &    |- ( ph -> I e. Fin )   &    |- D = ( dist ` Y )   &    |- B = ( Base ` Y )   &    |- ( ph -> R : I --> *MetSp )   &    |- J = ( TopOpen ` Y )   &    |- V = ( Base ` ( R ` k ) )   &    |- E = ( ( dist ` ( R ` k ) ) |` ( V X. V ) )   &    |- K = ( TopOpen ` ( R ` k ) )   &    |- C = { x | E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) }   =>    |- ( ph -> J = ( MetOpen ` D ) )
Theorem	prdsxms 20903	The indexed product structure is an extended metric space when the index set is finite. (Although the extended metric is still valid when the index set is infinite, it no longer agrees with the product topology, which is not metrizable in any case.) (Contributed by Mario Carneiro, 28-Aug-2015.)
|- Y = ( S X_s R )   =>    |- ( ( S e. W /\ I e. Fin /\ R : I --> *MetSp ) -> Y e. *MetSp )
Theorem	prdsms 20904	The indexed product structure is a metric space when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- Y = ( S X_s R )   =>    |- ( ( S e. W /\ I e. Fin /\ R : I --> MetSp ) -> Y e. MetSp )
Theorem	pwsxms 20905	The product of a finite family of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. *MetSp /\ I e. Fin ) -> Y e. *MetSp )
Theorem	pwsms 20906	The product of a finite family of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. MetSp /\ I e. Fin ) -> Y e. MetSp )
Theorem	xpsxms 20907	A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- T = ( R X.s S )   =>    |- ( ( R e. *MetSp /\ S e. *MetSp ) -> T e. *MetSp )
Theorem	xpsms 20908	A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- T = ( R X.s S )   =>    |- ( ( R e. MetSp /\ S e. MetSp ) -> T e. MetSp )
Theorem	tmsxps 20909	Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- P = ( dist ` ( (toMetSp ` M ) X.s (toMetSp ` N ) ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   =>    |- ( ph -> P e. ( *Met ` ( X X. Y ) ) )
Theorem	tmsxpsmopn 20910	Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- P = ( dist ` ( (toMetSp ` M ) X.s (toMetSp ` N ) ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- J = ( MetOpen ` M )   &    |- K = ( MetOpen ` N )   &    |- L = ( MetOpen ` P )   =>    |- ( ph -> L = ( J tX K ) )
Theorem	tmsxpsval 20911	Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- P = ( dist ` ( (toMetSp ` M ) X.s (toMetSp ` N ) ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. Y )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   =>    |- ( ph -> ( <. A , B >. P <. C , D >. ) = sup ( { ( A M C ) , ( B N D ) } , RR* , < ) )
Theorem	tmsxpsval2 20912	Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- P = ( dist ` ( (toMetSp ` M ) X.s (toMetSp ` N ) ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. Y )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   =>    |- ( ph -> ( <. A , B >. P <. C , D >. ) = if ( ( A M C ) <_ ( B N D ) , ( B N D ) , ( A M C ) ) )
12.4.5  Continuity in metric spaces
Theorem	metcnp3 20913*	Two ways to express that F is continuous at P for metric spaces. Proposition 14-4.2 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) )
Theorem	metcnp 20914*	Two ways to say a mapping from metric C to metric D is continuous at point P. (Contributed by NM, 11-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( P C w ) < z -> ( ( F ` P ) D ( F ` w ) ) < y ) ) ) )
Theorem	metcnp2 20915*	Two ways to say a mapping from metric C to metric D is continuous at point P. The distance arguments are swapped compared to metcnp 20914 (and Munkres' metcn 20916) for compatibility with df-lm 19600. Definition 1.3-3 of [Kreyszig] p. 20. (Contributed by NM, 4-Jun-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( w C P ) < z -> ( ( F ` w ) D ( F ` P ) ) < y ) ) ) )
Theorem	metcn 20916*	Two ways to say a mapping from metric C to metric D is continuous. Theorem 10.1 of [Munkres] p. 127. The second biconditional argument says that for every positive "epsilon" y there is a positive "delta" z such that a distance less than delta in C maps to a distance less than epsilon in D. (Contributed by NM, 15-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. X A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( F ` x ) D ( F ` w ) ) < y ) ) ) )
Theorem	metcnpi 20917*	Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 20914. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. X ( ( P C y ) < x -> ( ( F ` P ) D ( F ` y ) ) < A ) )
Theorem	metcnpi2 20918*	Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 20915. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. X ( ( y C P ) < x -> ( ( F ` y ) D ( F ` P ) ) < A ) )
Theorem	metcnpi3 20919*	Epsilon-delta property of a metric space function continuous at P. A variation of metcnpi2 20918 with non-strict ordering. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. X ( ( y C P ) <_ x -> ( ( F ` y ) D ( F ` P ) ) <_ A ) )
Theorem	txmetcnp 20920*	Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   &    |- L = ( MetOpen ` E )   =>    |- ( ( ( 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 ) ) ) )
Theorem	txmetcn 20921*	Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   &    |- L = ( MetOpen ` E )   =>    |- ( ( 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 ) ) ) )
12.4.6  The uniform structure generated by a metric
Theorem	metuvalOLD 20922*	Value of the uniform structure generated by metric D. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( D e. ( *Met ` X ) -> (metUnifOLD ` D ) = ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) )
Theorem	metuval 20923*	Value of the uniform structure generated by metric D. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ( D e. (PsMet ` X ) -> (metUnif ` D ) = ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) )
Theorem	metustelOLD 20924*	Define a filter base F generated by a metric D. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( D e. ( *Met ` X ) -> ( B e. F <-> E. a e. RR+ B = ( `' D " ( 0 [,) a ) ) ) )
Theorem	metustel 20925*	Define a filter base F generated by a metric D. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( D e. (PsMet ` X ) -> ( B e. F <-> E. a e. RR+ B = ( `' D " ( 0 [,) a ) ) ) )
Theorem	metustssOLD 20926*	Range of the elements of the filter base generated by the metric D. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( D e. ( *Met ` X ) /\ A e. F ) -> A C_ ( X X. X ) )
Theorem	metustss 20927*	Range of the elements of the filter base generated by the metric D. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( D e. (PsMet ` X ) /\ A e. F ) -> A C_ ( X X. X ) )
Theorem	metustrelOLD 20928*	Elements of the filter base generated by the metric D are relations. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( D e. ( *Met ` X ) /\ A e. F ) -> Rel A )
Theorem	metustrel 20929*	Elements of the filter base generated by the metric D are relations. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( D e. (PsMet ` X ) /\ A e. F ) -> Rel A )
Theorem	metusttoOLD 20930*	Any two elements of the filter base generated by the metric D can be compared, like for RR+ (i.e. it's totally ordered). (Contributed by Thierry Arnoux, 22-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( D e. ( *Met ` X ) /\ A e. F /\ B e. F ) -> ( A C_ B \/ B C_ A ) )
Theorem	metustto 20931*	Any two elements of the filter base generated by the metric D can be compared, like for RR+ (i.e. it's totally ordered). (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( D e. (PsMet ` X ) /\ A e. F /\ B e. F ) -> ( A C_ B \/ B C_ A ) )
Theorem	metustidOLD 20932*	The identity diagonal is included in all elements of the filter base generated by the metric D. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( D e. ( *Met ` X ) /\ A e. F ) -> ( _I |` X ) C_ A )
Theorem	metustid 20933*	The identity diagonal is included in all elements of the filter base generated by the metric D. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( D e. (PsMet ` X ) /\ A e. F ) -> ( _I |` X ) C_ A )
Theorem	metustsymOLD 20934*	Elements of the filter base generated by the metric D are symmetric. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( D e. ( *Met ` X ) /\ A e. F ) -> `' A = A )
Theorem	metustsym 20935*	Elements of the filter base generated by the metric D are symmetric. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( D e. (PsMet ` X ) /\ A e. F ) -> `' A = A )
Theorem	metustexhalfOLD 20936*	For any element A of the filter base generated by the metric D, the half element (corresponding to half the distance) is also in this base. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( ( X =/= (/) /\ D e. ( *Met ` X ) ) /\ A e. F ) -> E. v e. F ( v o. v ) C_ A )
Theorem	metustexhalf 20937*	For any element A of the filter base generated by the metric D, the half element (corresponding to half the distance) is also in this base. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ A e. F ) -> E. v e. F ( v o. v ) C_ A )
Theorem	metustfbasOLD 20938*	The filter base generated by a metric D. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> F e. ( fBas ` ( X X. X ) ) )
Theorem	metustfbas 20939*	The filter base generated by a metric D. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> F e. ( fBas ` ( X X. X ) ) )
Theorem	metustOLD 20940*	The uniform structure generated by a metric D. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( ( X X. X ) filGen F ) e. (UnifOn ` X ) )
Theorem	metust 20941*	The uniform structure generated by a metric D. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> ( ( X X. X ) filGen F ) e. (UnifOn ` X ) )
Theorem	cfilucfilOLD 20942*	Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 21574. (Contributed by Thierry Arnoux, 29-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( C e. (CauFilu ` ( ( X X. X ) filGen F ) ) <-> ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )
Theorem	cfilucfil 20943*	Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 21574. (Contributed by Thierry Arnoux, 29-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> ( C e. (CauFilu ` ( ( X X. X ) filGen F ) ) <-> ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )
Theorem	metuustOLD 20944	The uniform structure generated by metric D is a uniform structure. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> (metUnifOLD ` D ) e. (UnifOn ` X ) )
Theorem	metuust 20945	The uniform structure generated by metric D is a uniform structure. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> (metUnif ` D ) e. (UnifOn ` X ) )
Theorem	cfilucfil2OLD 20946*	Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 21574. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( C e. (CauFilu ` (metUnifOLD ` D ) ) <-> ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )
Theorem	cfilucfil2 20947*	Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 21574. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> ( C e. (CauFilu ` (metUnif ` D ) ) <-> ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )
Theorem	blval2 20948	The ball around a point P, alternative definition. (Contributed by Thierry Arnoux, 7-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( D e. (PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( P ( ball ` D ) R ) = ( ( `' D " ( 0 [,) R ) ) " { P } ) )
Theorem	elbl4 20949	Membership in a ball, alternative definition. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( ( D e. (PsMet ` X ) /\ R e. RR+ ) /\ ( A e. X /\ B e. X ) ) -> ( B e. ( A ( ball ` D ) R ) <-> B ( `' D " ( 0 [,) R ) ) A ) )
Theorem	metuelOLD 20950*	Elementhood in the uniform structure generated by a metric D (Contributed by Thierry Arnoux, 8-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( V e. (metUnifOLD ` D ) <-> ( V C_ ( X X. X ) /\ E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ V ) ) )
Theorem	metuel 20951*	Elementhood in the uniform structure generated by a metric D (Contributed by Thierry Arnoux, 8-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> ( V e. (metUnif ` D ) <-> ( V C_ ( X X. X ) /\ E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ V ) ) )
Theorem	metuel2 20952*	Elementhood in the uniform structure generated by a metric D (Contributed by Thierry Arnoux, 24-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- U = (metUnif ` D )   =>    |- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> ( V e. U <-> ( V C_ ( X X. X ) /\ E. d e. RR+ A. x e. X A. y e. X ( ( x D y ) < d -> x V y ) ) ) )
Theorem	metustblOLD 20953*	The "section" image of an entourage at a point P always contains a ball (centered on this point). (Contributed by Thierry Arnoux, 8-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( D e. ( *Met ` X ) /\ V e. (metUnifOLD ` D ) /\ P e. X ) -> E. a e. ran ( ball ` D ) ( P e. a /\ a C_ ( V " { P } ) ) )
Theorem	metustbl 20954*	The "section" image of an entourage at a point P always contains a ball (centered on this point). (Contributed by Thierry Arnoux, 8-Dec-2017.)
|- ( ( D e. (PsMet ` X ) /\ V e. (metUnif ` D ) /\ P e. X ) -> E. a e. ran ( ball ` D ) ( P e. a /\ a C_ ( V " { P } ) ) )
Theorem	metutopOLD 20955	The topology induced by a uniform structure generated by a metric D is that metric's open sets. (Contributed by Thierry Arnoux, 6-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> (unifTop ` (metUnifOLD ` D ) ) = ( MetOpen ` D ) )
Theorem	psmetutop 20956	The topology induced by a uniform structure generated by a metric D is generated by that metric's open balls. (Contributed by Thierry Arnoux, 6-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> (unifTop ` (metUnif ` D ) ) = ( topGen ` ran ( ball ` D ) ) )
Theorem	xmetutop 20957	The topology induced by a uniform structure generated by an extended metric D is that metric's open sets. (Contributed by Thierry Arnoux, 11-Mar-2018.)
|- ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> (unifTop ` (metUnif ` D ) ) = ( MetOpen ` D ) )
Theorem	xmsuspOLD 20958	If the uniform set of a metric space is the uniform structure generated by its metric, then it is a uniform space. (Contributed by Thierry Arnoux, 14-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- X = ( Base ` F )   &    |- D = ( ( dist ` F ) |` ( X X. X ) )   &    |- U = (UnifSt ` F )   =>    |- ( ( X =/= (/) /\ F e. *MetSp /\ U = (metUnifOLD ` D ) ) -> F e. UnifSp )
Theorem	xmsusp 20959	If the uniform set of a metric space is the uniform structure generated by its metric, then it is a uniform space. (Contributed by Thierry Arnoux, 14-Dec-2017.)
|- X = ( Base ` F )   &    |- D = ( ( dist ` F ) |` ( X X. X ) )   &    |- U = (UnifSt ` F )   =>    |- ( ( X =/= (/) /\ F e. *MetSp /\ U = (metUnif ` D ) ) -> F e. UnifSp )
Theorem	restmetu 20960	The uniform structure generated by the restriction of a metric is its trace. (Contributed by Thierry Arnoux, 18-Dec-2017.)
|- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> ( (metUnif ` D ) ↾t ( A X. A ) ) = (metUnif ` ( D |` ( A X. A ) ) ) )
Theorem	metucnOLD 20961*	Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn 20916. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- U = (metUnifOLD ` C )   &    |- V = (metUnifOLD ` D )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> Y =/= (/) )   &    |- ( ph -> C e. ( *Met ` X ) )   &    |- ( ph -> D e. ( *Met ` Y ) )   =>    |- ( ph -> ( F e. ( U Cnu V ) <-> ( F : X --> Y /\ A. d e. RR+ E. c e. RR+ A. x e. X A. y e. X ( ( x C y ) < c -> ( ( F ` x ) D ( F ` y ) ) < d ) ) ) )
Theorem	metucn 20962*	Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn 20916. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- U = (metUnif ` C )   &    |- V = (metUnif ` D )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> Y =/= (/) )   &    |- ( ph -> C e. (PsMet ` X ) )   &    |- ( ph -> D e. (PsMet ` Y ) )   =>    |- ( ph -> ( F e. ( U Cnu V ) <-> ( F : X --> Y /\ A. d e. RR+ E. c e. RR+ A. x e. X A. y e. X ( ( x C y ) < c -> ( ( F ` x ) D ( F ` y ) ) < d ) ) ) )
12.4.7  Examples of metric spaces
Theorem	dscmet 20963*	The discrete metric on any set X. Definition 1.1-8 of [Kreyszig] p. 8. (Contributed by FL, 12-Oct-2006.)
|- D = ( x e. X , y e. X |-> if ( x = y , 0 , 1 ) )   =>    |- ( X e. V -> D e. ( Met ` X ) )
Theorem	dscopn 20964*	The discrete metric generates the discrete topology. In particular, the discrete topology is metrizable. (Contributed by Mario Carneiro, 29-Jan-2014.)
|- D = ( x e. X , y e. X |-> if ( x = y , 0 , 1 ) )   =>    |- ( X e. V -> ( MetOpen ` D ) = ~P X )
Theorem	nrmmetd 20965*	Show that a group norm generates a metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> F : X --> RR )   &    |- ( ( ph /\ x e. X ) -> ( ( F ` x ) = 0 <-> x = .0. ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x .- y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )   =>    |- ( ph -> ( F o. .- ) e. ( Met ` X ) )
Theorem	abvmet 20966	An absolute value F generates a metric defined by d ( x , y ) = F ( x - y ), analogously to cnmet 21149. (In fact, the ring structure is not needed at all; the group properties abveq0 17346 and abvtri 17350, abvneg 17354 are sufficient.) (Contributed by Mario Carneiro, 9-Sep-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` R )   &    |- A = (AbsVal ` R )   &    |- .- = ( -g ` R )   =>    |- ( F e. A -> ( F o. .- ) e. ( Met ` X ) )
12.4.8  Normed algebraic structures
Syntax	cnm 20967	Norm of a normed ring.
class norm
Syntax	cngp 20968	The class of all normed groups.
class NrmGrp
Syntax	ctng 20969	Make a normed group from a norm and a group.
class toNrmGrp
Syntax	cnrg 20970	Normed ring.
class NrmRing
Syntax	cnlm 20971	Normed module.
class NrmMod
Syntax	cnvc 20972	Normed vector space.
class NrmVec
Definition	df-nm 20973*	Define the norm on a group or ring (when it makes sense) in terms of the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- norm = ( w e. _V |-> ( x e. ( Base ` w ) |-> ( x ( dist ` w ) ( 0g ` w ) ) ) )
Definition	df-ngp 20974	Define a normed group, which is a group with a right-translation-invariant metric. This is not a standard notion, but is helpful as the most general context in which a metric-like norm makes sense. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- NrmGrp = { g e. ( Grp i^i MetSp ) | ( ( norm ` g ) o. ( -g ` g ) ) C_ ( dist ` g ) }
Definition	df-tng 20975*	Define a function that fills in the topology and metric components of a structure given a group and a norm on it. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- toNrmGrp = ( g e. _V , f e. _V |-> ( ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) sSet <. (TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. ) )
Definition	df-nrg 20976	A normed ring is a ring with an induced topology and metric such that the metric is translation-invariant and the norm (distance from 0) is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- NrmRing = { w e. NrmGrp | ( norm ` w ) e. (AbsVal ` w ) }
Definition	df-nlm 20977*	A normed (left) module is a module which is also a normed group over a normed ring, such that the norm distributes over scalar multiplication. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- NrmMod = { w e. (NrmGrp i^i LMod ) | [. (Scalar ` w ) / f ]. ( f e. NrmRing /\ A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) ) }
Definition	df-nvc 20978	A normed vector space is a normed module which is also a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- NrmVec = (NrmMod i^i LVec )
Theorem	nmfval 20979*	The value of the norm function. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` W )   &    |- X = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- D = ( dist ` W )   =>    |- N = ( x e. X |-> ( x D .0. ) )
Theorem	nmval 20980	The value of the norm function. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` W )   &    |- X = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- D = ( dist ` W )   =>    |- ( A e. X -> ( N ` A ) = ( A D .0. ) )
Theorem	nmfval2 20981*	The value of the norm function using a restricted metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` W )   &    |- X = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- D = ( dist ` W )   &    |- E = ( D |` ( X X. X ) )   =>    |- ( W e. Grp -> N = ( x e. X |-> ( x E .0. ) ) )
Theorem	nmval2 20982	The value of the norm function using a restricted metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` W )   &    |- X = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- D = ( dist ` W )   &    |- E = ( D |` ( X X. X ) )   =>    |- ( ( W e. Grp /\ A e. X ) -> ( N ` A ) = ( A E .0. ) )
Theorem	nmf2 20983	The norm is a function from the base set into the reals. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` W )   &    |- X = ( Base ` W )   &    |- D = ( dist ` W )   &    |- E = ( D |` ( X X. X ) )   =>    |- ( ( W e. Grp /\ E e. ( Met ` X ) ) -> N : X --> RR )
Theorem	nmpropd 20984	Weak property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> ( Base ` K ) = ( Base ` L ) )   &    |- ( ph -> ( +g ` K ) = ( +g ` L ) )   &    |- ( ph -> ( dist ` K ) = ( dist ` L ) )   =>    |- ( ph -> ( norm ` K ) = ( norm ` L ) )
Theorem	nmpropd2 20985*	Strong property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> K e. Grp )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )   =>    |- ( ph -> ( norm ` K ) = ( norm ` L ) )
Theorem	isngp 20986	The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) C_ D ) )
Theorem	isngp2 20987	The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   &    |- X = ( Base ` G )   &    |- E = ( D |` ( X X. X ) )   =>    |- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) = E ) )
Theorem	isngp3 20988*	The property of being a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- N = ( norm ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   &    |- X = ( Base ` G )   =>    |- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ A. x e. X A. y e. X ( x D y ) = ( N ` ( x .- y ) ) ) )
Theorem	ngpgrp 20989	A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( G e. NrmGrp -> G e. Grp )
Theorem	ngpms 20990	A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( G e. NrmGrp -> G e. MetSp )
Theorem	ngpxms 20991	A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( G e. NrmGrp -> G e. *MetSp )
Theorem	ngptps 20992	A normed group is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- ( G e. NrmGrp -> G e. TopSp )
Theorem	ngpds 20993	Value of the distance function in terms of the norm of a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` G )   &    |- X = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A .- B ) ) )
Theorem	ngpdsr 20994	Value of the distance function in terms of the norm of a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` G )   &    |- X = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( B .- A ) ) )
Theorem	ngpds2 20995	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( ( A .- B ) D .0. ) )
Theorem	ngpds2r 20996	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( ( B .- A ) D .0. ) )
Theorem	ngpds3 20997	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( .0. D ( A .- B ) ) )
Theorem	ngpds3r 20998	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( .0. D ( B .- A ) ) )
Theorem	ngprcan 20999	Cancel right addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A .+ C ) D ( B .+ C ) ) = ( A D B ) )
Theorem	ngplcan 21000	Cancel left addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( C .+ A ) D ( C .+ B ) ) = ( A D B ) )