P. 211 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21001-21100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nmcl 21001	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 21002	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 21003	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 21004	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 21005	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 21006	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 21007	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 21008	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 21009	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 21010	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 21011	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 21012	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 21013	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 21014	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 21015	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 21016	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 21017*	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 21018	The function toNrmGrp is a two-argument function. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- Rel dom toNrmGrp
Theorem	tngval 21019	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 21020	Lemma for tngbas 21021 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 21021	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 21022	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 21023	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 21024	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 21025	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 21026	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 21027	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 21028	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 21029	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 21030	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 21031	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 21032	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 21033*	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 21034*	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 21035	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 21036	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 21037	A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. NrmRing -> R e. NrmGrp )
Theorem	nrgring 21038	A normed ring is a ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. NrmRing -> R e. Ring )
Theorem	nmmul 21039	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 21040	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 21041	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 21042	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 21043	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 21044	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 21045	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 21046	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 21047	A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- ( R e. NrmRing -> R e. TopGrp )
Theorem	subrgnrg 21048	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 21049	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 21050*	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 21051	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 21052	A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmMod -> W e. NrmGrp )
Theorem	nlmlmod 21053	A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmMod -> W e. LMod )
Theorem	nlmnrg 21054	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 21055	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 21056	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 21057	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 21058	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 21059	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 21060	Lemma for nlmvscn 21062. Compare this proof with the similar elementary proof mulcn2 13397 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 21061*	Lemma for nlmvscn 21062. (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 21062	The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 21064 and nlmtlm 21068. (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 21063	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 21064	A normed ring is a topological ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. NrmRing -> R e. TopRing )
Theorem	nrginvrcnlem 21065*	Lemma for nrginvrcn 21066. Compare this proof with reccn2 13398, 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 21066	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 21067	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 21068	A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( W e. NrmMod -> W e. TopMod )
Theorem	isnvc 21069	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 21070	A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. NrmMod )
Theorem	nvclvec 21071	A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. LVec )
Theorem	nvclmod 21072	A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. LMod )
Theorem	isnvc2 21073	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 21074	A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. TopVec )
Theorem	lssnlm 21075	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 21076	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 21077	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 21078	The operator norm function.
class normOp
Syntax	cnghm 21079	The class of normed group homomorphisms.
class NGHom
Syntax	cnmhm 21080	The class of normed module homomorphisms.
class NMHom
Definition	df-nmo 21081*	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 21082*	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 21083*	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 21084	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 21085	Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- Rel dom NGHom
Theorem	reldmnmhm 21086	Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
|- Rel dom NMHom
Theorem	nmofval 21087*	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 21088*	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 21089*	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 21090*	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 21091*	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 21092	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 21093	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 21094	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 21095	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 21096	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 21097	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 21098	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 21099	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 21100	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 )