P. 217 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21601-21700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prdsms 21601	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 21602	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 21603	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 21604	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 21605	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 21606	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 21607	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 21608	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 21609	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 21610*	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 21611*	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 21612*	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 21611 (and Munkres' metcn 21613) for compatibility with df-lm 20300. 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 21613*	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 21614*	Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 21611. (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 21615*	Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 21612. (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 21616*	Epsilon-delta property of a metric space function continuous at P. A variation of metcnpi2 21615 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 21617*	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 21618*	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	metuval 21619*	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	metustel 21620*	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	metustss 21621*	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	metustrel 21622*	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	metustto 21623*	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	metustid 21624*	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	metustsym 21625*	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	metustexhalf 21626*	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	metustfbas 21627*	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	metust 21628*	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	cfilucfil 21629*	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 22290. (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	metuust 21630	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	cfilucfil2 21631*	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 22290. (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 21632	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 21633	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	metuel 21634*	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 21635*	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	metustbl 21636*	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	psmetutop 21637	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 21638	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	xmsusp 21639	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 21640	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	metucn 21641*	Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn 21613. (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 21642*	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 21643*	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 21644*	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 21645	An absolute value F generates a metric defined by d ( x , y ) = F ( x - y ), analogously to cnmet 21847. (In fact, the ring structure is not needed at all; the group properties abveq0 18109 and abvtri 18113, abvneg 18117 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 21646	Norm of a normed ring.
class norm
Syntax	cngp 21647	The class of all normed groups.
class NrmGrp
Syntax	ctng 21648	Make a normed group from a norm and a group.
class toNrmGrp
Syntax	cnrg 21649	Normed ring.
class NrmRing
Syntax	cnlm 21650	Normed module.
class NrmMod
Syntax	cnvc 21651	Normed vector space.
class NrmVec
Definition	df-nm 21652*	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 21653	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 21654*	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 21655	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 21656*	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 21657	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 21658*	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 21659	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 21660*	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 21661	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 21662	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 21663	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 21664*	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 21665	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 21666	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 21667*	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 21668	A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( G e. NrmGrp -> G e. Grp )
Theorem	ngpms 21669	A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( G e. NrmGrp -> G e. MetSp )
Theorem	ngpxms 21670	A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( G e. NrmGrp -> G e. *MetSp )
Theorem	ngptps 21671	A normed group is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- ( G e. NrmGrp -> G e. TopSp )
Theorem	ngpds 21672	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 21673	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 21674	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 21675	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 21676	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 21677	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 21678	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 21679	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 ) )
Theorem	isngp4 21680*	Express the property of being a normed group purely in terms of right-translation invariance of the metric instead of using the definition of norm (which itself uses the metric). (Contributed by Mario Carneiro, 29-Oct-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- D = ( dist ` G )   =>    |- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ A. x e. X A. y e. X A. z e. X ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) ) )
Theorem	ngpinvds 21681	Two elements are the same distance apart as their inverses. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- I = ( invg ` G )   &    |- D = ( dist ` G )   =>    |- ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X ) ) -> ( ( I ` A ) D ( I ` B ) ) = ( A D B ) )
Theorem	ngpsubcan 21682	Cancel right subtraction inside a distance calculation. (Contributed by Mario Carneiro, 4-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	nmf 21683	The norm on a normed group is a function into the reals. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   =>    |- ( G e. NrmGrp -> N : X --> RR )
Theorem	nmcl 21684	The norm of a normed group is closed in the reals. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X ) -> ( N ` A ) e. RR )
Theorem	nmge0 21685	The norm of a normed group is nonnegative. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X ) -> 0 <_ ( N ` A ) )
Theorem	nmeq0 21686	The identity is the only element of the group with zero norm. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X ) -> ( ( N ` A ) = 0 <-> A = .0. ) )
Theorem	nmne0 21687	The norm of a nonzero element is nonzero. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ A =/= .0. ) -> ( N ` A ) =/= 0 )
Theorem	nmrpcl 21688	The norm of a nonzero element is a positive real. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ A =/= .0. ) -> ( N ` A ) e. RR+ )
Theorem	nminv 21689	The norm of a negated element is the same as the norm of the original element. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   &    |- I = ( invg ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X ) -> ( N ` ( I ` A ) ) = ( N ` A ) )
Theorem	nmmtri 21690	The triangle inequality for the norm of a subtraction. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( A .- B ) ) <_ ( ( N ` A ) + ( N ` B ) ) )
Theorem	nmsub 21691	The norm of the difference between two elements. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( A .- B ) ) = ( N ` ( B .- A ) ) )
Theorem	nmrtri 21692	Reverse triangle inequality for the norm of a subtraction. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( abs ` ( ( N ` A ) - ( N ` B ) ) ) <_ ( N ` ( A .- B ) ) )
Theorem	nm2dif 21693	Inequality for the difference of norms. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( ( N ` A ) - ( N ` B ) ) <_ ( N ` ( A .- B ) ) )
Theorem	nmtri 21694	The triangle inequality for the norm of a sum. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( A .+ B ) ) <_ ( ( N ` A ) + ( N ` B ) ) )
Theorem	nm0 21695	Norm of the identity element. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- N = ( norm ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( G e. NrmGrp -> ( N ` .0. ) = 0 )
Theorem	subgnm 21696	The norm in a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- H = ( G ↾s A )   &    |- N = ( norm ` G )   &    |- M = ( norm ` H )   =>    |- ( A e. (SubGrp ` G ) -> M = ( N |` A ) )
Theorem	subgnm2 21697	A substructure assigns the same values to the norms of elements of a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- H = ( G ↾s A )   &    |- N = ( norm ` G )   &    |- M = ( norm ` H )   =>    |- ( ( A e. (SubGrp ` G ) /\ X e. A ) -> ( M ` X ) = ( N ` X ) )
Theorem	subgngp 21698	A normed group restricted to a subgroup is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- H = ( G ↾s A )   =>    |- ( ( G e. NrmGrp /\ A e. (SubGrp ` G ) ) -> H e. NrmGrp )
Theorem	ngptgp 21699	A normed abelian group is a topological group (with the topology induced by the metric induced by the norm). (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ( G e. NrmGrp /\ G e. Abel ) -> G e. TopGrp )
Theorem	ngppropd 21700*	Property deduction for a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( 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 -> ( TopOpen ` K ) = ( TopOpen ` L ) )   =>    |- ( ph -> ( K e. NrmGrp <-> L e. NrmGrp ) )