P. 209 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20801-20900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	metust 20801*	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 20802*	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 21434. (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 20803*	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 21434. (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 20804	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 20805	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 20806*	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 21434. (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 20807*	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 21434. (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 20808	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 20809	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 20810*	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 20811*	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 20812*	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 20813*	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 20814*	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 20815	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 20816	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 20817	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 20818	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 20819	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 20820	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 20821*	Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn 20776. (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 20822*	Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn 20776. (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 20823*	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 20824*	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 20825*	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 20826	An absolute value F generates a metric defined by d ( x , y ) = F ( x - y ), analogously to cnmet 21009. (In fact, the ring structure is not needed at all; the group properties abveq0 17253 and abvtri 17257, abvneg 17261 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 20827	Norm of a normed ring.
class norm
Syntax	cngp 20828	The class of all normed groups.
class NrmGrp
Syntax	ctng 20829	Make a normed group from a norm and a group.
class toNrmGrp
Syntax	cnrg 20830	Normed ring.
class NrmRing
Syntax	cnlm 20831	Normed module.
class NrmMod
Syntax	cnvc 20832	Normed vector space.
class NrmVec
Definition	df-nm 20833*	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 20834	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 20835*	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 20836	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 20837*	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 20838	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 20839*	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 20840	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 20841*	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 20842	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 20843	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 20844	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 20845*	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 20846	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 20847	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 20848*	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 20849	A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( G e. NrmGrp -> G e. Grp )
Theorem	ngpms 20850	A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( G e. NrmGrp -> G e. MetSp )
Theorem	ngpxms 20851	A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( G e. NrmGrp -> G e. *MetSp )
Theorem	ngptps 20852	A normed group is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- ( G e. NrmGrp -> G e. TopSp )
Theorem	ngpds 20853	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 20854	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 20855	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 20856	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 20857	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 20858	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 20859	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 20860	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 20861*	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 20862	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 20863	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 20864	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 20865	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 20866	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 20867	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 20868	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 20869	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 20870	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 20871	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 20872	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 20873	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 20874	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 20875	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 20876	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 20877	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 20878	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 20879	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 20880	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 20881*	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 ) )
Theorem	reldmtng 20882	The function toNrmGrp is a two-argument function. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- Rel dom toNrmGrp
Theorem	tngval 20883	Value of the function which augments a given structure G with a norm N. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- .- = ( -g ` G )   &    |- D = ( N o. .- )   &    |- J = ( MetOpen ` D )   =>    |- ( ( G e. V /\ N e. W ) -> T = ( ( G sSet <. ( dist ` ndx ) , D >. ) sSet <. (TopSet ` ndx ) , J >. ) )
Theorem	tnglem 20884	Lemma for tngbas 20885 and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- E = Slot K   &    |- K e. NN   &    |- K < 9   =>    |- ( N e. V -> ( E ` G ) = ( E ` T ) )
Theorem	tngbas 20885	The base set of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- B = ( Base ` G )   =>    |- ( N e. V -> B = ( Base ` T ) )
Theorem	tngplusg 20886	The group addition of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- .+ = ( +g ` G )   =>    |- ( N e. V -> .+ = ( +g ` T ) )
Theorem	tng0 20887	The group identity of a structure augmented with a norm. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- .0. = ( 0g ` G )   =>    |- ( N e. V -> .0. = ( 0g ` T ) )
Theorem	tngmulr 20888	The ring multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- .x. = ( .r ` G )   =>    |- ( N e. V -> .x. = ( .r ` T ) )
Theorem	tngsca 20889	The scalar ring of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- F = (Scalar ` G )   =>    |- ( N e. V -> F = (Scalar ` T ) )
Theorem	tngvsca 20890	The scalar multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- .x. = ( .s ` G )   =>    |- ( N e. V -> .x. = ( .s ` T ) )
Theorem	tngip 20891	The inner product operation of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- ., = ( .i ` G )   =>    |- ( N e. V -> ., = ( .i ` T ) )
Theorem	tngds 20892	The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- .- = ( -g ` G )   =>    |- ( N e. V -> ( N o. .- ) = ( dist ` T ) )
Theorem	tngtset 20893	The topology generated by a normed structure. (Contributed by Mario Carneiro, 3-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- D = ( dist ` T )   &    |- J = ( MetOpen ` D )   =>    |- ( ( G e. V /\ N e. W ) -> J = (TopSet ` T ) )
Theorem	tngtopn 20894	The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- D = ( dist ` T )   &    |- J = ( MetOpen ` D )   =>    |- ( ( G e. V /\ N e. W ) -> J = ( TopOpen ` T ) )
Theorem	tngnm 20895	The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- X = ( Base ` G )   &    |- A e. _V   =>    |- ( ( G e. Grp /\ N : X --> A ) -> N = ( norm ` T ) )
Theorem	tngngp2 20896	A norm turns a group into a normed group iff the generated metric is in fact a metric. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- X = ( Base ` G )   &    |- D = ( dist ` T )   =>    |- ( N : X --> RR -> ( T e. NrmGrp <-> ( G e. Grp /\ D e. ( Met ` X ) ) ) )
Theorem	tngngpd 20897*	Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- X = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> N : X --> RR )   &    |- ( ( ph /\ x e. X ) -> ( ( N ` x ) = 0 <-> x = .0. ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )   =>    |- ( ph -> T e. NrmGrp )
Theorem	tngngp 20898*	Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- T = ( G toNrmGrp N )   &    |- X = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( N : X --> RR -> ( T e. NrmGrp <-> ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) )
Theorem	isnrg 20899	A normed ring is a ring with a norm that makes it into a normed group, and such that the norm is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- N = ( norm ` R )   &    |- A = (AbsVal ` R )   =>    |- ( R e. NrmRing <-> ( R e. NrmGrp /\ N e. A ) )
Theorem	nrgabv 20900	The norm of a normed ring is an absolute value. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- N = ( norm ` R )   &    |- A = (AbsVal ` R )   =>    |- ( R e. NrmRing -> N e. A )