P. 238 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23701-23800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tngval 23701	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 23702	Lemma for tngbas 23704 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 23703	Obsolete version of tnglem 23702 as of 31-Oct-2024. Lemma for tngbas 23704 and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐸 = Slot 𝐾    &   ⊢ 𝐾 ∈ ℕ    &   ⊢ 𝐾 < 9    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐸‘𝐺) = (𝐸‘𝑇))
Theorem	tngbas 23704	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 23705	Obsolete proof of tngbas 23704 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 23706	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 23707	Obsolete proof of tngplusg 23706 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 23708	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 23709	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 23710	Obsolete proof of tngmulr 23709 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 23711	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 23712	Obsolete proof of tngsca 23711 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 23713	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 23714	Obsolete proof of tngvsca 23713 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 23715	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 23716	Obsolete proof of tngip 23715 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 23717	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 23718	Obsolete proof of tngds 23717 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 23719	The topology generated by a normed structure. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐷 = (dist‘𝑇)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopSet‘𝑇))
Theorem	tngtopn 23720	The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐷 = (dist‘𝑇)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopOpen‘𝑇))
Theorem	tngnm 23721	The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶𝐴) → 𝑁 = (norm‘𝑇))
Theorem	tngngp2 23722	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 23723*	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 23724*	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 23725	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 23726*	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 23727	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 23728	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 23729	The induced metric of a normed group is a function. (Contributed by AV, 19-Oct-2021.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐷 = (dist‘𝑇)    ⇒   ⊢ (𝐺 ∈ NrmGrp → 𝐷:(𝑋 × 𝑋)⟶ℝ)
Theorem	isnrg 23730	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 23731	The norm of a normed ring is an absolute value. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑁 = (norm‘𝑅)    &   ⊢ 𝐴 = (AbsVal‘𝑅)    ⇒   ⊢ (𝑅 ∈ NrmRing → 𝑁 ∈ 𝐴)
Theorem	nrgngp 23732	A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)
Theorem	nrgring 23733	A normed ring is a ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring)
Theorem	nmmul 23734	The norm of a product in a normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 · 𝐵)) = ((𝑁‘𝐴) · (𝑁‘𝐵)))
Theorem	nrgdsdi 23735	Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝑁‘𝐴) · (𝐵𝐷𝐶)) = ((𝐴 · 𝐵)𝐷(𝐴 · 𝐶)))
Theorem	nrgdsdir 23736	Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵) · (𝑁‘𝐶)) = ((𝐴 · 𝐶)𝐷(𝐵 · 𝐶)))
Theorem	nm1 23737	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 23738	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 23739	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 23740	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 23741	A nonzero normed ring is a domain. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → (𝑅 ∈ Domn ↔ 𝑅 ∈ NzRing))
Theorem	nrgtgp 23742	A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopGrp)
Theorem	subrgnrg 23743	A normed ring restricted to a subring is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    ⇒   ⊢ ((𝐺 ∈ NrmRing ∧ 𝐴 ∈ (SubRing‘𝐺)) → 𝐻 ∈ NrmRing)
Theorem	tngnrg 23744	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 23745*	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 23746	Defining property of a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐴 = (norm‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑁‘(𝑋 · 𝑌)) = ((𝐴‘𝑋) · (𝑁‘𝑌)))
Theorem	nlmngp 23747	A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp)
Theorem	nlmlmod 23748	A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod)
Theorem	nlmnrg 23749	The scalar component of a left module is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmRing)
Theorem	nlmngp2 23750	The scalar component of a left module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp)
Theorem	nlmdsdi 23751	Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐴 = (norm‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝐴‘𝑋) · (𝑌𝐷𝑍)) = ((𝑋 · 𝑌)𝐷(𝑋 · 𝑍)))
Theorem	nlmdsdir 23752	Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝐸 = (dist‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉)) → ((𝑋𝐸𝑌) · (𝑁‘𝑍)) = ((𝑋 · 𝑍)𝐷(𝑌 · 𝑍)))
Theorem	nlmmul0or 23753	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 23754	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 23755	Lemma for nlmvscn 23757. Compare this proof with the similar elementary proof mulcn2 15233 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 23756*	Lemma for nlmvscn 23757. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐸 = (dist‘𝐹)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝐴 = (norm‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1))    &   ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇))    &   ⊢ (𝜑 → 𝑊 ∈ NrmMod)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅))
Theorem	nlmvscn 23757	The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 23760 and nlmtlm 23764. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·sf ‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐾 = (TopOpen‘𝐹)    ⇒   ⊢ (𝑊 ∈ NrmMod → · ∈ ((𝐾 ×t 𝐽) Cn 𝐽))
Theorem	rlmnlm 23758	The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → (ringLMod‘𝑅) ∈ NrmMod)
Theorem	rlmnm 23759	The norm function in the ring module. (Contributed by AV, 9-Oct-2021.)
⊢ (norm‘𝑅) = (norm‘(ringLMod‘𝑅))
Theorem	nrgtrg 23760	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 23761*	Lemma for nrginvrcn 23762. Compare this proof with reccn2 15234, 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 23762	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 23763	A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ TopDRing)
Theorem	nlmtlm 23764	A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ TopMod)
Theorem	isnvc 23765	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 23766	A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod)
Theorem	nvclvec 23767	A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LVec)
Theorem	nvclmod 23768	A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LMod)
Theorem	isnvc2 23769	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 23770	A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ TopVec)
Theorem	lssnlm 23771	A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmMod)
Theorem	lssnvc 23772	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 23773	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 23774	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 23775	The operator norm function.
class normOp
Syntax	cnghm 23776	The class of normed group homomorphisms.
class NGHom
Syntax	cnmhm 23777	The class of normed module homomorphisms.
class NMHom
Definition	df-nmo 23778*	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 23779*	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 23780*	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 23781	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 23782	Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ Rel dom NGHom
Theorem	reldmnmhm 23783	Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ Rel dom NMHom
Theorem	nmofval 23784*	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 23785*	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 23786*	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 23787*	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 23788*	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 23789	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 23790	The operator norm of an operator is an extended real. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝑁‘𝐹) ∈ ℝ*)
Theorem	nmoge0 23791	The operator norm of an operator is nonnegative. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → 0 ≤ (𝑁‘𝐹))
Theorem	nghmfval 23792	A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (𝑆 NGHom 𝑇) = (◡𝑁 “ ℝ)
Theorem	isnghm 23793	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 23794	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 23795	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 23796	A bounded group homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝐴 ∈ ℝ ∧ (𝑁‘𝐹) ≤ 𝐴)) → 𝐹 ∈ (𝑆 NGHom 𝑇))
Theorem	nghmcl 23797	A normed group homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → (𝑁‘𝐹) ∈ ℝ)
Theorem	nmoi 23798	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 23799	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 23800	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 )) → ((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ≤ (𝑁‘𝐹))