P. 210 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	tngngp2 20901	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 20902*	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 20903*	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 20904	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 20905	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 )
Theorem	nrgngp 20906	A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. NrmRing -> R e. NrmGrp )
Theorem	nrgrng 20907	A normed ring is a ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. NrmRing -> R e. Ring )
Theorem	nmmul 20908	The norm of a product in a normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- X = ( Base ` R )   &    |- N = ( norm ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. NrmRing /\ A e. X /\ B e. X ) -> ( N ` ( A .x. B ) ) = ( ( N ` A ) x. ( N ` B ) ) )
Theorem	nrgdsdi 20909	Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- X = ( Base ` R )   &    |- N = ( norm ` R )   &    |- .x. = ( .r ` R )   &    |- D = ( dist ` R )   =>    |- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( N ` A ) x. ( B D C ) ) = ( ( A .x. B ) D ( A .x. C ) ) )
Theorem	nrgdsdir 20910	Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- X = ( Base ` R )   &    |- N = ( norm ` R )   &    |- .x. = ( .r ` R )   &    |- D = ( dist ` R )   =>    |- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D B ) x. ( N ` C ) ) = ( ( A .x. C ) D ( B .x. C ) ) )
Theorem	nm1 20911	The norm of one in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- N = ( norm ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. NrmRing /\ R e. NzRing ) -> ( N ` .1. ) = 1 )
Theorem	unitnmn0 20912	The norm of a unit is nonzero in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- N = ( norm ` R )   &    |- U = (Unit ` R )   =>    |- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` A ) =/= 0 )
Theorem	nminvr 20913	The norm of an inverse in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- N = ( norm ` R )   &    |- U = (Unit ` R )   &    |- I = ( invr ` R )   =>    |- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` ( I ` A ) ) = ( 1 / ( N ` A ) ) )
Theorem	nmdvr 20914	The norm of a division in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- X = ( Base ` R )   &    |- N = ( norm ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   =>    |- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` ( A ./ B ) ) = ( ( N ` A ) / ( N ` B ) ) )
Theorem	nrgdomn 20915	A nonzero normed ring is a domain. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. NrmRing -> ( R e. Domn <-> R e. NzRing ) )
Theorem	nrgtgp 20916	A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- ( R e. NrmRing -> R e. TopGrp )
Theorem	subrgnrg 20917	A normed ring restricted to a subring is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- H = ( G ↾s A )   =>    |- ( ( G e. NrmRing /\ A e. (SubRing ` G ) ) -> H e. NrmRing )
Theorem	tngnrg 20918	Given any absolute value over a ring, augmenting the ring with the absolute value produces a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- T = ( R toNrmGrp F )   &    |- A = (AbsVal ` R )   =>    |- ( F e. A -> T e. NrmRing )
Theorem	isnlm 20919*	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.)
|- V = ( Base ` W )   &    |- N = ( norm ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- A = ( norm ` F )   =>    |- ( W e. NrmMod <-> ( ( W e. NrmGrp /\ W e. LMod /\ F e. NrmRing ) /\ A. x e. K A. y e. V ( N ` ( x .x. y ) ) = ( ( A ` x ) x. ( N ` y ) ) ) )
Theorem	nmvs 20920	Defining property of a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- V = ( Base ` W )   &    |- N = ( norm ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- A = ( norm ` F )   =>    |- ( ( W e. NrmMod /\ X e. K /\ Y e. V ) -> ( N ` ( X .x. Y ) ) = ( ( A ` X ) x. ( N ` Y ) ) )
Theorem	nlmngp 20921	A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmMod -> W e. NrmGrp )
Theorem	nlmlmod 20922	A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmMod -> W e. LMod )
Theorem	nlmnrg 20923	The scalar component of a left module is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. NrmMod -> F e. NrmRing )
Theorem	nlmngp2 20924	The scalar component of a left module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. NrmMod -> F e. NrmGrp )
Theorem	nlmdsdi 20925	Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- D = ( dist ` W )   &    |- A = ( norm ` F )   =>    |- ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> ( ( A ` X ) x. ( Y D Z ) ) = ( ( X .x. Y ) D ( X .x. Z ) ) )
Theorem	nlmdsdir 20926	Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- D = ( dist ` W )   &    |- N = ( norm ` W )   &    |- E = ( dist ` F )   =>    |- ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> ( ( X E Y ) x. ( N ` Z ) ) = ( ( X .x. Z ) D ( Y .x. Z ) ) )
Theorem	nlmmul0or 20927	If a scalar product is zero, one of its factors must be zero. (Contributed by NM, 6-Dec-2007.) (Revised by Mario Carneiro, 4-Oct-2015.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- O = ( 0g ` F )   =>    |- ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( ( A .x. B ) = .0. <-> ( A = O \/ B = .0. ) ) )
Theorem	sranlm 20928	The subring algebra over a normed ring is a normed left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- A = ( (subringAlg ` W ) ` S )   =>    |- ( ( W e. NrmRing /\ S e. (SubRing ` W ) ) -> A e. NrmMod )
Theorem	nlmvscnlem2 20929	Lemma for nlmvscn 20931. Compare this proof with the similar elementary proof mulcn2 13377 for continuity of multiplication on CC. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- F = (Scalar ` W )   &    |- V = ( Base ` W )   &    |- K = ( Base ` F )   &    |- D = ( dist ` W )   &    |- E = ( dist ` F )   &    |- N = ( norm ` W )   &    |- A = ( norm ` F )   &    |- .x. = ( .s ` W )   &    |- T = ( ( R / 2 ) / ( ( A ` B ) + 1 ) )   &    |- U = ( ( R / 2 ) / ( ( N ` X ) + T ) )   &    |- ( ph -> W e. NrmMod )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> B e. K )   &    |- ( ph -> X e. V )   &    |- ( ph -> C e. K )   &    |- ( ph -> Y e. V )   &    |- ( ph -> ( B E C ) < U )   &    |- ( ph -> ( X D Y ) < T )   =>    |- ( ph -> ( ( B .x. X ) D ( C .x. Y ) ) < R )
Theorem	nlmvscnlem1 20930*	Lemma for nlmvscn 20931. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- F = (Scalar ` W )   &    |- V = ( Base ` W )   &    |- K = ( Base ` F )   &    |- D = ( dist ` W )   &    |- E = ( dist ` F )   &    |- N = ( norm ` W )   &    |- A = ( norm ` F )   &    |- .x. = ( .s ` W )   &    |- T = ( ( R / 2 ) / ( ( A ` B ) + 1 ) )   &    |- U = ( ( R / 2 ) / ( ( N ` X ) + T ) )   &    |- ( ph -> W e. NrmMod )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> B e. K )   &    |- ( ph -> X e. V )   =>    |- ( ph -> E. r e. RR+ A. x e. K A. y e. V ( ( ( B E x ) < r /\ ( X D y ) < r ) -> ( ( B .x. X ) D ( x .x. y ) ) < R ) )
Theorem	nlmvscn 20931	The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 20933 and nlmtlm 20937. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- F = (Scalar ` W )   &    |- .x. = ( .sf ` W )   &    |- J = ( TopOpen ` W )   &    |- K = ( TopOpen ` F )   =>    |- ( W e. NrmMod -> .x. e. ( ( K tX J ) Cn J ) )
Theorem	rlmnlm 20932	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 20933	A normed ring is a topological ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. NrmRing -> R e. TopRing )
Theorem	nrginvrcnlem 20934*	Lemma for nrginvrcn 20935. Compare this proof with reccn2 13378, 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 20935	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 20936	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 20937	A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( W e. NrmMod -> W e. TopMod )
Theorem	isnvc 20938	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 20939	A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. NrmMod )
Theorem	nvclvec 20940	A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. LVec )
Theorem	nvclmod 20941	A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. LMod )
Theorem	isnvc2 20942	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 20943	A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. TopVec )
Theorem	lssnlm 20944	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 20945	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 20946	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 20947	The operator norm function.
class normOp
Syntax	cnghm 20948	The class of normed group homomorphisms.
class NGHom
Syntax	cnmhm 20949	The class of normed module homomorphisms.
class NMHom
Definition	df-nmo 20950*	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 20951*	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 20952*	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 20953	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 20954	Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- Rel dom NGHom
Theorem	reldmnmhm 20955	Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- Rel dom NMHom
Theorem	nmofval 20956*	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 20957*	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 20958*	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 20959*	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 20960*	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 20961	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 20962	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 20963	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 20964	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 20965	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 20966	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 20967	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 20968	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 20969	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 20970	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 20971	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 20972	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 20973*	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 20974	Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NGHom T ) -> S e. NrmGrp )
Theorem	nghmrcl2 20975	Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NGHom T ) -> T e. NrmGrp )
Theorem	nghmghm 20976	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 20977	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 20978	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 20979	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 20980	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 20981	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 20982	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 20983	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 20984	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 20985	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 20986	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 20987	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 20988	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 20989	Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NMHom T ) -> S e. NrmMod )
Theorem	nmhmrcl2 20990	Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- ( F e. ( S NMHom T ) -> T e. NrmMod )
Theorem	nmhmlmhm 20991	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 20992	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 20993	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 20994	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 20995	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 20996	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 20997	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 20998	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 20999	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 21000	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