P. 245 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24401-24500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	comet 24401*	The composition of an extended metric with a monotonic subadditive function is an extended metric. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐹:(0[,]+∞)⟶ℝ*)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞)) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐷) ∈ (∞Met‘𝑋))
Theorem	stdbdmetval 24402*	Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = if((𝐴𝐶𝐵) ≤ 𝑅, (𝐴𝐶𝐵), 𝑅))
Theorem	stdbdxmet 24403*	The standard bounded metric is an extended metric given an extended metric and a positive extended real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝐷 ∈ (∞Met‘𝑋))
Theorem	stdbdmet 24404*	The standard bounded metric is a proper metric given an extended metric and a positive real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ+) → 𝐷 ∈ (Met‘𝑋))
Theorem	stdbdbl 24405*	The standard bounded metric corresponding to 𝐶 generates the same balls as 𝐶 for radii less than 𝑅. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))    ⇒   ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ* ∧ 𝑆 ≤ 𝑅)) → (𝑃(ball‘𝐷)𝑆) = (𝑃(ball‘𝐶)𝑆))
Theorem	stdbdmopn 24406*	The standard bounded metric corresponding to 𝐶 generates the same topology as 𝐶. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))    &   ⊢ 𝐽 = (MetOpen‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝐽 = (MetOpen‘𝐷))
Theorem	mopnex 24407*	The topology generated by an extended metric can also be generated by a true metric. Thus, "metrizable topologies" can equivalently be defined in terms of metrics or extended metrics. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∃𝑑 ∈ (Met‘𝑋)𝐽 = (MetOpen‘𝑑))
Theorem	methaus 24408	The topology generated by a metric space is Hausdorff. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus)
Theorem	met1stc 24409	The topology generated by a metric space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ 1stω)
Theorem	met2ndci 24410	A separable metric space (a metric space with a countable dense subset) is second-countable. (Contributed by Mario Carneiro, 13-Apr-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ 2ndω)
Theorem	met2ndc 24411*	A metric space is second-countable iff it is separable (has a countable dense subset). (Contributed by Mario Carneiro, 13-Apr-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐽 ∈ 2ndω ↔ ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋)))
Theorem	metrest 24412	Two alternate formulations of a subspace topology of a metric space topology. (Contributed by Jeff Hankins, 19-Aug-2009.) (Proof shortened by Mario Carneiro, 5-Jan-2014.)
⊢ 𝐷 = (𝐶 ↾ (𝑌 × 𝑌))    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾t 𝑌) = 𝐾)
Theorem	ressxms 24413	The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ ∞MetSp)
Theorem	ressms 24414	The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ MetSp)
Theorem	prdsmslem1 24415	Lemma for prdsms 24419. The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅:𝐼⟶MetSp)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵))
Theorem	prdsxmslem1 24416	Lemma for prdsms 24419. The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅:𝐼⟶∞MetSp)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵))
Theorem	prdsxmslem2 24417*	Lemma for prdsxms 24418. The topology generated by the supremum metric is the same as the product topology, when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅:𝐼⟶∞MetSp)    &   ⊢ 𝐽 = (TopOpen‘𝑌)    &   ⊢ 𝑉 = (Base‘(𝑅‘𝑘))    &   ⊢ 𝐸 = ((dist‘(𝑅‘𝑘)) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐾 = (TopOpen‘(𝑅‘𝑘))    &   ⊢ 𝐶 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))}    ⇒   ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷))
Theorem	prdsxms 24418	The indexed product structure is an extended metric space when the index set is finite. (Although the extended metric is still valid when the index set is infinite, it no longer agrees with the product topology, which is not metrizable in any case.) (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    ⇒   ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶∞MetSp) → 𝑌 ∈ ∞MetSp)
Theorem	prdsms 24419	The indexed product structure is a metric space when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    ⇒   ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶MetSp) → 𝑌 ∈ MetSp)
Theorem	pwsxms 24420	A power of an extended metric space is an extended metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ ∞MetSp ∧ 𝐼 ∈ Fin) → 𝑌 ∈ ∞MetSp)
Theorem	pwsms 24421	A power of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ MetSp ∧ 𝐼 ∈ Fin) → 𝑌 ∈ MetSp)
Theorem	xpsxms 24422	A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    ⇒   ⊢ ((𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp) → 𝑇 ∈ ∞MetSp)
Theorem	xpsms 24423	A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    ⇒   ⊢ ((𝑅 ∈ MetSp ∧ 𝑆 ∈ MetSp) → 𝑇 ∈ MetSp)
Theorem	tmsxps 24424	Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁)))    &   ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌))    ⇒   ⊢ (𝜑 → 𝑃 ∈ (∞Met‘(𝑋 × 𝑌)))
Theorem	tmsxpsmopn 24425	Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁)))    &   ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌))    &   ⊢ 𝐽 = (MetOpen‘𝑀)    &   ⊢ 𝐾 = (MetOpen‘𝑁)    &   ⊢ 𝐿 = (MetOpen‘𝑃)    ⇒   ⊢ (𝜑 → 𝐿 = (𝐽 ×t 𝐾))
Theorem	tmsxpsval 24426	Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁)))    &   ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩𝑃⟨𝐶, 𝐷⟩) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
Theorem	tmsxpsval2 24427	Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁)))    &   ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩𝑃⟨𝐶, 𝐷⟩) = if((𝐴𝑀𝐶) ≤ (𝐵𝑁𝐷), (𝐵𝑁𝐷), (𝐴𝑀𝐶)))
12.4.5  Continuity in metric spaces
Theorem	metcnp3 24428*	Two ways to express that 𝐹 is continuous at 𝑃 for metric spaces. Proposition 14-4.2 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ (𝐹 “ (𝑃(ball‘𝐶)𝑧)) ⊆ ((𝐹‘𝑃)(ball‘𝐷)𝑦))))
Theorem	metcnp 24429*	Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous at point 𝑃. (Contributed by NM, 11-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝑋 ((𝑃𝐶𝑤) < 𝑧 → ((𝐹‘𝑃)𝐷(𝐹‘𝑤)) < 𝑦))))
Theorem	metcnp2 24430*	Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous at point 𝑃. The distance arguments are swapped compared to metcnp 24429 (and Munkres' metcn 24431) for compatibility with df-lm 23116. Definition 1.3-3 of [Kreyszig] p. 20. (Contributed by NM, 4-Jun-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝑋 ((𝑤𝐶𝑃) < 𝑧 → ((𝐹‘𝑤)𝐷(𝐹‘𝑃)) < 𝑦))))
Theorem	metcn 24431*	Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous. Theorem 10.1 of [Munkres] p. 127. The second biconditional argument says that for every positive "epsilon" 𝑦 there is a positive "delta" 𝑧 such that a distance less than delta in 𝐶 maps to a distance less than epsilon in 𝐷. (Contributed by NM, 15-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝐹‘𝑥)𝐷(𝐹‘𝑤)) < 𝑦))))
Theorem	metcnpi 24432*	Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 24429. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑋 ((𝑃𝐶𝑦) < 𝑥 → ((𝐹‘𝑃)𝐷(𝐹‘𝑦)) < 𝐴))
Theorem	metcnpi2 24433*	Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 24430. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) < 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) < 𝐴))
Theorem	metcnpi3 24434*	Epsilon-delta property of a metric space function continuous at 𝑃. A variation of metcnpi2 24433 with non-strict ordering. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) ≤ 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) ≤ 𝐴))
Theorem	txmetcnp 24435*	Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    &   ⊢ 𝐿 = (MetOpen‘𝐸)    ⇒   ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝐸 ∈ (∞Met‘𝑍)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐹 ∈ (((𝐽 ×t 𝐾) CnP 𝐿)‘⟨𝐴, 𝐵⟩) ↔ (𝐹:(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑧 ∈ ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((𝐴𝐶𝑢) < 𝑤 ∧ (𝐵𝐷𝑣) < 𝑤) → ((𝐴𝐹𝐵)𝐸(𝑢𝐹𝑣)) < 𝑧))))
Theorem	txmetcn 24436*	Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    &   ⊢ 𝐿 = (MetOpen‘𝐸)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝐸 ∈ (∞Met‘𝑍)) → (𝐹 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↔ (𝐹:(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ∀𝑧 ∈ ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((𝑥𝐶𝑢) < 𝑤 ∧ (𝑦𝐷𝑣) < 𝑤) → ((𝑥𝐹𝑦)𝐸(𝑢𝐹𝑣)) < 𝑧))))
12.4.6  The uniform structure generated by a metric
Theorem	metuval 24437*	Value of the uniform structure generated by metric 𝐷. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → (metUnif‘𝐷) = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))))
Theorem	metustel 24438*	Define a filter base 𝐹 generated by a metric 𝐷. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝐵 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐵 = (◡𝐷 “ (0[,)𝑎))))
Theorem	metustss 24439*	Range of the elements of the filter base generated by the metric 𝐷. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝐴 ⊆ (𝑋 × 𝑋))
Theorem	metustrel 24440*	Elements of the filter base generated by the metric 𝐷 are relations. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → Rel 𝐴)
Theorem	metustto 24441*	Any two elements of the filter base generated by the metric 𝐷 can be compared, like for RR+ (i.e. it's totally ordered). (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))
Theorem	metustid 24442*	The identity diagonal is included in all elements of the filter base generated by the metric 𝐷. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → ( I ↾ 𝑋) ⊆ 𝐴)
Theorem	metustsym 24443*	Elements of the filter base generated by the metric 𝐷 are symmetric. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → ◡𝐴 = 𝐴)
Theorem	metustexhalf 24444*	For any element 𝐴 of the filter base generated by the metric 𝐷, the half element (corresponding to half the distance) is also in this base. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)
Theorem	metustfbas 24445*	The filter base generated by a metric 𝐷. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
Theorem	metust 24446*	The uniform structure generated by a metric 𝐷. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
Theorem	cfilucfil 24447*	Given a metric 𝐷 and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 25165. (Contributed by Thierry Arnoux, 29-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))))
Theorem	metuust 24448	The uniform structure generated by metric 𝐷 is a uniform structure. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (metUnif‘𝐷) ∈ (UnifOn‘𝑋))
Theorem	cfilucfil2 24449*	Given a metric 𝐷 and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 25165. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFilu‘(metUnif‘𝐷)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))))
Theorem	blval2 24450	The ball around a point 𝑃, alternative definition. (Contributed by Thierry Arnoux, 7-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) = ((◡𝐷 “ (0[,)𝑅)) “ {𝑃}))
Theorem	elbl4 24451	Membership in a ball, alternative definition. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Mar-2018.)
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ+) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐵 ∈ (𝐴(ball‘𝐷)𝑅) ↔ 𝐵(◡𝐷 “ (0[,)𝑅))𝐴))
Theorem	metuel 24452*	Elementhood in the uniform structure generated by a metric 𝐷 (Contributed by Thierry Arnoux, 8-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑉 ∈ (metUnif‘𝐷) ↔ (𝑉 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))𝑤 ⊆ 𝑉)))
Theorem	metuel2 24453*	Elementhood in the uniform structure generated by a metric 𝐷 (Contributed by Thierry Arnoux, 24-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝑈 = (metUnif‘𝐷)    ⇒   ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑉 ∈ 𝑈 ↔ (𝑉 ⊆ (𝑋 × 𝑋) ∧ ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐷𝑦) < 𝑑 → 𝑥𝑉𝑦))))
Theorem	metustbl 24454*	The "section" image of an entourage at a point 𝑃 always contains a ball (centered on this point). (Contributed by Thierry Arnoux, 8-Dec-2017.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑉 ∈ (metUnif‘𝐷) ∧ 𝑃 ∈ 𝑋) → ∃𝑎 ∈ ran (ball‘𝐷)(𝑃 ∈ 𝑎 ∧ 𝑎 ⊆ (𝑉 “ {𝑃})))
Theorem	psmetutop 24455	The topology induced by a uniform structure generated by a metric 𝐷 is generated by that metric's open balls. (Contributed by Thierry Arnoux, 6-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.)
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (unifTop‘(metUnif‘𝐷)) = (topGen‘ran (ball‘𝐷)))
Theorem	xmetutop 24456	The topology induced by a uniform structure generated by an extended metric 𝐷 is that metric's open sets. (Contributed by Thierry Arnoux, 11-Mar-2018.)
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (∞Met‘𝑋)) → (unifTop‘(metUnif‘𝐷)) = (MetOpen‘𝐷))
Theorem	xmsusp 24457	If the uniform set of a metric space is the uniform structure generated by its metric, then it is a uniform space. (Contributed by Thierry Arnoux, 14-Dec-2017.)
⊢ 𝑋 = (Base‘𝐹)    &   ⊢ 𝐷 = ((dist‘𝐹) ↾ (𝑋 × 𝑋))    &   ⊢ 𝑈 = (UnifSt‘𝐹)    ⇒   ⊢ ((𝑋 ≠ ∅ ∧ 𝐹 ∈ ∞MetSp ∧ 𝑈 = (metUnif‘𝐷)) → 𝐹 ∈ UnifSp)
Theorem	restmetu 24458	The uniform structure generated by the restriction of a metric is its trace. (Contributed by Thierry Arnoux, 18-Dec-2017.)
⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((metUnif‘𝐷) ↾t (𝐴 × 𝐴)) = (metUnif‘(𝐷 ↾ (𝐴 × 𝐴))))
Theorem	metucn 24459*	Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn 24431. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝑈 = (metUnif‘𝐶)    &   ⊢ 𝑉 = (metUnif‘𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → 𝑌 ≠ ∅)    &   ⊢ (𝜑 → 𝐶 ∈ (PsMet‘𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑌))    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑))))
12.4.7  Examples of metric spaces
Theorem	dscmet 24460*	The discrete metric on any set 𝑋. Definition 1.1-8 of [Kreyszig] p. 8. (Contributed by FL, 12-Oct-2006.)
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if(𝑥 = 𝑦, 0, 1))    ⇒   ⊢ (𝑋 ∈ 𝑉 → 𝐷 ∈ (Met‘𝑋))
Theorem	dscopn 24461*	The discrete metric generates the discrete topology. In particular, the discrete topology is metrizable. (Contributed by Mario Carneiro, 29-Jan-2014.)
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if(𝑥 = 𝑦, 0, 1))    ⇒   ⊢ (𝑋 ∈ 𝑉 → (MetOpen‘𝐷) = 𝒫 𝑋)
Theorem	nrmmetd 24462*	Show that a group norm generates a metric. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐹:𝑋⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 ))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → (𝐹 ∘ − ) ∈ (Met‘𝑋))
Theorem	abvmet 24463	An absolute value 𝐹 generates a metric defined by 𝑑(𝑥, 𝑦) = 𝐹(𝑥 − 𝑦), analogously to cnmet 24659. (In fact, the ring structure is not needed at all; the group properties abveq0 20727 and abvtri 20731, abvneg 20735 are sufficient.) (Contributed by Mario Carneiro, 9-Sep-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ − = (-g‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (𝐹 ∘ − ) ∈ (Met‘𝑋))
12.4.8  Normed algebraic structures In the following, the norm of a normed algebraic structure (group, left module, vector space) is defined by the (given) distance function (the norm 𝑁 of an element is its distance 𝐷 from the zero element, see nmval 24477: (𝑁‘𝐴) = (𝐴𝐷 0 )). By this definition, the norm function 𝑁 is actually a norm (satisfying the properties: being a function into the reals; subadditivity/triangle inequality (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)); absolute homogeneity ( n(sx) = |s| n(x) ) [Remark: for group norms, some authors (e.g., Juris Steprans in "A characterization of free abelian groups") demand that n(sx) = |s| n(x) for all 𝑠 ∈ ℤ, whereas other authors (e.g., N. H. Bingham and A. J. Ostaszewski in "Normed versus topological groups: Dichotomy and duality") only require inversion symmetry, i.e., (𝑁‘( − 𝑥) = 𝑁‘𝑥). The definition df-ngp 24471 of a group norm follows the second approach, see nminv 24509.] and positive definiteness/point-separation ((𝑁‘𝑥) = 0 ↔ 𝑥 = 0)) if the structure is a metric space with a right-translation-invariant metric (see nmf 24503, nmtri 24514, nmvs 24564 and nmeq0 24506). An alternate definition of a normed group (i.e., a group equipped with a norm) not using the properties of a metric space is given by Theorem tngngp3 24544. The norm can be expressed as the distance to zero (nmfval 24476), so in a structure with a zero (a "pointed set", for instance a monoid or a group), the norm can be expressed as the distance restricted to the elements of the base set to zero (nmfval0 24478). Usually, however, the norm of a normed structure is given, and the corresponding metric ("induced metric") is defined as the distance function based on the norm (the distance 𝐷 between two elements is the norm 𝑁 of their difference, see ngpds 24492: (𝐴𝐷𝐵) = (𝑁‘(𝐴 − 𝐵))). The operation toNrmGrp does exactly this, i.e., it adds a distance function (and a topology) to a structure (which should be at least a group for the difference of two elements to make sense) corresponding to a given norm as explained above: (dist‘𝑇) = (𝑁 ∘ − ), see also tngds 24536. By this, the enhanced structure becomes a normed structure if the induced metric is in fact a metric (see tngngp2 24540) or a norm (see tngngpd 24541). If the norm is derived from a given metric, as done with df-nm 24470, the induced metric is the original metric restricted to the base set: (dist‘𝑇) = ((dist‘𝐺) ↾ (𝑋 × 𝑋)), see nrmtngdist 24545, and the norm remains the same: (norm‘𝑇) = (norm‘𝐺), see nrmtngnrm 24546.
Syntax	cnm 24464	Norm of a normed ring.
class norm
Syntax	cngp 24465	The class of all normed groups.
class NrmGrp
Syntax	ctng 24466	Make a normed group from a norm and a group.
class toNrmGrp
Syntax	cnrg 24467	Normed ring.
class NrmRing
Syntax	cnlm 24468	Normed module.
class NrmMod
Syntax	cnvc 24469	Normed vector space.
class NrmVec
Definition	df-nm 24470*	Define the norm on a group or ring (when it makes sense) in terms of the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ norm = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤) ↦ (𝑥(dist‘𝑤)(0g‘𝑤))))
Definition	df-ngp 24471	Define a normed group, which is a group with a right-translation-invariant metric. This is not a standard notion, but is helpful as the most general context in which a metric-like norm makes sense. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ NrmGrp = {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)}
Definition	df-tng 24472*	Define a function that fills in the topology and metric components of a structure given a group and a norm on it. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ toNrmGrp = (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet ⟨(dist‘ndx), (𝑓 ∘ (-g‘𝑔))⟩) sSet ⟨(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))⟩))
Definition	df-nrg 24473	A normed ring is a ring with an induced topology and metric such that the metric is translation-invariant and the norm (distance from 0) is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ NrmRing = {𝑤 ∈ NrmGrp ∣ (norm‘𝑤) ∈ (AbsVal‘𝑤)}
Definition	df-nlm 24474*	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.)
⊢ NrmMod = {𝑤 ∈ (NrmGrp ∩ LMod) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))}
Definition	df-nvc 24475	A normed vector space is a normed module which is also a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ NrmVec = (NrmMod ∩ LVec)
Theorem	nmfval 24476*	The value of the norm function as the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐷 = (dist‘𝑊)    ⇒   ⊢ 𝑁 = (𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 ))
Theorem	nmval 24477	The value of the norm as the distance to zero. Problem 1 of [Kreyszig] p. 63. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐷 = (dist‘𝑊)    ⇒   ⊢ (𝐴 ∈ 𝑋 → (𝑁‘𝐴) = (𝐴𝐷 0 ))
Theorem	nmfval0 24478*	The value of the norm function on a structure containing a zero as the distance restricted to the elements of the base set to zero. Examples of structures containing a "zero" are groups (see nmfval2 24479 proved from this theorem and grpidcl 18897) or more generally monoids (see mndidcl 18676), or pointed sets). (Contributed by Mario Carneiro, 2-Oct-2015.) Extract this result from the proof of nmfval2 24479. (Revised by BJ, 27-Aug-2024.)
⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋))    ⇒   ⊢ ( 0 ∈ 𝑋 → 𝑁 = (𝑥 ∈ 𝑋 ↦ (𝑥𝐸 0 )))
Theorem	nmfval2 24479*	The value of the norm function on a group as the distance restricted to the elements of the base set to zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝑊 ∈ Grp → 𝑁 = (𝑥 ∈ 𝑋 ↦ (𝑥𝐸 0 )))
Theorem	nmval2 24480	The value of the norm on a group as the distance restricted to the elements of the base set to zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋))    ⇒   ⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (𝐴𝐸 0 ))
Theorem	nmf2 24481	The norm on a metric group is a function from the base set into the reals. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋))    ⇒   ⊢ ((𝑊 ∈ Grp ∧ 𝐸 ∈ (Met‘𝑋)) → 𝑁:𝑋⟶ℝ)
Theorem	nmpropd 24482	Weak property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (+g‘𝐾) = (+g‘𝐿))    &   ⊢ (𝜑 → (dist‘𝐾) = (dist‘𝐿))    ⇒   ⊢ (𝜑 → (norm‘𝐾) = (norm‘𝐿))
Theorem	nmpropd2 24483*	Strong property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐾 ∈ Grp)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → (norm‘𝐾) = (norm‘𝐿))
Theorem	isngp 24484	The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) ⊆ 𝐷))
Theorem	isngp2 24485	The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = 𝐸))
Theorem	isngp3 24486*	The property of being a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑁 = (norm‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦))))
Theorem	ngpgrp 24487	A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp)
Theorem	ngpms 24488	A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp)
Theorem	ngpxms 24489	A normed group is an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ ∞MetSp)
Theorem	ngptps 24490	A normed group is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ TopSp)
Theorem	ngpmet 24491	The (induced) metric of a normed group is a metric. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by AV, 14-Oct-2021.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐷 = ((dist‘𝐺) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝐺 ∈ NrmGrp → 𝐷 ∈ (Met‘𝑋))
Theorem	ngpds 24492	Value of the distance function in terms of the norm of a normed group. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 28-Nov-2006.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐴 − 𝐵)))
Theorem	ngpdsr 24493	Value of the distance function in terms of the norm of a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐵 − 𝐴)))
Theorem	ngpds2 24494	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = ((𝐴 − 𝐵)𝐷 0 ))
Theorem	ngpds2r 24495	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = ((𝐵 − 𝐴)𝐷 0 ))
Theorem	ngpds3 24496	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = ( 0 𝐷(𝐴 − 𝐵)))
Theorem	ngpds3r 24497	Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = ( 0 𝐷(𝐵 − 𝐴)))
Theorem	ngprcan 24498	Cancel right addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ ((𝐺 ∈ NrmGrp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐶)𝐷(𝐵 + 𝐶)) = (𝐴𝐷𝐵))
Theorem	ngplcan 24499	Cancel left addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ (((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶 + 𝐴)𝐷(𝐶 + 𝐵)) = (𝐴𝐷𝐵))
Theorem	isngp4 24500*	Express the property of being a normed group purely in terms of right-translation invariance of the metric instead of using the definition of norm (which itself uses the metric). (Contributed by Mario Carneiro, 29-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦)))