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	ngptgp 24601	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 24602*	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 24603	The function toNrmGrp is a two-argument function. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ Rel dom toNrmGrp
Theorem	tngval 24604	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 24605	Lemma for tngbas 24606 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 24606	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 24607	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 24608	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 24609	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 24610	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 24611	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 24612	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 24613	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 24614	The topology generated by a normed structure. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐷 = (dist‘𝑇)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopSet‘𝑇))
Theorem	tngtopn 24615	The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝐷 = (dist‘𝑇)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopOpen‘𝑇))
Theorem	tngnm 24616	The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶𝐴) → 𝑁 = (norm‘𝑇))
Theorem	tngngp2 24617	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 24618*	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 24619*	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 24620	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 24621*	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 24622	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 24623	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 24624	The induced metric of a normed group is a function. (Contributed by AV, 19-Oct-2021.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐷 = (dist‘𝑇)    ⇒   ⊢ (𝐺 ∈ NrmGrp → 𝐷:(𝑋 × 𝑋)⟶ℝ)
Theorem	isnrg 24625	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 24626	The norm of a normed ring is an absolute value. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑁 = (norm‘𝑅)    &   ⊢ 𝐴 = (AbsVal‘𝑅)    ⇒   ⊢ (𝑅 ∈ NrmRing → 𝑁 ∈ 𝐴)
Theorem	nrgngp 24627	A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)
Theorem	nrgring 24628	A normed ring is a ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring)
Theorem	nmmul 24629	The norm of a product in a normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 · 𝐵)) = ((𝑁‘𝐴) · (𝑁‘𝐵)))
Theorem	nrgdsdi 24630	Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝑁‘𝐴) · (𝐵𝐷𝐶)) = ((𝐴 · 𝐵)𝐷(𝐴 · 𝐶)))
Theorem	nrgdsdir 24631	Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵) · (𝑁‘𝐶)) = ((𝐴 · 𝐶)𝐷(𝐵 · 𝐶)))
Theorem	nm1 24632	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 24633	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 24634	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 24635	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 24636	A nonzero normed ring is a domain. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → (𝑅 ∈ Domn ↔ 𝑅 ∈ NzRing))
Theorem	nrgtgp 24637	A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopGrp)
Theorem	subrgnrg 24638	A normed ring restricted to a subring is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    ⇒   ⊢ ((𝐺 ∈ NrmRing ∧ 𝐴 ∈ (SubRing‘𝐺)) → 𝐻 ∈ NrmRing)
Theorem	tngnrg 24639	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 24640*	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 24641	Defining property of a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐴 = (norm‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑁‘(𝑋 · 𝑌)) = ((𝐴‘𝑋) · (𝑁‘𝑌)))
Theorem	nlmngp 24642	A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp)
Theorem	nlmlmod 24643	A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod)
Theorem	nlmnrg 24644	The scalar component of a left module is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmRing)
Theorem	nlmngp2 24645	The scalar component of a left module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp)
Theorem	nlmdsdi 24646	Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐴 = (norm‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝐴‘𝑋) · (𝑌𝐷𝑍)) = ((𝑋 · 𝑌)𝐷(𝑋 · 𝑍)))
Theorem	nlmdsdir 24647	Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝐸 = (dist‘𝐹)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉)) → ((𝑋𝐸𝑌) · (𝑁‘𝑍)) = ((𝑋 · 𝑍)𝐷(𝑌 · 𝑍)))
Theorem	nlmmul0or 24648	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 24649	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 24650	Lemma for nlmvscn 24652. Compare this proof with the similar elementary proof mulcn2 15558 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 24651*	Lemma for nlmvscn 24652. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐸 = (dist‘𝐹)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝐴 = (norm‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1))    &   ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇))    &   ⊢ (𝜑 → 𝑊 ∈ NrmMod)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅))
Theorem	nlmvscn 24652	The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 24655 and nlmtlm 24659. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·sf ‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐾 = (TopOpen‘𝐹)    ⇒   ⊢ (𝑊 ∈ NrmMod → · ∈ ((𝐾 ×t 𝐽) Cn 𝐽))
Theorem	rlmnlm 24653	The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑅 ∈ NrmRing → (ringLMod‘𝑅) ∈ NrmMod)
Theorem	rlmnm 24654	The norm function in the ring module. (Contributed by AV, 9-Oct-2021.)
⊢ (norm‘𝑅) = (norm‘(ringLMod‘𝑅))
Theorem	nrgtrg 24655	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 24656*	Lemma for nrginvrcn 24657. Compare this proof with reccn2 15559, 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 24657	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 24658	A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ TopDRing)
Theorem	nlmtlm 24659	A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ TopMod)
Theorem	isnvc 24660	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 24661	A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod)
Theorem	nvclvec 24662	A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LVec)
Theorem	nvclmod 24663	A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LMod)
Theorem	isnvc2 24664	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 24665	A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ TopVec)
Theorem	lssnlm 24666	A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmMod)
Theorem	lssnvc 24667	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 24668	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 24669	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 24670	The operator norm function.
class normOp
Syntax	cnghm 24671	The class of normed group homomorphisms.
class NGHom
Syntax	cnmhm 24672	The class of normed module homomorphisms.
class NMHom
Definition	df-nmo 24673*	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 24674*	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 24675*	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 24676	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 24677	Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ Rel dom NGHom
Theorem	reldmnmhm 24678	Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ Rel dom NMHom
Theorem	nmofval 24679*	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 24680*	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 24681*	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 24682*	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 24683*	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 24684	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 24685	The operator norm of an operator is an extended real. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝑁‘𝐹) ∈ ℝ*)
Theorem	nmoge0 24686	The operator norm of an operator is nonnegative. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → 0 ≤ (𝑁‘𝐹))
Theorem	nghmfval 24687	A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (𝑆 NGHom 𝑇) = (◡𝑁 “ ℝ)
Theorem	isnghm 24688	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 24689	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 24690	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 24691	A bounded group homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝐴 ∈ ℝ ∧ (𝑁‘𝐹) ≤ 𝐴)) → 𝐹 ∈ (𝑆 NGHom 𝑇))
Theorem	nghmcl 24692	A normed group homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → (𝑁‘𝐹) ∈ ℝ)
Theorem	nmoi 24693	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 24694	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 24695	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 24696*	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 24697	Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑆 ∈ NrmGrp)
Theorem	nghmrcl2 24698	Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑇 ∈ NrmGrp)
Theorem	nghmghm 24699	A normed group homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	nmo0 24700	The operator norm of the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑁‘(𝑉 × { 0 })) = 0)