P. 225 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22401-22500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isngp2 22401	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 22402*	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 22403	A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( G e. NrmGrp -> G e. Grp )
Theorem	ngpms 22404	A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( G e. NrmGrp -> G e. MetSp )
Theorem	ngpxms 22405	A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( G e. NrmGrp -> G e. *MetSp )
Theorem	ngptps 22406	A normed group is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- ( G e. NrmGrp -> G e. TopSp )
Theorem	ngpmet 22407	The (induced) metric of a normed group is a metric. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by AV, 14-Oct-2021.)
|- X = ( Base ` G )   &    |- D = ( ( dist ` G ) |` ( X X. X ) )   =>    |- ( G e. NrmGrp -> D e. ( Met ` X ) )
Theorem	ngpds 22408	Value of the distance function in terms of the norm of a normed group. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 28-Nov-2006.) (Revised 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 22409	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 22410	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 22411	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 22412	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 22413	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 22414	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 22415	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 22416*	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 22417	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 22418	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 22419	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 22420	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 22421	The norm of a normed group is nonnegative. Second part of Problem 2 of [Kreyszig] p. 64. (Contributed by NM, 28-Nov-2006.) (Revised by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X ) -> 0 <_ ( N ` A ) )
Theorem	nmeq0 22422	The identity is the only element of the group with zero norm. First part of Problem 2 of [Kreyszig] p. 64. (Contributed by NM, 24-Nov-2006.) (Revised 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 22423	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 22424	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 22425	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 22426	The triangle inequality for the norm of a subtraction. (Contributed by NM, 27-Dec-2007.) (Revised 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 22427	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 22428	Reverse triangle inequality for the norm of a subtraction. Problem 3 of [Kreyszig] p. 64. (Contributed by NM, 4-Dec-2006.) (Revised 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 22429	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 22430	The triangle inequality for the norm of a sum. (Contributed by NM, 11-Nov-2006.) (Revised 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	nmtri2 22431	Triangle inequality for the norm of two subtractions. (Contributed by NM, 24-Feb-2008.) (Revised by AV, 8-Oct-2021.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( N ` ( A .- C ) ) <_ ( ( N ` ( A .- B ) ) + ( N ` ( B .- C ) ) ) )
Theorem	ngpi 22432*	The properties of a normed group, which is a group accompanied by a norm. (Contributed by AV, 7-Oct-2021.)
|- V = ( Base ` W )   &    |- N = ( norm ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( W e. NrmGrp -> ( W e. Grp /\ N : V --> RR /\ A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )
Theorem	nm0 22433	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	nmgt0 22434	The norm of a nonzero element is a positive real. (Contributed by NM, 20-Nov-2007.) (Revised by AV, 8-Oct-2021.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. NrmGrp /\ A e. X ) -> ( A =/= .0. <-> 0 < ( N ` A ) ) )
Theorem	sgrim 22435	The induced metric on a subgroup is the induced metric on the parent group equipped with a norm. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 19-Oct-2021.)
|- X = ( T ↾s U )   &    |- D = ( dist ` T )   &    |- E = ( dist ` X )   =>    |- ( U e. S -> E = D )
Theorem	sgrimval 22436	The induced metric on a subgroup in terms of the induced metric on the parent normed group. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 19-Oct-2021.)
|- X = ( T ↾s U )   &    |- D = ( dist ` T )   &    |- E = ( dist ` X )   &    |- T = ( G toNrmGrp N )   &    |- N = ( norm ` G )   &    |- S = (SubGrp ` T )   =>    |- ( ( ( G e. NrmGrp /\ U e. S ) /\ ( A e. U /\ B e. U ) ) -> ( A E B ) = ( A D B ) )
Theorem	subgnm 22437	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 22438	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 22439	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 22440	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 22441*	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 22442	The function toNrmGrp is a two-argument function. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- Rel dom toNrmGrp
Theorem	tngval 22443	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 22444	Lemma for tngbas 22445 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 22445	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 22446	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 22447	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 22448	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 22449	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 22450	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 22451	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 22452	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 22453	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 22454	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 22455	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 22456	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 22457*	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 22458*	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	tnggrpr 22459	If a structure equipped with a norm is a normed group, the structure itself must be a group. (Contributed by AV, 15-Oct-2021.)
|- T = ( G toNrmGrp N )   =>    |- ( ( N e. V /\ T e. NrmGrp ) -> G e. Grp )
Theorem	tngngp3 22460*	Alternate definition of a normed group (i.e. a group equipped with a norm) without using the properties of a metric space. This corresponds to the definition in N. H. Bingham, A. J. Ostaszewski: "Normed versus topological groups: dichotomy and duality", 2010, Dissertationes Mathematicae 472, pp. 1-138 and E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006. (Contributed by AV, 16-Oct-2021.)
|- T = ( G toNrmGrp N )   &    |- X = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- I = ( invg ` G )   =>    |- ( N : X --> RR -> ( T e. NrmGrp <-> ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) )
Theorem	nrmtngdist 22461	The augmentation of a normed group by its own norm has the same distance function as the normed group (restricted to the base set). (Contributed by AV, 15-Oct-2021.)
|- T = ( G toNrmGrp ( norm ` G ) )   &    |- X = ( Base ` G )   =>    |- ( G e. NrmGrp -> ( dist ` T ) = ( ( dist ` G ) |` ( X X. X ) ) )
Theorem	nrmtngnrm 22462	The augmentation of a normed group by its own norm is a normed group with the same norm. (Contributed by AV, 15-Oct-2021.)
|- T = ( G toNrmGrp ( norm ` G ) )   =>    |- ( G e. NrmGrp -> ( T e. NrmGrp /\ ( norm ` T ) = ( norm ` G ) ) )
Theorem	tngngpim 22463	The induced metric of a normed group is a function. (Contributed by AV, 19-Oct-2021.)
|- T = ( G toNrmGrp N )   &    |- N = ( norm ` G )   &    |- X = ( Base ` G )   &    |- D = ( dist ` T )   =>    |- ( G e. NrmGrp -> D : ( X X. X ) --> RR )
Theorem	isnrg 22464	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 22465	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 22466	A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. NrmRing -> R e. NrmGrp )
Theorem	nrgring 22467	A normed ring is a ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. NrmRing -> R e. Ring )
Theorem	nmmul 22468	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 22469	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 22470	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 22471	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 22472	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 22473	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 22474	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 22475	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 22476	A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- ( R e. NrmRing -> R e. TopGrp )
Theorem	subrgnrg 22477	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 22478	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 22479*	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 22480	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 22481	A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmMod -> W e. NrmGrp )
Theorem	nlmlmod 22482	A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmMod -> W e. LMod )
Theorem	nlmnrg 22483	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 22484	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 22485	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 22486	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 22487	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 22488	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 22489	Lemma for nlmvscn 22491. Compare this proof with the similar elementary proof mulcn2 14326 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 22490*	Lemma for nlmvscn 22491. (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 22491	The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 22494 and nlmtlm 22498. (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 22492	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	rlmnm 22493	The norm function in the ring module. (Contributed by AV, 9-Oct-2021.)
|- ( norm ` R ) = ( norm ` (ringLMod ` R ) )
Theorem	nrgtrg 22494	A normed ring is a topological ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. NrmRing -> R e. TopRing )
Theorem	nrginvrcnlem 22495*	Lemma for nrginvrcn 22496. Compare this proof with reccn2 14327, 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 22496	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 22497	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 22498	A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( W e. NrmMod -> W e. TopMod )
Theorem	isnvc 22499	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 22500	A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( W e. NrmVec -> W e. NrmMod )