P. 226 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22501-22600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nvclvec 22501	A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. LVec )
Theorem	nvclmod 22502	A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. LMod )
Theorem	isnvc2 22503	A normed vector space is just a normed module whose scalar ring is a division ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. NrmVec <-> ( W e. NrmMod /\ F e. DivRing ) )
Theorem	nvctvc 22504	A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. TopVec )
Theorem	lssnlm 22505	A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( W ↾s U )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. NrmMod /\ U e. S ) -> X e. NrmMod )
Theorem	lssnvc 22506	A subspace of a normed vector space is a normed vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( W ↾s U )   &    |- S = ( LSubSp ` W )   =>    |- ( ( W e. NrmVec /\ U e. S ) -> X e. NrmVec )
Theorem	rlmnvc 22507	The ring module over a normed division ring is a normed vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ( R e. NrmRing /\ R e. DivRing ) -> (ringLMod ` R ) e. NrmVec )
Theorem	ngpocelbl 22508	Membership of an off-center vector in a ball in a normed module. (Contributed by NM, 27-Dec-2007.) (Revised by AV, 14-Oct-2021.)
|- N = ( norm ` G )   &    |- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- D = ( ( dist ` G ) |` ( X X. X ) )   =>    |- ( ( G e. NrmMod /\ R e. RR* /\ ( P e. X /\ A e. X ) ) -> ( ( P .+ A ) e. ( P ( ball ` D ) R ) <-> ( N ` A ) < R ) )
12.4.9  Normed space homomorphisms (bounded linear operators)
Syntax	cnmo 22509	The operator norm function.
class normOp
Syntax	cnghm 22510	The class of normed group homomorphisms.
class NGHom
Syntax	cnmhm 22511	The class of normed module homomorphisms.
class NMHom
Definition	df-nmo 22512*	Define the norm of an operator between two normed groups (usually vector spaces). This definition produces an operator norm function for each pair of groups <. s , t >.. Equivalent to the definition of linear operator norm in [AkhiezerGlazman] p. 39. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 25-Sep-2020.)
|- normOp = ( s e. NrmGrp , t e. NrmGrp |-> ( f e. ( s GrpHom t ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) } , RR* , < ) ) )
Definition	df-nghm 22513*	Define the set of normed group homomorphisms between two normed groups. A normed group homomorphism is a group homomorphism which additionally bounds the increase of norm by a fixed real operator. In vector spaces these are also known as bounded linear operators. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- NGHom = ( s e. NrmGrp , t e. NrmGrp |-> ( `' ( s normOp t ) " RR ) )
Definition	df-nmhm 22514*	Define a normed module homomorphism, also known as a bounded linear operator. This is a module homomorphism (a linear function) such that the operator norm is finite, or equivalently there is a constant c such that... (Contributed by Mario Carneiro, 18-Oct-2015.)
|- NMHom = ( s e. NrmMod , t e. NrmMod |-> ( ( s LMHom t ) i^i ( s NGHom t ) ) )
Theorem	nmoffn 22515	The function producing operator norm functions is a function on normed groups. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.)
|- normOp Fn (NrmGrp X. NrmGrp )
Theorem	reldmnghm 22516	Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- Rel dom NGHom
Theorem	reldmnmhm 22517	Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- Rel dom NMHom
Theorem	nmofval 22518*	Value of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 26-Sep-2020.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- L = ( norm ` S )   &    |- M = ( norm ` T )   =>    |- ( ( S e. NrmGrp /\ T e. NrmGrp ) -> N = ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) ) )
Theorem	nmoval 22519*	Value of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 26-Sep-2020.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- L = ( norm ` S )   &    |- M = ( norm ` T )   =>    |- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) = inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) )
Theorem	nmogelb 22520*	Property of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- L = ( norm ` S )   &    |- M = ( norm ` T )   =>    |- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ A e. RR* ) -> ( A <_ ( N ` F ) <-> A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> A <_ r ) ) )
Theorem	nmolb 22521*	Any upper bound on the values of a linear operator translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- L = ( norm ` S )   &    |- M = ( norm ` T )   =>    |- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ A e. RR /\ 0 <_ A ) -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) )
Theorem	nmolb2d 22522*	Any upper bound on the values of a linear operator at nonzero vectors translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- L = ( norm ` S )   &    |- M = ( norm ` T )   &    |- .0. = ( 0g ` S )   &    |- ( ph -> S e. NrmGrp )   &    |- ( ph -> T e. NrmGrp )   &    |- ( ph -> F e. ( S GrpHom T ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ( ph /\ ( x e. V /\ x =/= .0. ) ) -> ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) )   =>    |- ( ph -> ( N ` F ) <_ A )
Theorem	nmof 22523	The operator norm is a function into the extended reals. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.)
|- N = ( S normOp T )   =>    |- ( ( S e. NrmGrp /\ T e. NrmGrp ) -> N : ( S GrpHom T ) --> RR* )
Theorem	nmocl 22524	The operator norm of an operator is an extended real. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- N = ( S normOp T )   =>    |- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) e. RR* )
Theorem	nmoge0 22525	The operator norm of an operator is nonnegative. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- N = ( S normOp T )   =>    |- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> 0 <_ ( N ` F ) )
Theorem	nghmfval 22526	A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- N = ( S normOp T )   =>    |- ( S NGHom T ) = ( `' N " RR )
Theorem	isnghm 22527	A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- N = ( S normOp T )   =>    |- ( F e. ( S NGHom T ) <-> ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) )
Theorem	isnghm2 22528	A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- N = ( S normOp T )   =>    |- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( F e. ( S NGHom T ) <-> ( N ` F ) e. RR ) )
Theorem	isnghm3 22529	A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- N = ( S normOp T )   =>    |- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( F e. ( S NGHom T ) <-> ( N ` F ) < +oo ) )
Theorem	bddnghm 22530	A bounded group homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- N = ( S normOp T )   =>    |- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( A e. RR /\ ( N ` F ) <_ A ) ) -> F e. ( S NGHom T ) )
Theorem	nghmcl 22531	A normed group homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- N = ( S normOp T )   =>    |- ( F e. ( S NGHom T ) -> ( N ` F ) e. RR )
Theorem	nmoi 22532	The operator norm achieves the minimum of the set of upper bounds, if the operator is bounded. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- L = ( norm ` S )   &    |- M = ( norm ` T )   =>    |- ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( M ` ( F ` X ) ) <_ ( ( N ` F ) x. ( L ` X ) ) )
Theorem	nmoix 22533	The operator norm is a bound on the size of an operator, even when it is infinite (using extended real multiplication). (Contributed by Mario Carneiro, 18-Oct-2015.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- L = ( norm ` S )   &    |- M = ( norm ` T )   =>    |- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( M ` ( F ` X ) ) <_ ( ( N ` F ) xe ( L ` X ) ) )
Theorem	nmoi2 22534	The operator norm is a bound on the growth of a vector under the action of the operator. (Contributed by Mario Carneiro, 19-Oct-2015.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- L = ( norm ` S )   &    |- M = ( norm ` T )   &    |- .0. = ( 0g ` S )   =>    |- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( M ` ( F ` X ) ) / ( L ` X ) ) <_ ( N ` F ) )
Theorem	nmoleub 22535*	The operator norm, defined as an infimum of upper bounds, can also be defined as a supremum of norms of F ( x ) away from zero. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- L = ( norm ` S )   &    |- M = ( norm ` T )   &    |- .0. = ( 0g ` S )   &    |- ( ph -> S e. NrmGrp )   &    |- ( ph -> T e. NrmGrp )   &    |- ( ph -> F e. ( S GrpHom T ) )   &    |- ( ph -> A e. RR* )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) ) )
Theorem	nghmrcl1 22536	Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NGHom T ) -> S e. NrmGrp )
Theorem	nghmrcl2 22537	Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NGHom T ) -> T e. NrmGrp )
Theorem	nghmghm 22538	A normed group homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NGHom T ) -> F e. ( S GrpHom T ) )
Theorem	nmo0 22539	The operator norm of the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- .0. = ( 0g ` T )   =>    |- ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( N ` ( V X. { .0. } ) ) = 0 )
Theorem	nmoeq0 22540	The operator norm is zero only for the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- .0. = ( 0g ` T )   =>    |- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( ( N ` F ) = 0 <-> F = ( V X. { .0. } ) ) )
Theorem	nmoco 22541	An upper bound on the operator norm of a composition. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- N = ( S normOp U )   &    |- L = ( T normOp U )   &    |- M = ( S normOp T )   =>    |- ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> ( N ` ( F o. G ) ) <_ ( ( L ` F ) x. ( M ` G ) ) )
Theorem	nghmco 22542	The composition of normed group homomorphisms is a normed group homomorphism. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> ( F o. G ) e. ( S NGHom U ) )
Theorem	nmotri 22543	Triangle inequality for the operator norm. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- N = ( S normOp T )   &    |- .+ = ( +g ` T )   =>    |- ( ( T e. Abel /\ F e. ( S NGHom T ) /\ G e. ( S NGHom T ) ) -> ( N ` ( F oF .+ G ) ) <_ ( ( N ` F ) + ( N ` G ) ) )
Theorem	nghmplusg 22544	The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- .+ = ( +g ` T )   =>    |- ( ( T e. Abel /\ F e. ( S NGHom T ) /\ G e. ( S NGHom T ) ) -> ( F oF .+ G ) e. ( S NGHom T ) )
Theorem	0nghm 22545	The zero operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- V = ( Base ` S )   &    |- .0. = ( 0g ` T )   =>    |- ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( V X. { .0. } ) e. ( S NGHom T ) )
Theorem	nmoid 22546	The operator norm of the identity function on a nontrivial group. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- N = ( S normOp S )   &    |- V = ( Base ` S )   &    |- .0. = ( 0g ` S )   =>    |- ( ( S e. NrmGrp /\ { .0. } C. V ) -> ( N ` ( _I |` V ) ) = 1 )
Theorem	idnghm 22547	The identity operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- V = ( Base ` S )   =>    |- ( S e. NrmGrp -> ( _I |` V ) e. ( S NGHom S ) )
Theorem	nmods 22548	Upper bound for the distance between the values of a bounded linear operator. (Contributed by Mario Carneiro, 22-Oct-2015.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- C = ( dist ` S )   &    |- D = ( dist ` T )   =>    |- ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> ( ( F ` A ) D ( F ` B ) ) <_ ( ( N ` F ) x. ( A C B ) ) )
Theorem	nghmcn 22549	A normed group homomorphism is a continuous function. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- J = ( TopOpen ` S )   &    |- K = ( TopOpen ` T )   =>    |- ( F e. ( S NGHom T ) -> F e. ( J Cn K ) )
Theorem	isnmhm 22550	A normed module homomorphism is a left module homomorphism which is also a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NMHom T ) <-> ( ( S e. NrmMod /\ T e. NrmMod ) /\ ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) )
Theorem	nmhmrcl1 22551	Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NMHom T ) -> S e. NrmMod )
Theorem	nmhmrcl2 22552	Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NMHom T ) -> T e. NrmMod )
Theorem	nmhmlmhm 22553	A normed module homomorphism is a left module homomorphism (a linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NMHom T ) -> F e. ( S LMHom T ) )
Theorem	nmhmnghm 22554	A normed module homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NMHom T ) -> F e. ( S NGHom T ) )
Theorem	nmhmghm 22555	A normed module homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NMHom T ) -> F e. ( S GrpHom T ) )
Theorem	isnmhm2 22556	A normed module homomorphism is a left module homomorphism with bounded norm (a bounded linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.)
|- N = ( S normOp T )   =>    |- ( ( S e. NrmMod /\ T e. NrmMod /\ F e. ( S LMHom T ) ) -> ( F e. ( S NMHom T ) <-> ( N ` F ) e. RR ) )
Theorem	nmhmcl 22557	A normed module homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- N = ( S normOp T )   =>    |- ( F e. ( S NMHom T ) -> ( N ` F ) e. RR )
Theorem	idnmhm 22558	The identity operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- V = ( Base ` S )   =>    |- ( S e. NrmMod -> ( _I |` V ) e. ( S NMHom S ) )
Theorem	0nmhm 22559	The zero operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- V = ( Base ` S )   &    |- .0. = ( 0g ` T )   &    |- F = (Scalar ` S )   &    |- G = (Scalar ` T )   =>    |- ( ( S e. NrmMod /\ T e. NrmMod /\ F = G ) -> ( V X. { .0. } ) e. ( S NMHom T ) )
Theorem	nmhmco 22560	The composition of bounded linear operators is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- ( ( F e. ( T NMHom U ) /\ G e. ( S NMHom T ) ) -> ( F o. G ) e. ( S NMHom U ) )
Theorem	nmhmplusg 22561	The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- .+ = ( +g ` T )   =>    |- ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> ( F oF .+ G ) e. ( S NMHom T ) )
12.4.10  Topology on the reals
Theorem	qtopbaslem 22562	The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014.)
|- S C_ RR*   =>    |- ( (,) " ( S X. S ) ) e. TopBases
Theorem	qtopbas 22563	The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.)
|- ( (,) " ( QQ X. QQ ) ) e. TopBases
Theorem	retopbas 22564	A basis for the standard topology on the reals. (Contributed by NM, 6-Feb-2007.) (Proof shortened by Mario Carneiro, 17-Jun-2014.)
|- ran (,) e. TopBases
Theorem	retop 22565	The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
|- ( topGen ` ran (,) ) e. Top
Theorem	uniretop 22566	The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.)
|- RR = U. ( topGen ` ran (,) )
Theorem	retopon 22567	The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ( topGen ` ran (,) ) e. (TopOn ` RR )
Theorem	retps 22568	The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.)
|- K = { <. ( Base ` ndx ) , RR >. , <. (TopSet ` ndx ) , ( topGen ` ran (,) ) >. }   =>    |- K e. TopSp
Theorem	iooretop 22569	Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.)
|- ( A (,) B ) e. ( topGen ` ran (,) )
Theorem	icccld 22570	Closed intervals are closed sets of the standard topology on RR. (Contributed by FL, 14-Sep-2007.)
|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
Theorem	icopnfcld 22571	Right-unbounded closed intervals are closed sets of the standard topology on RR. (Contributed by Mario Carneiro, 17-Feb-2015.)
|- ( A e. RR -> ( A [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
Theorem	iocmnfcld 22572	Left-unbounded closed intervals are closed sets of the standard topology on RR. (Contributed by Mario Carneiro, 17-Feb-2015.)
|- ( A e. RR -> ( -oo (,] A ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
Theorem	qdensere 22573	QQ is dense in the standard topology on RR. (Contributed by NM, 1-Mar-2007.)
|- ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = RR
Theorem	cnmetdval 22574	Value of the distance function of the metric space of complex numbers. (Contributed by NM, 9-Dec-2006.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- D = ( abs o. - )   =>    |- ( ( A e. CC /\ B e. CC ) -> ( A D B ) = ( abs ` ( A - B ) ) )
Theorem	cnmet 22575	The absolute value metric determines a metric space on the complex numbers. This theorem provides a link between complex numbers and metrics spaces, making metric space theorems available for use with complex numbers. (Contributed by FL, 9-Oct-2006.)
|- ( abs o. - ) e. ( Met ` CC )
Theorem	cnxmet 22576	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ( abs o. - ) e. ( *Met ` CC )
Theorem	cnbl0 22577	Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
|- D = ( abs o. - )   =>    |- ( R e. RR* -> ( `' abs " ( 0 [,) R ) ) = ( 0 ( ball ` D ) R ) )
Theorem	cnblcld 22578*	Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
|- D = ( abs o. - )   =>    |- ( R e. RR* -> ( `' abs " ( 0 [,] R ) ) = { x e. CC | ( 0 D x ) <_ R } )
Theorem	cnfldms 22579	The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ℂfld e. MetSp
Theorem	cnfldxms 22580	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ℂfld e. *MetSp
Theorem	cnfldtps 22581	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ℂfld e. TopSp
Theorem	cnfldnm 22582	The norm of the field of complex numbers. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- abs = ( norm ` ℂfld )
Theorem	cnngp 22583	The complex numbers form a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ℂfld e. NrmGrp
Theorem	cnnrg 22584	The complex numbers form a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ℂfld e. NrmRing
Theorem	cnfldtopn 22585	The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J = ( MetOpen ` ( abs o. - ) )
Theorem	cnfldtopon 22586	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J e. (TopOn ` CC )
Theorem	cnfldtop 22587	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J e. Top
Theorem	cnfldhaus 22588	The topology of the complex numbers is Hausdorff. (Contributed by Mario Carneiro, 8-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J e. Haus
Theorem	unicntop 22589	The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- CC = U. ( TopOpen ` ℂfld )
Theorem	cnopn 22590	The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- CC e. ( TopOpen ` ℂfld )
Theorem	zringnrg 22591	The ring of integers is a normed ring. (Contributed by AV, 13-Jun-2019.)
|- ℤring e. NrmRing
Theorem	remetdval 22592	Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> ( A D B ) = ( abs ` ( A - B ) ) )
Theorem	remet 22593	The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- D e. ( Met ` RR )
Theorem	rexmet 22594	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- D e. ( *Met ` RR )
Theorem	bl2ioo 22595	A ball in terms of an open interval of reals. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> ( A ( ball ` D ) B ) = ( ( A - B ) (,) ( A + B ) ) )
Theorem	ioo2bl 22596	An open interval of reals in terms of a ball. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> ( A (,) B ) = ( ( ( A + B ) / 2 ) ( ball ` D ) ( ( B - A ) / 2 ) ) )
Theorem	ioo2blex 22597	An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> ( A (,) B ) e. ran ( ball ` D ) )
Theorem	blssioo 22598	The balls of the standard real metric space are included in the open real intervals. (Contributed by NM, 8-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ran ( ball ` D ) C_ ran (,)
Theorem	tgioo 22599	The topology generated by open intervals of reals is the same as the open sets of the standard metric space on the reals. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   &    |- J = ( MetOpen ` D )   =>    |- ( topGen ` ran (,) ) = J
Theorem	qdensere2 22600	QQ is dense in RR. (Contributed by NM, 24-Aug-2007.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   &    |- J = ( MetOpen ` D )   =>    |- ( ( cls ` J ) ` QQ ) = RR