P. 247 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24601-24700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dscopn 24601*	The discrete metric generates the discrete topology. In particular, the discrete topology is metrizable. (Contributed by Mario Carneiro, 29-Jan-2014.)
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if(𝑥 = 𝑦, 0, 1))    ⇒   ⊢ (𝑋 ∈ 𝑉 → (MetOpen‘𝐷) = 𝒫 𝑋)
Theorem	nrmmetd 24602*	Show that a group norm generates a metric. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 ))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → (𝐹 ∘ − ) ∈ (Met‘𝑋))
Theorem	abvmet 24603	An absolute value 𝐹 generates a metric defined by 𝑑(𝑥, 𝑦) = 𝐹(𝑥 − 𝑦), analogously to cnmet 24807. (In fact, the ring structure is not needed at all; the group properties abveq0 20835 and abvtri 20839, abvneg 20843 are sufficient.) (Contributed by Mario Carneiro, 9-Sep-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ − = (-g‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (𝐹 ∘ − ) ∈ (Met‘𝑋))
12.4.8  Normed algebraic structures In the following, the norm of a normed algebraic structure (group, left module, vector space) is defined by the (given) distance function (the norm 𝑁 of an element is its distance 𝐷 from the zero element, see nmval 24617: (𝑁‘𝐴) = (𝐴𝐷 0 )). By this definition, the norm function 𝑁 is actually a norm (satisfying the properties: being a function into the reals; subadditivity/triangle inequality (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)); absolute homogeneity ( n(sx) = |s| n(x) ) [Remark: for group norms, some authors (e.g., Juris Steprans in "A characterization of free abelian groups") demand that n(sx) = |s| n(x) for all 𝑠 ∈ ℤ, whereas other authors (e.g., N. H. Bingham and A. J. Ostaszewski in "Normed versus topological groups: Dichotomy and duality") only require inversion symmetry, i.e., (𝑁‘( − 𝑥) = 𝑁‘𝑥). The definition df-ngp 24611 of a group norm follows the second approach, see nminv 24649.] and positive definiteness/point-separation ((𝑁‘𝑥) = 0 ↔ 𝑥 = 0)) if the structure is a metric space with a right-translation-invariant metric (see nmf 24643, nmtri 24654, nmvs 24712 and nmeq0 24646). An alternate definition of a normed group (i.e., a group equipped with a norm) not using the properties of a metric space is given by Theorem tngngp3 24692. The norm can be expressed as the distance to zero (nmfval 24616), so in a structure with a zero (a "pointed set", for instance a monoid or a group), the norm can be expressed as the distance restricted to the elements of the base set to zero (nmfval0 24618). Usually, however, the norm of a normed structure is given, and the corresponding metric ("induced metric") is defined as the distance function based on the norm (the distance 𝐷 between two elements is the norm 𝑁 of their difference, see ngpds 24632: (𝐴𝐷𝐵) = (𝑁‘(𝐴 − 𝐵))). The operation toNrmGrp does exactly this, i.e., it adds a distance function (and a topology) to a structure (which should be at least a group for the difference of two elements to make sense) corresponding to a given norm as explained above: (dist‘𝑇) = (𝑁 ∘ − ), see also tngds 24683. By this, the enhanced structure becomes a normed structure if the induced metric is in fact a metric (see tngngp2 24688) or a norm (see tngngpd 24689). If the norm is derived from a given metric, as done with df-nm 24610, the induced metric is the original metric restricted to the base set: (dist‘𝑇) = ((dist‘𝐺) ↾ (𝑋 × 𝑋)), see nrmtngdist 24693, and the norm remains the same: (norm‘𝑇) = (norm‘𝐺), see nrmtngnrm 24694.
Syntax	cnm 24604	Norm of a normed ring.
class norm
Syntax	cngp 24605	The class of all normed groups.
class NrmGrp
Syntax	ctng 24606	Make a normed group from a norm and a group.
class toNrmGrp
Syntax	cnrg 24607	Normed ring.
class NrmRing
Syntax	cnlm 24608	Normed module.
class NrmMod
Syntax	cnvc 24609	Normed vector space.
class NrmVec
Definition	df-nm 24610*	Define the norm on a group or ring (when it makes sense) in terms of the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ norm = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤) ↦ (𝑥(dist‘𝑤)(0g‘𝑤))))
Definition	df-ngp 24611	Define a normed group, which is a group with a right-translation-invariant metric. This is not a standard notion, but is helpful as the most general context in which a metric-like norm makes sense. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ NrmGrp = {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)}
Definition	df-tng 24612*	Define a function that fills in the topology and metric components of a structure given a group and a norm on it. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ toNrmGrp = (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩))
Definition	df-nrg 24613	A normed ring is a ring with an induced topology and metric such that the metric is translation-invariant and the norm (distance from 0) is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ NrmRing = {𝑤 ∈ NrmGrp ∣ (norm‘𝑤) ∈ (AbsVal‘𝑤)}
Definition	df-nlm 24614*	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.)
⊢ NrmMod = {𝑤 ∈ (NrmGrp ∩ LMod) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))}
Definition	df-nvc 24615	A normed vector space is a normed module which is also a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ NrmVec = (NrmMod ∩ LVec)
Theorem	nmfval 24616*	The value of the norm function as the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐷 = (dist‘𝑊)    ⇒   ⊢ 𝑁 = (𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 ))
Theorem	nmval 24617	The value of the norm as the distance to zero. Problem 1 of [Kreyszig] p. 63. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐷 = (dist‘𝑊)    ⇒   ⊢ (𝐴 ∈ 𝑋 → (𝑁‘𝐴) = (𝐴𝐷 0 ))
Theorem	nmfval0 24618*	The value of the norm function on a structure containing a zero as the distance restricted to the elements of the base set to zero. Examples of structures containing a "zero" are groups (see nmfval2 24619 proved from this theorem and grpidcl 18995) or more generally monoids (see mndidcl 18774), or pointed sets). (Contributed by Mario Carneiro, 2-Oct-2015.) Extract this result from the proof of nmfval2 24619. (Revised by BJ, 27-Aug-2024.)
⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋))    ⇒   ⊢ ( 0 ∈ 𝑋 → 𝑁 = (𝑥 ∈ 𝑋 ↦ (𝑥𝐸 0 )))
Theorem	nmfval2 24619*	The value of the norm function on a group as the distance restricted to the elements of the base set to zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝑊 ∈ Grp → 𝑁 = (𝑥 ∈ 𝑋 ↦ (𝑥𝐸 0 )))
Theorem	nmval2 24620	The value of the norm on a group as the distance restricted to the elements of the base set to zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋))    ⇒   ⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (𝐴𝐸 0 ))
Theorem	nmf2 24621	The norm on a metric group is a function from the base set into the reals. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋))    ⇒   ⊢ ((𝑊 ∈ Grp ∧ 𝐸 ∈ (Met‘𝑋)) → 𝑁:𝑋⟶ℝ)
Theorem	nmpropd 24622	Weak property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (+g‘𝐾) = (+g‘𝐿))    &   ⊢ (𝜑 → (dist‘𝐾) = (dist‘𝐿))    ⇒   ⊢ (𝜑 → (norm‘𝐾) = (norm‘𝐿))
Theorem	nmpropd2 24623*	Strong property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐾 ∈ Grp)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → (norm‘𝐾) = (norm‘𝐿))
Theorem	isngp 24624	The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) ⊆ 𝐷))
Theorem	isngp2 24625	The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = 𝐸))
Theorem	isngp3 24626*	The property of being a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑁 = (norm‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦))))
Theorem	ngpgrp 24627	A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp)
Theorem	ngpms 24628	A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp)
Theorem	ngpxms 24629	A normed group is an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ ∞MetSp)
Theorem	ngptps 24630	A normed group is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ TopSp)
Theorem	ngpmet 24631	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.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐷 = ((dist‘𝐺) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝐺 ∈ NrmGrp → 𝐷 ∈ (Met‘𝑋))
Theorem	ngpds 24632	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.)
⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐴 − 𝐵)))
Theorem	ngpdsr 24633	Value of the distance function in terms of the norm of a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐵 − 𝐴)))
Theorem	ngpds2 24634	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = ((𝐴 − 𝐵)𝐷 0 ))
Theorem	ngpds2r 24635	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = ((𝐵 − 𝐴)𝐷 0 ))
Theorem	ngpds3 24636	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = ( 0 𝐷(𝐴 − 𝐵)))
Theorem	ngpds3r 24637	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = ( 0 𝐷(𝐵 − 𝐴)))
Theorem	ngprcan 24638	Cancel right addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐶)𝐷(𝐵 + 𝐶)) = (𝐴𝐷𝐵))
Theorem	ngplcan 24639	Cancel left addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ (((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶 + 𝐴)𝐷(𝐶 + 𝐵)) = (𝐴𝐷𝐵))
Theorem	isngp4 24640*	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.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦)))
Theorem	ngpinvds 24641	Two elements are the same distance apart as their inverses. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ (((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐼‘𝐴)𝐷(𝐼‘𝐵)) = (𝐴𝐷𝐵))
Theorem	ngpsubcan 24642	Cancel right subtraction inside a distance calculation. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴 − 𝐶)𝐷(𝐵 − 𝐶)) = (𝐴𝐷𝐵))
Theorem	nmf 24643	The norm on a normed group is a function into the reals. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmGrp → 𝑁:𝑋⟶ℝ)
Theorem	nmcl 24644	The norm of a normed group is closed in the reals. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ)
Theorem	nmge0 24645	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.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → 0 ≤ (𝑁‘𝐴))
Theorem	nmeq0 24646	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.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴) = 0 ↔ 𝐴 = 0 ))
Theorem	nmne0 24647	The norm of a nonzero element is nonzero. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → (𝑁‘𝐴) ≠ 0)
Theorem	nmrpcl 24648	The norm of a nonzero element is a positive real. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → (𝑁‘𝐴) ∈ ℝ+)
Theorem	nminv 24649	The norm of a negated element is the same as the norm of the original element. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝑁‘(𝐼‘𝐴)) = (𝑁‘𝐴))
Theorem	nmmtri 24650	The triangle inequality for the norm of a subtraction. (Contributed by NM, 27-Dec-2007.) (Revised by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 − 𝐵)) ≤ ((𝑁‘𝐴) + (𝑁‘𝐵)))
Theorem	nmsub 24651	The norm of the difference between two elements. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 − 𝐵)) = (𝑁‘(𝐵 − 𝐴)))
Theorem	nmrtri 24652	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.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (abs‘((𝑁‘𝐴) − (𝑁‘𝐵))) ≤ (𝑁‘(𝐴 − 𝐵)))
Theorem	nm2dif 24653	Inequality for the difference of norms. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘𝐴) − (𝑁‘𝐵)) ≤ (𝑁‘(𝐴 − 𝐵)))
Theorem	nmtri 24654	The triangle inequality for the norm of a sum. (Contributed by NM, 11-Nov-2006.) (Revised by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 + 𝐵)) ≤ ((𝑁‘𝐴) + (𝑁‘𝐵)))
Theorem	nmtri2 24655	Triangle inequality for the norm of two subtractions. (Contributed by NM, 24-Feb-2008.) (Revised by AV, 8-Oct-2021.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝑁‘(𝐴 − 𝐶)) ≤ ((𝑁‘(𝐴 − 𝐵)) + (𝑁‘(𝐵 − 𝐶))))
Theorem	ngpi 24656*	The properties of a normed group, which is a group accompanied by a norm. (Contributed by AV, 7-Oct-2021.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ (𝑊 ∈ NrmGrp → (𝑊 ∈ Grp ∧ 𝑁:𝑉⟶ℝ ∧ ∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))))
Theorem	nm0 24657	Norm of the identity element. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmGrp → (𝑁‘ 0 ) = 0)
Theorem	nmgt0 24658	The norm of a nonzero element is a positive real. (Contributed by NM, 20-Nov-2007.) (Revised by AV, 8-Oct-2021.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ≠ 0 ↔ 0 < (𝑁‘𝐴)))
Theorem	sgrim 24659	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.)
⊢ 𝑋 = (𝑇 ↾s 𝑈)    &   ⊢ 𝐷 = (dist‘𝑇)    &   ⊢ 𝐸 = (dist‘𝑋)    ⇒   ⊢ (𝑈 ∈ 𝑆 → 𝐸 = 𝐷)
Theorem	sgrimval 24660	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.)
⊢ 𝑋 = (𝑇 ↾s 𝑈)    &   ⊢ 𝐷 = (dist‘𝑇)    &   ⊢ 𝐸 = (dist‘𝑋)    &   ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑆 = (SubGrp‘𝑇)    ⇒   ⊢ (((𝐺 ∈ NrmGrp ∧ 𝑈 ∈ 𝑆) ∧ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈)) → (𝐴𝐸𝐵) = (𝐴𝐷𝐵))
Theorem	subgnm 24661	The norm in a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑀 = (norm‘𝐻)    ⇒   ⊢ (𝐴 ∈ (SubGrp‘𝐺) → 𝑀 = (𝑁 ↾ 𝐴))
Theorem	subgnm2 24662	A substructure assigns the same values to the norms of elements of a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑀 = (norm‘𝐻)    ⇒   ⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝐴) → (𝑀‘𝑋) = (𝑁‘𝑋))
Theorem	subgngp 24663	A normed group restricted to a subgroup is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ NrmGrp)
Theorem	ngptgp 24664	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.)
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) → 𝐺 ∈ TopGrp)
Theorem	ngppropd 24665*	Property deduction for a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵)))    &   ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))    ⇒   ⊢ (𝜑 → (𝐾 ∈ NrmGrp ↔ 𝐿 ∈ NrmGrp))
Theorem	reldmtng 24666	The function toNrmGrp is a two-argument function. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ Rel dom toNrmGrp
Theorem	tngval 24667	Value of the function which augments a given structure 𝐺 with a norm 𝑁. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (𝑁 ∘ − )    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝑇 = ((𝐺 sSet ⟨(dist‘ndx), 𝐷⟩) sSet ⟨(TopSet‘ndx), 𝐽⟩))
Theorem	tnglem 24668	Lemma for tngbas 24670 and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (TopSet‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (dist‘ndx)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐸‘𝐺) = (𝐸‘𝑇))
Theorem	tnglemOLD 24669	Obsolete version of tnglem 24668 as of 31-Oct-2024. Lemma for tngbas 24670 and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐸 = Slot 𝐾    &   ⊢ 𝐾 ∈ ℕ    &   ⊢ 𝐾 < 9    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐸‘𝐺) = (𝐸‘𝑇))
Theorem	tngbas 24670	The base set of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝐵 = (Base‘𝑇))
Theorem	tngbasOLD 24671	Obsolete version of tngbas 24670 as of 31-Oct-2024. The base set of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝐵 = (Base‘𝑇))
Theorem	tngplusg 24672	The group addition of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → + = (+g‘𝑇))
Theorem	tngplusgOLD 24673	Obsolete version of tngplusg 24672 as of 31-Oct-2024. The group addition of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → + = (+g‘𝑇))
Theorem	tng0 24674	The group identity of a structure augmented with a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by AV, 31-Oct-2024.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → 0 = (0g‘𝑇))
Theorem	tngmulr 24675	The ring multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ · = (.r‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → · = (.r‘𝑇))
Theorem	tngmulrOLD 24676	Obsolete version of tngmulr 24675 as of 31-Oct-2024. The ring multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ · = (.r‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → · = (.r‘𝑇))
Theorem	tngsca 24677	The scalar ring of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐹 = (Scalar‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝐹 = (Scalar‘𝑇))
Theorem	tngscaOLD 24678	Obsolete version of tngsca 24677 as of 31-Oct-2024. The scalar ring of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐹 = (Scalar‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝐹 = (Scalar‘𝑇))
Theorem	tngvsca 24679	The scalar multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ · = ( ·𝑠 ‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → · = ( ·𝑠 ‘𝑇))
Theorem	tngvscaOLD 24680	Obsolete version of tngvsca 24679 as of 31-Oct-2024. The scalar multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ · = ( ·𝑠 ‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → · = ( ·𝑠 ‘𝑇))
Theorem	tngip 24681	The inner product operation of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ , = (·𝑖‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → , = (·𝑖‘𝑇))
Theorem	tngipOLD 24682	Obsolete version of tngip 24681 as of 31-Oct-2024. The inner product operation of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ , = (·𝑖‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → , = (·𝑖‘𝑇))
Theorem	tngds 24683	The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015.) (Proof shortened by AV, 29-Oct-2024.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝑁 ∘ − ) = (dist‘𝑇))
Theorem	tngdsOLD 24684	Obsolete version of tngds 24683 as of 29-Oct-2024. The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝑁 ∘ − ) = (dist‘𝑇))
Theorem	tngtset 24685	The topology generated by a normed structure. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐷 = (dist‘𝑇)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopSet‘𝑇))
Theorem	tngtopn 24686	The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐷 = (dist‘𝑇)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopOpen‘𝑇))
Theorem	tngnm 24687	The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶𝐴) → 𝑁 = (norm‘𝑇))
Theorem	tngngp2 24688	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.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐷 = (dist‘𝑇)    ⇒   ⊢ (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))))
Theorem	tngngpd 24689*	Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑁:𝑋⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))    ⇒   ⊢ (𝜑 → 𝑇 ∈ NrmGrp)
Theorem	tngngp 24690*	Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))))
Theorem	tnggrpr 24691	If a structure equipped with a norm is a normed group, the structure itself must be a group. (Contributed by AV, 15-Oct-2021.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑇 ∈ NrmGrp) → 𝐺 ∈ Grp)
Theorem	tngngp3 24692*	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.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))))
Theorem	nrmtngdist 24693	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.)
⊢ 𝑇 = (𝐺 toNrmGrp (norm‘𝐺))    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmGrp → (dist‘𝑇) = ((dist‘𝐺) ↾ (𝑋 × 𝑋)))
Theorem	nrmtngnrm 24694	The augmentation of a normed group by its own norm is a normed group with the same norm. (Contributed by AV, 15-Oct-2021.)
⊢ 𝑇 = (𝐺 toNrmGrp (norm‘𝐺))    ⇒   ⊢ (𝐺 ∈ NrmGrp → (𝑇 ∈ NrmGrp ∧ (norm‘𝑇) = (norm‘𝐺)))
Theorem	tngngpim 24695	The induced metric of a normed group is a function. (Contributed by AV, 19-Oct-2021.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐷 = (dist‘𝑇)    ⇒   ⊢ (𝐺 ∈ NrmGrp → 𝐷:(𝑋 × 𝑋)⟶ℝ)
Theorem	isnrg 24696	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.)
⊢ 𝑁 = (norm‘𝑅)    &   ⊢ 𝐴 = (AbsVal‘𝑅)    ⇒   ⊢ (𝑅 ∈ NrmRing ↔ (𝑅 ∈ NrmGrp ∧ 𝑁 ∈ 𝐴))
Theorem	nrgabv 24697	The norm of a normed ring is an absolute value. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑁 = (norm‘𝑅)    &   ⊢ 𝐴 = (AbsVal‘𝑅)    ⇒   ⊢ (𝑅 ∈ NrmRing → 𝑁 ∈ 𝐴)
Theorem	nrgngp 24698	A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)
Theorem	nrgring 24699	A normed ring is a ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring)
Theorem	nmmul 24700	The norm of a product in a normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 · 𝐵)) = ((𝑁‘𝐴) · (𝑁‘𝐵)))