P. 226 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22501-22600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tngtopn 22501	The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐷 = (dist‘𝑇)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopOpen‘𝑇))
Theorem	tngnm 22502	The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶𝐴) → 𝑁 = (norm‘𝑇))
Theorem	tngngp2 22503	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 22504*	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 22505*	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 22506	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 22507*	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 22508	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 22509	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 22510	The induced metric of a normed group is a function. (Contributed by AV, 19-Oct-2021.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐷 = (dist‘𝑇)    ⇒   ⊢ (𝐺 ∈ NrmGrp → 𝐷:(𝑋 × 𝑋)⟶ℝ)
Theorem	isnrg 22511	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 22512	The norm of a normed ring is an absolute value. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑁 = (norm‘𝑅)    &   ⊢ 𝐴 = (AbsVal‘𝑅)    ⇒   ⊢ (𝑅 ∈ NrmRing → 𝑁 ∈ 𝐴)
Theorem	nrgngp 22513	A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)
Theorem	nrgring 22514	A normed ring is a ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring)
Theorem	nmmul 22515	The norm of a product in a normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 · 𝐵)) = ((𝑁‘𝐴) · (𝑁‘𝐵)))
Theorem	nrgdsdi 22516	Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝑁‘𝐴) · (𝐵𝐷𝐶)) = ((𝐴 · 𝐵)𝐷(𝐴 · 𝐶)))
Theorem	nrgdsdir 22517	Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵) · (𝑁‘𝐶)) = ((𝐴 · 𝐶)𝐷(𝐵 · 𝐶)))
Theorem	nm1 22518	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 22519	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 22520	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 22521	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 22522	A nonzero normed ring is a domain. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → (𝑅 ∈ Domn ↔ 𝑅 ∈ NzRing))
Theorem	nrgtgp 22523	A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopGrp)
Theorem	subrgnrg 22524	A normed ring restricted to a subring is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    ⇒   ⊢ ((𝐺 ∈ NrmRing ∧ 𝐴 ∈ (SubRing‘𝐺)) → 𝐻 ∈ NrmRing)
Theorem	tngnrg 22525	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 22526*	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 22527	Defining property of a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐴 = (norm‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑁‘(𝑋 · 𝑌)) = ((𝐴‘𝑋) · (𝑁‘𝑌)))
Theorem	nlmngp 22528	A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp)
Theorem	nlmlmod 22529	A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod)
Theorem	nlmnrg 22530	The scalar component of a left module is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmRing)
Theorem	nlmngp2 22531	The scalar component of a left module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp)
Theorem	nlmdsdi 22532	Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐴 = (norm‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝐴‘𝑋) · (𝑌𝐷𝑍)) = ((𝑋 · 𝑌)𝐷(𝑋 · 𝑍)))
Theorem	nlmdsdir 22533	Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝐸 = (dist‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉)) → ((𝑋𝐸𝑌) · (𝑁‘𝑍)) = ((𝑋 · 𝑍)𝐷(𝑌 · 𝑍)))
Theorem	nlmmul0or 22534	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 22535	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 22536	Lemma for nlmvscn 22538. Compare this proof with the similar elementary proof mulcn2 14370 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 22537*	Lemma for nlmvscn 22538. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐸 = (dist‘𝐹)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝐴 = (norm‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1))    &   ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇))    &   ⊢ (𝜑 → 𝑊 ∈ NrmMod)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅))
Theorem	nlmvscn 22538	The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 22541 and nlmtlm 22545. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·sf ‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐾 = (TopOpen‘𝐹)    ⇒   ⊢ (𝑊 ∈ NrmMod → · ∈ ((𝐾 ×t 𝐽) Cn 𝐽))
Theorem	rlmnlm 22539	The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → (ringLMod‘𝑅) ∈ NrmMod)
Theorem	rlmnm 22540	The norm function in the ring module. (Contributed by AV, 9-Oct-2021.)
⊢ (norm‘𝑅) = (norm‘(ringLMod‘𝑅))
Theorem	nrgtrg 22541	A normed ring is a topological ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopRing)
Theorem	nrginvrcnlem 22542*	Lemma for nrginvrcn 22543. Compare this proof with reccn2 14371, 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 22543	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 22544	A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ TopDRing)
Theorem	nlmtlm 22545	A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ TopMod)
Theorem	isnvc 22546	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 22547	A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod)
Theorem	nvclvec 22548	A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LVec)
Theorem	nvclmod 22549	A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LMod)
Theorem	isnvc2 22550	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 22551	A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ TopVec)
Theorem	lssnlm 22552	A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmMod)
Theorem	lssnvc 22553	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 22554	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 22555	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 22556	The operator norm function.
class normOp
Syntax	cnghm 22557	The class of normed group homomorphisms.
class NGHom
Syntax	cnmhm 22558	The class of normed module homomorphisms.
class NMHom
Definition	df-nmo 22559*	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 22560*	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 22561*	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 𝑡)))
Theorem	nmoffn 22562	The function producing operator norm functions is a function on normed groups. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.)
⊢ normOp Fn (NrmGrp × NrmGrp)
Theorem	reldmnghm 22563	Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ Rel dom NGHom
Theorem	reldmnmhm 22564	Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ Rel dom NMHom
Theorem	nmofval 22565*	Value of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 26-Sep-2020.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → 𝑁 = (𝑓 ∈ (𝑆 GrpHom 𝑇) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ 𝑉 (𝑀‘(𝑓‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥))}, ℝ*, < )))
Theorem	nmoval 22566*	Value of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 26-Sep-2020.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝑁‘𝐹) = inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ 𝑉 (𝑀‘(𝐹‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥))}, ℝ*, < ))
Theorem	nmogelb 22567*	Property of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    ⇒   ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝐴 ∈ ℝ*) → (𝐴 ≤ (𝑁‘𝐹) ↔ ∀𝑟 ∈ (0[,)+∞)(∀𝑥 ∈ 𝑉 (𝑀‘(𝐹‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥)) → 𝐴 ≤ 𝑟)))
Theorem	nmolb 22568*	Any upper bound on the values of a linear operator translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    ⇒   ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (∀𝑥 ∈ 𝑉 (𝑀‘(𝐹‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) → (𝑁‘𝐹) ≤ 𝐴))
Theorem	nmolb2d 22569*	Any upper bound on the values of a linear operator at nonzero vectors translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ NrmGrp)    &   ⊢ (𝜑 → 𝑇 ∈ NrmGrp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → (𝑀‘(𝐹‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)))    ⇒   ⊢ (𝜑 → (𝑁‘𝐹) ≤ 𝐴)
Theorem	nmof 22570	The operator norm is a function into the extended reals. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → 𝑁:(𝑆 GrpHom 𝑇)⟶ℝ*)
Theorem	nmocl 22571	The operator norm of an operator is an extended real. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝑁‘𝐹) ∈ ℝ*)
Theorem	nmoge0 22572	The operator norm of an operator is nonnegative. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → 0 ≤ (𝑁‘𝐹))
Theorem	nghmfval 22573	A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (𝑆 NGHom 𝑇) = (◡𝑁 “ ℝ)
Theorem	isnghm 22574	A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑁‘𝐹) ∈ ℝ)))
Theorem	isnghm2 22575	A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ (𝑁‘𝐹) ∈ ℝ))
Theorem	isnghm3 22576	A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ (𝑁‘𝐹) < +∞))
Theorem	bddnghm 22577	A bounded group homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝐴 ∈ ℝ ∧ (𝑁‘𝐹) ≤ 𝐴)) → 𝐹 ∈ (𝑆 NGHom 𝑇))
Theorem	nghmcl 22578	A normed group homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → (𝑁‘𝐹) ∈ ℝ)
Theorem	nmoi 22579	The operator norm achieves the minimum of the set of upper bounds, if the operator is bounded. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) · (𝐿‘𝑋)))
Theorem	nmoix 22580	The operator norm is a bound on the size of an operator, even when it is infinite (using extended real multiplication). (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    ⇒   ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) ·e (𝐿‘𝑋)))
Theorem	nmoi2 22581	The operator norm is a bound on the growth of a vector under the action of the operator. (Contributed by Mario Carneiro, 19-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    ⇒   ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 )) → ((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ≤ (𝑁‘𝐹))
Theorem	nmoleub 22582*	The operator norm, defined as an infimum of upper bounds, can also be defined as a supremum of norms of 𝐹(𝑥) away from zero. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ NrmGrp)    &   ⊢ (𝜑 → 𝑇 ∈ NrmGrp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 (𝑥 ≠ 0 → ((𝑀‘(𝐹‘𝑥)) / (𝐿‘𝑥)) ≤ 𝐴)))
Theorem	nghmrcl1 22583	Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑆 ∈ NrmGrp)
Theorem	nghmrcl2 22584	Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑇 ∈ NrmGrp)
Theorem	nghmghm 22585	A normed group homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	nmo0 22586	The operator norm of the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑁‘(𝑉 × { 0 })) = 0)
Theorem	nmoeq0 22587	The operator norm is zero only for the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → ((𝑁‘𝐹) = 0 ↔ 𝐹 = (𝑉 × { 0 })))
Theorem	nmoco 22588	An upper bound on the operator norm of a composition. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑈)    &   ⊢ 𝐿 = (𝑇 normOp 𝑈)    &   ⊢ 𝑀 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘ 𝐺)) ≤ ((𝐿‘𝐹) · (𝑀‘𝐺)))
Theorem	nghmco 22589	The composition of normed group homomorphisms is a normed group homomorphism. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NGHom 𝑈))
Theorem	nmotri 22590	Triangle inequality for the operator norm. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ + = (+g‘𝑇)    ⇒   ⊢ ((𝑇 ∈ Abel ∧ 𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘𝑓 + 𝐺)) ≤ ((𝑁‘𝐹) + (𝑁‘𝐺)))
Theorem	nghmplusg 22591	The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ + = (+g‘𝑇)    ⇒   ⊢ ((𝑇 ∈ Abel ∧ 𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝐹 ∘𝑓 + 𝐺) ∈ (𝑆 NGHom 𝑇))
Theorem	0nghm 22592	The zero operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑉 × { 0 }) ∈ (𝑆 NGHom 𝑇))
Theorem	nmoid 22593	The operator norm of the identity function on a nontrivial group. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑆)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉) → (𝑁‘( I ↾ 𝑉)) = 1)
Theorem	idnghm 22594	The identity operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑉 = (Base‘𝑆)    ⇒   ⊢ (𝑆 ∈ NrmGrp → ( I ↾ 𝑉) ∈ (𝑆 NGHom 𝑆))
Theorem	nmods 22595	Upper bound for the distance between the values of a bounded linear operator. (Contributed by Mario Carneiro, 22-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐶 = (dist‘𝑆)    &   ⊢ 𝐷 = (dist‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐹‘𝐴)𝐷(𝐹‘𝐵)) ≤ ((𝑁‘𝐹) · (𝐴𝐶𝐵)))
Theorem	nghmcn 22596	A normed group homomorphism is a continuous function. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝐾 = (TopOpen‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	isnmhm 22597	A normed module homomorphism is a left module homomorphism which is also a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod) ∧ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇))))
Theorem	nmhmrcl1 22598	Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑆 ∈ NrmMod)
Theorem	nmhmrcl2 22599	Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑇 ∈ NrmMod)
Theorem	nmhmlmhm 22600	A normed module homomorphism is a left module homomorphism (a linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 LMHom 𝑇))