P. 248 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24701-24800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tngngpim 24701	The induced metric of a normed group is a function. (Contributed by AV, 19-Oct-2021.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐷 = (dist‘𝑇)    ⇒   ⊢ (𝐺 ∈ NrmGrp → 𝐷:(𝑋 × 𝑋)⟶ℝ)
Theorem	isnrg 24702	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 24703	The norm of a normed ring is an absolute value. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑁 = (norm‘𝑅)    &   ⊢ 𝐴 = (AbsVal‘𝑅)    ⇒   ⊢ (𝑅 ∈ NrmRing → 𝑁 ∈ 𝐴)
Theorem	nrgngp 24704	A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)
Theorem	nrgring 24705	A normed ring is a ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring)
Theorem	nmmul 24706	The norm of a product in a normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 · 𝐵)) = ((𝑁‘𝐴) · (𝑁‘𝐵)))
Theorem	nrgdsdi 24707	Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝑁‘𝐴) · (𝐵𝐷𝐶)) = ((𝐴 · 𝐵)𝐷(𝐴 · 𝐶)))
Theorem	nrgdsdir 24708	Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵) · (𝑁‘𝐶)) = ((𝐴 · 𝐶)𝐷(𝐵 · 𝐶)))
Theorem	nm1 24709	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 24710	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 24711	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 24712	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 24713	A nonzero normed ring is a domain. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → (𝑅 ∈ Domn ↔ 𝑅 ∈ NzRing))
Theorem	nrgtgp 24714	A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopGrp)
Theorem	subrgnrg 24715	A normed ring restricted to a subring is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    ⇒   ⊢ ((𝐺 ∈ NrmRing ∧ 𝐴 ∈ (SubRing‘𝐺)) → 𝐻 ∈ NrmRing)
Theorem	tngnrg 24716	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 24717*	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 24718	Defining property of a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐴 = (norm‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑁‘(𝑋 · 𝑌)) = ((𝐴‘𝑋) · (𝑁‘𝑌)))
Theorem	nlmngp 24719	A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp)
Theorem	nlmlmod 24720	A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod)
Theorem	nlmnrg 24721	The scalar component of a left module is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmRing)
Theorem	nlmngp2 24722	The scalar component of a left module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp)
Theorem	nlmdsdi 24723	Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐴 = (norm‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝐴‘𝑋) · (𝑌𝐷𝑍)) = ((𝑋 · 𝑌)𝐷(𝑋 · 𝑍)))
Theorem	nlmdsdir 24724	Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝐸 = (dist‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉)) → ((𝑋𝐸𝑌) · (𝑁‘𝑍)) = ((𝑋 · 𝑍)𝐷(𝑌 · 𝑍)))
Theorem	nlmmul0or 24725	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 24726	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 24727	Lemma for nlmvscn 24729. Compare this proof with the similar elementary proof mulcn2 15642 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 24728*	Lemma for nlmvscn 24729. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐸 = (dist‘𝐹)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝐴 = (norm‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1))    &   ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇))    &   ⊢ (𝜑 → 𝑊 ∈ NrmMod)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅))
Theorem	nlmvscn 24729	The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 24732 and nlmtlm 24736. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·sf ‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐾 = (TopOpen‘𝐹)    ⇒   ⊢ (𝑊 ∈ NrmMod → · ∈ ((𝐾 ×t 𝐽) Cn 𝐽))
Theorem	rlmnlm 24730	The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → (ringLMod‘𝑅) ∈ NrmMod)
Theorem	rlmnm 24731	The norm function in the ring module. (Contributed by AV, 9-Oct-2021.)
⊢ (norm‘𝑅) = (norm‘(ringLMod‘𝑅))
Theorem	nrgtrg 24732	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 24733*	Lemma for nrginvrcn 24734. Compare this proof with reccn2 15643, 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 24734	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 24735	A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ TopDRing)
Theorem	nlmtlm 24736	A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ TopMod)
Theorem	isnvc 24737	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 24738	A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod)
Theorem	nvclvec 24739	A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LVec)
Theorem	nvclmod 24740	A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LMod)
Theorem	isnvc2 24741	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 24742	A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ TopVec)
Theorem	lssnlm 24743	A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmMod)
Theorem	lssnvc 24744	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 24745	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 24746	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 24747	The operator norm function.
class normOp
Syntax	cnghm 24748	The class of normed group homomorphisms.
class NGHom
Syntax	cnmhm 24749	The class of normed module homomorphisms.
class NMHom
Definition	df-nmo 24750*	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 24751*	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 24752*	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 24753	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 24754	Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ Rel dom NGHom
Theorem	reldmnmhm 24755	Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ Rel dom NMHom
Theorem	nmofval 24756*	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 24757*	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 24758*	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 24759*	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 24760*	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 24761	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 24762	The operator norm of an operator is an extended real. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝑁‘𝐹) ∈ ℝ*)
Theorem	nmoge0 24763	The operator norm of an operator is nonnegative. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → 0 ≤ (𝑁‘𝐹))
Theorem	nghmfval 24764	A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (𝑆 NGHom 𝑇) = (◡𝑁 “ ℝ)
Theorem	isnghm 24765	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 24766	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 24767	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 24768	A bounded group homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝐴 ∈ ℝ ∧ (𝑁‘𝐹) ≤ 𝐴)) → 𝐹 ∈ (𝑆 NGHom 𝑇))
Theorem	nghmcl 24769	A normed group homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → (𝑁‘𝐹) ∈ ℝ)
Theorem	nmoi 24770	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 24771	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 24772	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 24773*	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 24774	Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑆 ∈ NrmGrp)
Theorem	nghmrcl2 24775	Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑇 ∈ NrmGrp)
Theorem	nghmghm 24776	A normed group homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	nmo0 24777	The operator norm of the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑁‘(𝑉 × { 0 })) = 0)
Theorem	nmoeq0 24778	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 24779	An upper bound on the operator norm of a composition. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑈)    &   ⊢ 𝐿 = (𝑇 normOp 𝑈)    &   ⊢ 𝑀 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘ 𝐺)) ≤ ((𝐿‘𝐹) · (𝑀‘𝐺)))
Theorem	nghmco 24780	The composition of normed group homomorphisms is a normed group homomorphism. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NGHom 𝑈))
Theorem	nmotri 24781	Triangle inequality for the operator norm. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ + = (+g‘𝑇)    ⇒   ⊢ ((𝑇 ∈ Abel ∧ 𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘f + 𝐺)) ≤ ((𝑁‘𝐹) + (𝑁‘𝐺)))
Theorem	nghmplusg 24782	The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ + = (+g‘𝑇)    ⇒   ⊢ ((𝑇 ∈ Abel ∧ 𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝐹 ∘f + 𝐺) ∈ (𝑆 NGHom 𝑇))
Theorem	0nghm 24783	The zero operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑉 × { 0 }) ∈ (𝑆 NGHom 𝑇))
Theorem	nmoid 24784	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 24785	The identity operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑉 = (Base‘𝑆)    ⇒   ⊢ (𝑆 ∈ NrmGrp → ( I ↾ 𝑉) ∈ (𝑆 NGHom 𝑆))
Theorem	nmods 24786	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 24787	A normed group homomorphism is a continuous function. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝐾 = (TopOpen‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	isnmhm 24788	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 24789	Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑆 ∈ NrmMod)
Theorem	nmhmrcl2 24790	Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑇 ∈ NrmMod)
Theorem	nmhmlmhm 24791	A normed module homomorphism is a left module homomorphism (a linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 LMHom 𝑇))
Theorem	nmhmnghm 24792	A normed module homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 NGHom 𝑇))
Theorem	nmhmghm 24793	A normed module homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	isnmhm2 24794	A normed module homomorphism is a left module homomorphism with bounded norm (a bounded linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝑁‘𝐹) ∈ ℝ))
Theorem	nmhmcl 24795	A normed module homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → (𝑁‘𝐹) ∈ ℝ)
Theorem	idnmhm 24796	The identity operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑉 = (Base‘𝑆)    ⇒   ⊢ (𝑆 ∈ NrmMod → ( I ↾ 𝑉) ∈ (𝑆 NMHom 𝑆))
Theorem	0nmhm 24797	The zero operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐹 = (Scalar‘𝑆)    &   ⊢ 𝐺 = (Scalar‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 = 𝐺) → (𝑉 × { 0 }) ∈ (𝑆 NMHom 𝑇))
Theorem	nmhmco 24798	The composition of bounded linear operators is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ ((𝐹 ∈ (𝑇 NMHom 𝑈) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NMHom 𝑈))
Theorem	nmhmplusg 24799	The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ + = (+g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 NMHom 𝑇) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘f + 𝐺) ∈ (𝑆 NMHom 𝑇))
12.4.10  Topology on the reals
Theorem	qtopbaslem 24800	The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ 𝑆 ⊆ ℝ*    ⇒   ⊢ ((,) “ (𝑆 × 𝑆)) ∈ TopBases