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	ngplcan 24601	Cancel left addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ (((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶 + 𝐴)𝐷(𝐶 + 𝐵)) = (𝐴𝐷𝐵))
Theorem	isngp4 24602*	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 24603	Two elements are the same distance apart as their inverses. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ (((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐼‘𝐴)𝐷(𝐼‘𝐵)) = (𝐴𝐷𝐵))
Theorem	ngpsubcan 24604	Cancel right subtraction inside a distance calculation. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴 − 𝐶)𝐷(𝐵 − 𝐶)) = (𝐴𝐷𝐵))
Theorem	nmf 24605	The norm on a normed group is a function into the reals. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmGrp → 𝑁:𝑋⟶ℝ)
Theorem	nmcl 24606	The norm of a normed group is closed in the reals. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ)
Theorem	nmge0 24607	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 24608	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 24609	The norm of a nonzero element is nonzero. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → (𝑁‘𝐴) ≠ 0)
Theorem	nmrpcl 24610	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 24611	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 24612	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 24613	The norm of the difference between two elements. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 − 𝐵)) = (𝑁‘(𝐵 − 𝐴)))
Theorem	nmrtri 24614	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 24615	Inequality for the difference of norms. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘𝐴) − (𝑁‘𝐵)) ≤ (𝑁‘(𝐴 − 𝐵)))
Theorem	nmtri 24616	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 24617	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 24618*	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 24619	Norm of the identity element. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmGrp → (𝑁‘ 0 ) = 0)
Theorem	nmgt0 24620	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 24621	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 24622	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 24623	The norm in a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑀 = (norm‘𝐻)    ⇒   ⊢ (𝐴 ∈ (SubGrp‘𝐺) → 𝑀 = (𝑁 ↾ 𝐴))
Theorem	subgnm2 24624	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 24625	A normed group restricted to a subgroup is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ NrmGrp)
Theorem	ngptgp 24626	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 24627*	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 24628	The function toNrmGrp is a two-argument function. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ Rel dom toNrmGrp
Theorem	tngval 24629	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 24630	Lemma for tngbas 24631 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	tngbas 24631	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	tngplusg 24632	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	tng0 24633	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 24634	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	tngsca 24635	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	tngvsca 24636	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	tngip 24637	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	tngds 24638	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	tngtset 24639	The topology generated by a normed structure. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐷 = (dist‘𝑇)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopSet‘𝑇))
Theorem	tngtopn 24640	The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐷 = (dist‘𝑇)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopOpen‘𝑇))
Theorem	tngnm 24641	The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶𝐴) → 𝑁 = (norm‘𝑇))
Theorem	tngngp2 24642	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 24643*	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 24644*	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 24645	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 24646*	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 24647	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 24648	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 24649	The induced metric of a normed group is a function. (Contributed by AV, 19-Oct-2021.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐷 = (dist‘𝑇)    ⇒   ⊢ (𝐺 ∈ NrmGrp → 𝐷:(𝑋 × 𝑋)⟶ℝ)
Theorem	isnrg 24650	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 24651	The norm of a normed ring is an absolute value. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑁 = (norm‘𝑅)    &   ⊢ 𝐴 = (AbsVal‘𝑅)    ⇒   ⊢ (𝑅 ∈ NrmRing → 𝑁 ∈ 𝐴)
Theorem	nrgngp 24652	A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)
Theorem	nrgring 24653	A normed ring is a ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring)
Theorem	nmmul 24654	The norm of a product in a normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 · 𝐵)) = ((𝑁‘𝐴) · (𝑁‘𝐵)))
Theorem	nrgdsdi 24655	Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝑁‘𝐴) · (𝐵𝐷𝐶)) = ((𝐴 · 𝐵)𝐷(𝐴 · 𝐶)))
Theorem	nrgdsdir 24656	Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵) · (𝑁‘𝐶)) = ((𝐴 · 𝐶)𝐷(𝐵 · 𝐶)))
Theorem	nm1 24657	The norm of one in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑁 = (norm‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) → (𝑁‘ 1 ) = 1)
Theorem	unitnmn0 24658	The norm of a unit is nonzero in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑁 = (norm‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈) → (𝑁‘𝐴) ≠ 0)
Theorem	nminvr 24659	The norm of an inverse in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑁 = (norm‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈) → (𝑁‘(𝐼‘𝐴)) = (1 / (𝑁‘𝐴)))
Theorem	nmdvr 24660	The norm of a division in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → (𝑁‘(𝐴 / 𝐵)) = ((𝑁‘𝐴) / (𝑁‘𝐵)))
Theorem	nrgdomn 24661	A nonzero normed ring is a domain. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → (𝑅 ∈ Domn ↔ 𝑅 ∈ NzRing))
Theorem	nrgtgp 24662	A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopGrp)
Theorem	subrgnrg 24663	A normed ring restricted to a subring is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    ⇒   ⊢ ((𝐺 ∈ NrmRing ∧ 𝐴 ∈ (SubRing‘𝐺)) → 𝐻 ∈ NrmRing)
Theorem	tngnrg 24664	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.)
⊢ 𝑇 = (𝑅 toNrmGrp 𝐹)    &   ⊢ 𝐴 = (AbsVal‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝑇 ∈ NrmRing)
Theorem	isnlm 24665*	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.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐴 = (norm‘𝐹)    ⇒   ⊢ (𝑊 ∈ NrmMod ↔ ((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 · 𝑦)) = ((𝐴‘𝑥) · (𝑁‘𝑦))))
Theorem	nmvs 24666	Defining property of a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐴 = (norm‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑁‘(𝑋 · 𝑌)) = ((𝐴‘𝑋) · (𝑁‘𝑌)))
Theorem	nlmngp 24667	A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp)
Theorem	nlmlmod 24668	A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod)
Theorem	nlmnrg 24669	The scalar component of a left module is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmRing)
Theorem	nlmngp2 24670	The scalar component of a left module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp)
Theorem	nlmdsdi 24671	Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐴 = (norm‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝐴‘𝑋) · (𝑌𝐷𝑍)) = ((𝑋 · 𝑌)𝐷(𝑋 · 𝑍)))
Theorem	nlmdsdir 24672	Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝐸 = (dist‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉)) → ((𝑋𝐸𝑌) · (𝑁‘𝑍)) = ((𝑋 · 𝑍)𝐷(𝑌 · 𝑍)))
Theorem	nlmmul0or 24673	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.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑂 = (0g‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉) → ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 𝑂 ∨ 𝐵 = 0 )))
Theorem	sranlm 24674	The subring algebra over a normed ring is a normed left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆)    ⇒   ⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → 𝐴 ∈ NrmMod)
Theorem	nlmvscnlem2 24675	Lemma for nlmvscn 24677. Compare this proof with the similar elementary proof mulcn2 15556 for continuity of multiplication on ℂ. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐸 = (dist‘𝐹)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝐴 = (norm‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1))    &   ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇))    &   ⊢ (𝜑 → 𝑊 ∈ NrmMod)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐵𝐸𝐶) < 𝑈)    &   ⊢ (𝜑 → (𝑋𝐷𝑌) < 𝑇)    ⇒   ⊢ (𝜑 → ((𝐵 · 𝑋)𝐷(𝐶 · 𝑌)) < 𝑅)
Theorem	nlmvscnlem1 24676*	Lemma for nlmvscn 24677. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐸 = (dist‘𝐹)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝐴 = (norm‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1))    &   ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇))    &   ⊢ (𝜑 → 𝑊 ∈ NrmMod)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅))
Theorem	nlmvscn 24677	The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 24680 and nlmtlm 24684. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·sf ‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐾 = (TopOpen‘𝐹)    ⇒   ⊢ (𝑊 ∈ NrmMod → · ∈ ((𝐾 ×t 𝐽) Cn 𝐽))
Theorem	rlmnlm 24678	The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → (ringLMod‘𝑅) ∈ NrmMod)
Theorem	rlmnm 24679	The norm function in the ring module. (Contributed by AV, 9-Oct-2021.)
⊢ (norm‘𝑅) = (norm‘(ringLMod‘𝑅))
Theorem	nrgtrg 24680	A normed ring is a topological ring. (Contributed by Mario Carneiro, 4-Oct-2015.) (Proof shortened by AV, 31-Oct-2024.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopRing)
Theorem	nrginvrcnlem 24681*	Lemma for nrginvrcn 24682. Compare this proof with reccn2 15557, the elementary proof of continuity of division. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ NrmRing)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ 𝑇 = (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑥 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))
Theorem	nrginvrcn 24682	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.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑅)    ⇒   ⊢ (𝑅 ∈ NrmRing → 𝐼 ∈ ((𝐽 ↾t 𝑈) Cn (𝐽 ↾t 𝑈)))
Theorem	nrgtdrg 24683	A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ TopDRing)
Theorem	nlmtlm 24684	A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ TopMod)
Theorem	isnvc 24685	A normed vector space is just a normed module which is algebraically a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec ↔ (𝑊 ∈ NrmMod ∧ 𝑊 ∈ LVec))
Theorem	nvcnlm 24686	A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod)
Theorem	nvclvec 24687	A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LVec)
Theorem	nvclmod 24688	A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LMod)
Theorem	isnvc2 24689	A normed vector space is just a normed module whose scalar ring is a division ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ NrmVec ↔ (𝑊 ∈ NrmMod ∧ 𝐹 ∈ DivRing))
Theorem	nvctvc 24690	A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ TopVec)
Theorem	lssnlm 24691	A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmMod)
Theorem	lssnvc 24692	A subspace of a normed vector space is a normed vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ NrmVec ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmVec)
Theorem	rlmnvc 24693	The ring module over a normed division ring is a normed vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → (ringLMod‘𝑅) ∈ NrmVec)
Theorem	ngpocelbl 24694	Membership of an off-center vector in a ball in a normed module. (Contributed by NM, 27-Dec-2007.) (Revised by AV, 14-Oct-2021.)
⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐷 = ((dist‘𝐺) ↾ (𝑋 × 𝑋))    ⇒   ⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ* ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑃 + 𝐴) ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑁‘𝐴) < 𝑅))
12.4.9  Normed space homomorphisms (bounded linear operators)
Syntax	cnmo 24695	The operator norm function.
class normOp
Syntax	cnghm 24696	The class of normed group homomorphisms.
class NGHom
Syntax	cnmhm 24697	The class of normed module homomorphisms.
class NMHom
Definition	df-nmo 24698*	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 ⟨𝑠, 𝑡⟩. Equivalent to the definition of linear operator norm in [AkhiezerGlazman] p. 39. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 25-Sep-2020.)
⊢ normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
Definition	df-nghm 24699*	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 = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (◡(𝑠 normOp 𝑡) “ ℝ))
Definition	df-nmhm 24700*	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 𝑐 such that... (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ NMHom = (𝑠 ∈ NrmMod, 𝑡 ∈ NrmMod ↦ ((𝑠 LMHom 𝑡) ∩ (𝑠 NGHom 𝑡)))