P. 217 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21601-21700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nmfval 21601*	The value of the norm function. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` W )   &    |- X = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- D = ( dist ` W )   =>    |- N = ( x e. X |-> ( x D .0. ) )
Theorem	nmval 21602	The value of the norm function. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` W )   &    |- X = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- D = ( dist ` W )   =>    |- ( A e. X -> ( N ` A ) = ( A D .0. ) )
Theorem	nmfval2 21603*	The value of the norm function using a restricted metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` W )   &    |- X = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- D = ( dist ` W )   &    |- E = ( D |` ( X X. X ) )   =>    |- ( W e. Grp -> N = ( x e. X |-> ( x E .0. ) ) )
Theorem	nmval2 21604	The value of the norm function using a restricted metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` W )   &    |- X = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- D = ( dist ` W )   &    |- E = ( D |` ( X X. X ) )   =>    |- ( ( W e. Grp /\ A e. X ) -> ( N ` A ) = ( A E .0. ) )
Theorem	nmf2 21605	The norm is a function from the base set into the reals. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` W )   &    |- X = ( Base ` W )   &    |- D = ( dist ` W )   &    |- E = ( D |` ( X X. X ) )   =>    |- ( ( W e. Grp /\ E e. ( Met ` X ) ) -> N : X --> RR )
Theorem	nmpropd 21606	Weak property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> ( Base ` K ) = ( Base ` L ) )   &    |- ( ph -> ( +g ` K ) = ( +g ` L ) )   &    |- ( ph -> ( dist ` K ) = ( dist ` L ) )   =>    |- ( ph -> ( norm ` K ) = ( norm ` L ) )
Theorem	nmpropd2 21607*	Strong property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> K e. Grp )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )   =>    |- ( ph -> ( norm ` K ) = ( norm ` L ) )
Theorem	isngp 21608	The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) C_ D ) )
Theorem	isngp2 21609	The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   &    |- X = ( Base ` G )   &    |- E = ( D |` ( X X. X ) )   =>    |- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) = E ) )
Theorem	isngp3 21610*	The property of being a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- N = ( norm ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   &    |- X = ( Base ` G )   =>    |- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ A. x e. X A. y e. X ( x D y ) = ( N ` ( x .- y ) ) ) )
Theorem	ngpgrp 21611	A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( G e. NrmGrp -> G e. Grp )
Theorem	ngpms 21612	A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( G e. NrmGrp -> G e. MetSp )
Theorem	ngpxms 21613	A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( G e. NrmGrp -> G e. *MetSp )
Theorem	ngptps 21614	A normed group is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- ( G e. NrmGrp -> G e. TopSp )
Theorem	ngpds 21615	Value of the distance function in terms of the norm of a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` G )   &    |- X = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A .- B ) ) )
Theorem	ngpdsr 21616	Value of the distance function in terms of the norm of a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` G )   &    |- X = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( B .- A ) ) )
Theorem	ngpds2 21617	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( ( A .- B ) D .0. ) )
Theorem	ngpds2r 21618	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( ( B .- A ) D .0. ) )
Theorem	ngpds3 21619	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( .0. D ( A .- B ) ) )
Theorem	ngpds3r 21620	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( .0. D ( B .- A ) ) )
Theorem	ngprcan 21621	Cancel right addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A .+ C ) D ( B .+ C ) ) = ( A D B ) )
Theorem	ngplcan 21622	Cancel left addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( C .+ A ) D ( C .+ B ) ) = ( A D B ) )
Theorem	isngp4 21623*	Express the property of being a normed group purely in terms of right-translation invariance of the metric instead of using the definition of norm (which itself uses the metric). (Contributed by Mario Carneiro, 29-Oct-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- D = ( dist ` G )   =>    |- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ A. x e. X A. y e. X A. z e. X ( ( x .+ z ) D ( y .+ z ) ) = ( x D y ) ) )
Theorem	ngpinvds 21624	Two elements are the same distance apart as their inverses. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- I = ( invg ` G )   &    |- D = ( dist ` G )   =>    |- ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( A e. X /\ B e. X ) ) -> ( ( I ` A ) D ( I ` B ) ) = ( A D B ) )
Theorem	ngpsubcan 21625	Cancel right subtraction inside a distance calculation. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A .- C ) D ( B .- C ) ) = ( A D B ) )
Theorem	nmf 21626	The norm on a normed group is a function into the reals. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   =>    |- ( G e. NrmGrp -> N : X --> RR )
Theorem	nmcl 21627	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 21628	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 21629	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 21630	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 21631	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 21632	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 21633	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 21634	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 21635	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 21636	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 21637	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 21638	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 21639	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 21640	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 21641	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 21642	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 21643*	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 21644	The function toNrmGrp is a two-argument function. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- Rel dom toNrmGrp
Theorem	tngval 21645	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 21646	Lemma for tngbas 21647 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 21647	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 21648	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 21649	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 21650	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 21651	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 21652	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 21653	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 21654	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 21655	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 21656	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 21657	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 21658	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 21659*	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 21660*	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 21661	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 21662	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 21663	A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. NrmRing -> R e. NrmGrp )
Theorem	nrgring 21664	A normed ring is a ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. NrmRing -> R e. Ring )
Theorem	nmmul 21665	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 21666	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 21667	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 21668	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 21669	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 21670	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 21671	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 21672	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 21673	A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- ( R e. NrmRing -> R e. TopGrp )
Theorem	subrgnrg 21674	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 21675	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 21676*	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 21677	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 21678	A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmMod -> W e. NrmGrp )
Theorem	nlmlmod 21679	A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmMod -> W e. LMod )
Theorem	nlmnrg 21680	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 21681	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 21682	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 21683	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 21684	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 21685	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 21686	Lemma for nlmvscn 21688. Compare this proof with the similar elementary proof mulcn2 13658 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 21687*	Lemma for nlmvscn 21688. (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 21688	The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 21690 and nlmtlm 21694. (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 21689	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 21690	A normed ring is a topological ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. NrmRing -> R e. TopRing )
Theorem	nrginvrcnlem 21691*	Lemma for nrginvrcn 21692. Compare this proof with reccn2 13659, 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 21692	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 21693	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 21694	A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( W e. NrmMod -> W e. TopMod )
Theorem	isnvc 21695	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 21696	A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. NrmMod )
Theorem	nvclvec 21697	A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. LVec )
Theorem	nvclmod 21698	A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. LMod )
Theorem	isnvc2 21699	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 21700	A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. TopVec )