P. 214 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21301-21400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rlmnlm 21301	The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. NrmRing -> (ringLMod ` R ) e. NrmMod )
Theorem	nrgtrg 21302	A normed ring is a topological ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. NrmRing -> R e. TopRing )
Theorem	nrginvrcnlem 21303*	Lemma for nrginvrcn 21304. Compare this proof with reccn2 13440, the elementary proof of continuity of division. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- X = ( Base ` R )   &    |- U = (Unit ` R )   &    |- I = ( invr ` R )   &    |- N = ( norm ` R )   &    |- D = ( dist ` R )   &    |- ( ph -> R e. NrmRing )   &    |- ( ph -> R e. NzRing )   &    |- ( ph -> A e. U )   &    |- ( ph -> B e. RR+ )   &    |- T = ( if ( 1 <_ ( ( N ` A ) x. B ) , 1 , ( ( N ` A ) x. B ) ) x. ( ( N ` A ) / 2 ) )   =>    |- ( ph -> E. x e. RR+ A. y e. U ( ( A D y ) < x -> ( ( I ` A ) D ( I ` y ) ) < B ) )
Theorem	nrginvrcn 21304	The ring inverse function is continuous in a normed ring. (Note that this is true even in rings which are not division rings.) (Contributed by Mario Carneiro, 6-Oct-2015.)
|- X = ( Base ` R )   &    |- U = (Unit ` R )   &    |- I = ( invr ` R )   &    |- J = ( TopOpen ` R )   =>    |- ( R e. NrmRing -> I e. ( ( J ↾t U ) Cn ( J ↾t U ) ) )
Theorem	nrgtdrg 21305	A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( ( R e. NrmRing /\ R e. DivRing ) -> R e. TopDRing )
Theorem	nlmtlm 21306	A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( W e. NrmMod -> W e. TopMod )
Theorem	isnvc 21307	A normed vector space is just a normed module which is algebraically a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec <-> ( W e. NrmMod /\ W e. LVec ) )
Theorem	nvcnlm 21308	A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. NrmMod )
Theorem	nvclvec 21309	A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. LVec )
Theorem	nvclmod 21310	A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. LMod )
Theorem	isnvc2 21311	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 21312	A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. TopVec )
Theorem	lssnlm 21313	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 21314	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 21315	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 )
12.4.9  Normed space homomorphisms (bounded linear operators)
Syntax	cnmo 21316	The operator norm function.
class normOp
Syntax	cnghm 21317	The class of normed group homomorphisms.
class NGHom
Syntax	cnmhm 21318	The class of normed module homomorphisms.
class NMHom
Definition	df-nmo 21319*	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.)
|- normOp = ( s e. NrmGrp , t e. NrmGrp |-> ( f e. ( s GrpHom t ) |-> sup ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) } , RR* , `' < ) ) )
Definition	df-nghm 21320*	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 21321*	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 21322	The function producing operator norm functions is a function on normed groups. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- normOp Fn (NrmGrp X. NrmGrp )
Theorem	reldmnghm 21323	Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- Rel dom NGHom
Theorem	reldmnmhm 21324	Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- Rel dom NMHom
Theorem	nmofval 21325*	Value of the operator norm. (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 ) -> N = ( f e. ( S GrpHom T ) |-> sup ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , `' < ) ) )
Theorem	nmoval 21326*	Value of the operator norm. (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 ) ) -> ( N ` F ) = sup ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , `' < ) )
Theorem	nmogelb 21327*	Property of the operator norm. (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 ) ) /\ 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 21328*	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.)
|- 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 21329*	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 21330	The operator norm is a function into the extended reals. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- N = ( S normOp T )   =>    |- ( ( S e. NrmGrp /\ T e. NrmGrp ) -> N : ( S GrpHom T ) --> RR* )
Theorem	nmocl 21331	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 21332	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 21333	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 21334	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 21335	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 21336	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 21337	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 21338	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 21339	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 21340	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 21341	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 21342*	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 21343	Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NGHom T ) -> S e. NrmGrp )
Theorem	nghmrcl2 21344	Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NGHom T ) -> T e. NrmGrp )
Theorem	nghmghm 21345	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 21346	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 21347	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 21348	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 21349	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 21350	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 21351	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 21352	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 21353	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 21354	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 21355	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 21356	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 21357	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 21358	Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NMHom T ) -> S e. NrmMod )
Theorem	nmhmrcl2 21359	Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NMHom T ) -> T e. NrmMod )
Theorem	nmhmlmhm 21360	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 21361	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 21362	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 21363	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 21364	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 21365	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 21366	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 21367	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 21368	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 21369	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 21370	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 21371	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 21372	The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
|- ( topGen ` ran (,) ) e. Top
Theorem	uniretop 21373	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 21374	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	retpsOLD 21375	The standard topological space on the reals. (Contributed by NM, 10-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- <. RR , ( topGen ` ran (,) ) >. e. TopSpOLD
Theorem	retps 21376	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 21377	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 21378	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 21379	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 21380	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 21381	QQ is dense in the standard topology on RR. (Contributed by NM, 1-Mar-2007.)
|- ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = RR
Theorem	cnmetdval 21382	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 21383	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 21384	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ( abs o. - ) e. ( *Met ` CC )
Theorem	cnbl0 21385	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 21386*	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 21387	The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ℂfld e. MetSp
Theorem	cnfldxms 21388	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ℂfld e. *MetSp
Theorem	cnfldtps 21389	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ℂfld e. TopSp
Theorem	cnfldnm 21390	The norm of the field of complex numbers. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- abs = ( norm ` ℂfld )
Theorem	cnngp 21391	The complex numbers form a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ℂfld e. NrmGrp
Theorem	cnnrg 21392	The complex numbers form a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ℂfld e. NrmRing
Theorem	cnfldtopn 21393	The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J = ( MetOpen ` ( abs o. - ) )
Theorem	cnfldtopon 21394	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 21395	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J e. Top
Theorem	cnfldhaus 21396	The topology of the complex numbers is Hausdorff. (Contributed by Mario Carneiro, 8-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J e. Haus
Theorem	zringnrg 21397	The ring of integers is a normed ring. (Contributed by AV, 13-Jun-2019.)
|- ℤring e. NrmRing
Theorem	remetdval 21398	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 21399	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 21400	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 )