P. 242 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24101-24200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	uspreg 24101	If a uniform space is Hausdorff, it is regular. Proposition 3 of [BourbakiTop1] p. II.5. (Contributed by Thierry Arnoux, 4-Jan-2018.)
⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ ((𝑊 ∈ UnifSp ∧ 𝐽 ∈ Haus) → 𝐽 ∈ Reg)
12.3.4  Uniform continuity
Syntax	cucn 24102	Extend class notation with the uniform continuity operation.
class Cnu
Definition	df-ucn 24103*	Define a function on two uniform structures which value is the set of uniformly continuous functions from the first uniform structure to the second. A function 𝑓 is uniformly continuous if, roughly speaking, it is possible to guarantee that (𝑓‘𝑥) and (𝑓‘𝑦) be as close to each other as we please by requiring only that 𝑥 and 𝑦 are sufficiently close to each other; unlike ordinary continuity, the maximum distance between (𝑓‘𝑥) and (𝑓‘𝑦) cannot depend on 𝑥 and 𝑦 themselves. This formulation is the definition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ Cnu = (𝑢 ∈ ∪ ran UnifOn, 𝑣 ∈ ∪ ran UnifOn ↦ {𝑓 ∈ (dom ∪ 𝑣 ↑m dom ∪ 𝑢) ∣ ∀𝑠 ∈ 𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
Theorem	ucnval 24104*	The set of all uniformly continuous function from uniform space 𝑈 to uniform space 𝑉. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝑈 Cnu𝑉) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
Theorem	isucn 24105*	The predicate "𝐹 is a uniformly continuous function from uniform space 𝑈 to uniform space 𝑉". (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))))
Theorem	isucn2 24106*	The predicate "𝐹 is a uniformly continuous function from uniform space 𝑈 to uniform space 𝑉", expressed with filter bases for the entourages. (Contributed by Thierry Arnoux, 26-Jan-2018.)
⊢ 𝑈 = ((𝑋 × 𝑋)filGen𝑅)    &   ⊢ 𝑉 = ((𝑌 × 𝑌)filGen𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝑅 ∈ (fBas‘(𝑋 × 𝑋)))    &   ⊢ (𝜑 → 𝑆 ∈ (fBas‘(𝑌 × 𝑌)))    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑠 ∈ 𝑆 ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))))
Theorem	ucnimalem 24107*	Reformulate the 𝐺 function as a mapping with one variable. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)    ⇒   ⊢ 𝐺 = (𝑝 ∈ (𝑋 × 𝑋) ↦ ⟨(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))⟩)
Theorem	ucnima 24108*	An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ 𝑈 (𝐺 “ 𝑟) ⊆ 𝑊)
Theorem	ucnprima 24109*	The preimage by a uniformly continuous function 𝐹 of an entourage 𝑊 of 𝑌 is an entourage of 𝑋. Note of the definition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)    ⇒   ⊢ (𝜑 → (◡𝐺 “ 𝑊) ∈ 𝑈)
Theorem	iducn 24110	The identity is uniformly continuous from a uniform structure to itself. Example 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ( I ↾ 𝑋) ∈ (𝑈 Cnu𝑈))
Theorem	cstucnd 24111	A constant function is uniformly continuous. Deduction form. Example 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑌)    ⇒   ⊢ (𝜑 → (𝑋 × {𝐴}) ∈ (𝑈 Cnu𝑉))
Theorem	ucncn 24112	Uniform continuity implies continuity. Deduction form. Proposition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 30-Nov-2017.)
⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ 𝐾 = (TopOpen‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ UnifSp)    &   ⊢ (𝜑 → 𝑆 ∈ UnifSp)    &   ⊢ (𝜑 → 𝑅 ∈ TopSp)    &   ⊢ (𝜑 → 𝑆 ∈ TopSp)    &   ⊢ (𝜑 → 𝐹 ∈ ((UnifSt‘𝑅) Cnu(UnifSt‘𝑆)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))
12.3.5  Cauchy filters in uniform spaces
Syntax	ccfilu 24113	Extend class notation with the set of Cauchy filter bases.
class CauFilu
Definition	df-cfilu 24114*	Define the set of Cauchy filter bases on a uniform space. A Cauchy filter base is a filter base on the set such that for every entourage 𝑣, there is an element 𝑎 of the filter "small enough in 𝑣 " i.e. such that every pair {𝑥, 𝑦} of points in 𝑎 is related by 𝑣". Definition 2 of [BourbakiTop1] p. II.13. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ CauFilu = (𝑢 ∈ ∪ ran UnifOn ↦ {𝑓 ∈ (fBas‘dom ∪ 𝑢) ∣ ∀𝑣 ∈ 𝑢 ∃𝑎 ∈ 𝑓 (𝑎 × 𝑎) ⊆ 𝑣})
Theorem	iscfilu 24115*	The predicate "𝐹 is a Cauchy filter base on uniform space 𝑈". (Contributed by Thierry Arnoux, 18-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐹 ∈ (CauFilu‘𝑈) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ 𝐹 (𝑎 × 𝑎) ⊆ 𝑣)))
Theorem	cfilufbas 24116	A Cauchy filter base is a filter base. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐹 ∈ (CauFilu‘𝑈)) → 𝐹 ∈ (fBas‘𝑋))
Theorem	cfiluexsm 24117*	For a Cauchy filter base and any entourage 𝑉, there is an element of the filter small in 𝑉. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐹 ∈ (CauFilu‘𝑈) ∧ 𝑉 ∈ 𝑈) → ∃𝑎 ∈ 𝐹 (𝑎 × 𝑎) ⊆ 𝑉)
Theorem	fmucndlem 24118*	Lemma for fmucnd 24119. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝐴 × 𝐴)) = ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))
Theorem	fmucnd 24119*	The image of a Cauchy filter base by an uniformly continuous function is a Cauchy filter base. Deduction form. Proposition 3 of [BourbakiTop1] p. II.13. (Contributed by Thierry Arnoux, 18-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))    &   ⊢ (𝜑 → 𝐶 ∈ (CauFilu‘𝑈))    &   ⊢ 𝐷 = ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (CauFilu‘𝑉))
Theorem	cfilufg 24120	The filter generated by a Cauchy filter base is still a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐹 ∈ (CauFilu‘𝑈)) → (𝑋filGen𝐹) ∈ (CauFilu‘𝑈))
Theorem	trcfilu 24121	Condition for the trace of a Cauchy filter base to be a Cauchy filter base for the restricted uniform structure. (Contributed by Thierry Arnoux, 24-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐹 ∈ (CauFilu‘𝑈) ∧ ¬ ∅ ∈ (𝐹 ↾t 𝐴)) ∧ 𝐴 ⊆ 𝑋) → (𝐹 ↾t 𝐴) ∈ (CauFilu‘(𝑈 ↾t (𝐴 × 𝐴))))
Theorem	cfiluweak 24122	A Cauchy filter base is also a Cauchy filter base on any coarser uniform structure. (Contributed by Thierry Arnoux, 24-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ (CauFilu‘(𝑈 ↾t (𝐴 × 𝐴)))) → 𝐹 ∈ (CauFilu‘𝑈))
Theorem	neipcfilu 24123	In an uniform space, a neighboring filter is a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018.)
⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑈 = (UnifSt‘𝑊)    ⇒   ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) ∈ (CauFilu‘𝑈))
12.3.6  Complete uniform spaces
Syntax	ccusp 24124	Extend class notation with the class of all complete uniform spaces.
class CUnifSp
Definition	df-cusp 24125*	Define the class of all complete uniform spaces. Definition 3 of [BourbakiTop1] p. II.15. (Contributed by Thierry Arnoux, 1-Dec-2017.)
⊢ CUnifSp = {𝑤 ∈ UnifSp ∣ ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)}
Theorem	iscusp 24126*	The predicate "𝑊 is a complete uniform space." (Contributed by Thierry Arnoux, 3-Dec-2017.)
⊢ (𝑊 ∈ CUnifSp ↔ (𝑊 ∈ UnifSp ∧ ∀𝑐 ∈ (Fil‘(Base‘𝑊))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅)))
Theorem	cuspusp 24127	A complete uniform space is an uniform space. (Contributed by Thierry Arnoux, 3-Dec-2017.)
⊢ (𝑊 ∈ CUnifSp → 𝑊 ∈ UnifSp)
Theorem	cuspcvg 24128	In a complete uniform space, any Cauchy filter 𝐶 has a limit. (Contributed by Thierry Arnoux, 3-Dec-2017.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ ((𝑊 ∈ CUnifSp ∧ 𝐶 ∈ (CauFilu‘(UnifSt‘𝑊)) ∧ 𝐶 ∈ (Fil‘𝐵)) → (𝐽 fLim 𝐶) ≠ ∅)
Theorem	iscusp2 24129*	The predicate "𝑊 is a complete uniform space." (Contributed by Thierry Arnoux, 15-Dec-2017.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑈 = (UnifSt‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ (𝑊 ∈ CUnifSp ↔ (𝑊 ∈ UnifSp ∧ ∀𝑐 ∈ (Fil‘𝐵)(𝑐 ∈ (CauFilu‘𝑈) → (𝐽 fLim 𝑐) ≠ ∅)))
Theorem	cnextucn 24130*	Extension by continuity. Proposition 11 of [BourbakiTop1] p. II.20. Given a topology 𝐽 on 𝑋, a subset 𝐴 dense in 𝑋, this states a condition for 𝐹 from 𝐴 to a space 𝑌 Hausdorff and complete to be extensible by continuity. (Contributed by Thierry Arnoux, 4-Dec-2017.)
⊢ 𝑋 = (Base‘𝑉)    &   ⊢ 𝑌 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑉)    &   ⊢ 𝐾 = (TopOpen‘𝑊)    &   ⊢ 𝑈 = (UnifSt‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ TopSp)    &   ⊢ (𝜑 → 𝑊 ∈ TopSp)    &   ⊢ (𝜑 → 𝑊 ∈ CUnifSp)    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑌)    &   ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑌 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∈ (CauFilu‘𝑈))    ⇒   ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))
Theorem	ucnextcn 24131	Extension by continuity. Theorem 2 of [BourbakiTop1] p. II.20. Given an uniform space on a set 𝑋, a subset 𝐴 dense in 𝑋, and a function 𝐹 uniformly continuous from 𝐴 to 𝑌, that function can be extended by continuity to the whole 𝑋, and its extension is uniformly continuous. (Contributed by Thierry Arnoux, 25-Jan-2018.)
⊢ 𝑋 = (Base‘𝑉)    &   ⊢ 𝑌 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑉)    &   ⊢ 𝐾 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (UnifSt‘𝑉)    &   ⊢ 𝑇 = (UnifSt‘(𝑉 ↾s 𝐴))    &   ⊢ 𝑈 = (UnifSt‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ TopSp)    &   ⊢ (𝜑 → 𝑉 ∈ UnifSp)    &   ⊢ (𝜑 → 𝑊 ∈ TopSp)    &   ⊢ (𝜑 → 𝑊 ∈ CUnifSp)    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑇 Cnu𝑈))    &   ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝑋)    ⇒   ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))
12.4  Metric spaces
12.4.1  Pseudometric spaces
Theorem	ispsmet 24132*	Express the predicate "𝐷 is a pseudometric." (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ (𝑋 ∈ 𝑉 → (𝐷 ∈ (PsMet‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐷𝑥) = 0 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))))
Theorem	psmetdmdm 24133	Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷)
Theorem	psmetf 24134	The distance function of a pseudometric as a function. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
Theorem	psmetcl 24135	Closure of the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)
Theorem	psmet0 24136	The distance function of a pseudometric space is zero if its arguments are equal. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0)
Theorem	psmettri2 24137	Triangle inequality for the distance function of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵)))
Theorem	psmetsym 24138	The distance function of a pseudometric is symmetrical. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
Theorem	psmettri 24139	Triangle inequality for the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐶𝐷𝐵)))
Theorem	psmetge0 24140	The distance function of a pseudometric space is nonnegative. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵))
Theorem	psmetxrge0 24141	The distance function of a pseudometric space is a function into the nonnegative extended real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
Theorem	psmetres2 24142	Restriction of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (PsMet‘𝑅))
Theorem	psmetlecl 24143	Real closure of an extended metric value that is upper bounded by a real. (Contributed by Thierry Arnoux, 11-Mar-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ ℝ ∧ (𝐴𝐷𝐵) ≤ 𝐶)) → (𝐴𝐷𝐵) ∈ ℝ)
Theorem	distspace 24144	A set 𝑋 together with a (distance) function 𝐷 which is a pseudometric is a distance space (according to E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006), i.e. a (base) set 𝑋 equipped with a distance 𝐷, which is a mapping of two elements of the base set to the (extended) reals and which is nonnegative, symmetric and equal to 0 if the two elements are equal. (Contributed by AV, 15-Oct-2021.) (Revised by AV, 5-Jul-2022.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ (𝐴𝐷𝐴) = 0) ∧ (0 ≤ (𝐴𝐷𝐵) ∧ (𝐴𝐷𝐵) = (𝐵𝐷𝐴))))
12.4.2  Basic metric space properties
Syntax	cxms 24145	Extend class notation with the class of extended metric spaces.
class ∞MetSp
Syntax	cms 24146	Extend class notation with the class of metric spaces.
class MetSp
Syntax	ctms 24147	Extend class notation with the function mapping a metric to the metric space it defines.
class toMetSp
Definition	df-xms 24148	Define the (proper) class of extended metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ ∞MetSp = {𝑓 ∈ TopSp ∣ (TopOpen‘𝑓) = (MetOpen‘((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))))}
Definition	df-ms 24149	Define the (proper) class of metric spaces. (Contributed by NM, 27-Aug-2006.)
⊢ MetSp = {𝑓 ∈ ∞MetSp ∣ ((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))) ∈ (Met‘(Base‘𝑓))}
Definition	df-tms 24150	Define the function mapping a metric to the metric space which it defines. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ toMetSp = (𝑑 ∈ ∪ ran ∞Met ↦ ({⟨(Base‘ndx), dom dom 𝑑⟩, ⟨(dist‘ndx), 𝑑⟩} sSet ⟨(TopSet‘ndx), (MetOpen‘𝑑)⟩))
Theorem	ismet 24151*	Express the predicate "𝐷 is a metric." (Contributed by NM, 25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))))
Theorem	isxmet 24152*	Express the predicate "𝐷 is an extended metric." (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (∞Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))))
Theorem	ismeti 24153*	Properties that determine a metric. (Contributed by NM, 17-Nov-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ 𝑋 ∈ V    &   ⊢ 𝐷:(𝑋 × 𝑋)⟶ℝ    &   ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))    &   ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))    ⇒   ⊢ 𝐷 ∈ (Met‘𝑋)
Theorem	isxmetd 24154*	Properties that determine an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) (Revised by AV, 9-Apr-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
Theorem	isxmet2d 24155*	It is safe to only require the triangle inequality when the values are real (so that we can use the standard addition over the reals), but in this case the nonnegativity constraint cannot be deduced and must be provided separately. (Counterexample: 𝐷(𝑥, 𝑦) = if(𝑥 = 𝑦, 0, -∞) satisfies all hypotheses except nonnegativity.) (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (𝑥𝐷𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
Theorem	metflem 24156*	Lemma for metf 24158 and others. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ (𝐷 ∈ (Met‘𝑋) → (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))))
Theorem	xmetf 24157	Mapping of the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
Theorem	metf 24158	Mapping of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.)
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ)
Theorem	xmetcl 24159	Closure of the distance function of a metric space. Part of Property M1 of [Kreyszig] p. 3. (Contributed by NM, 30-Aug-2006.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)
Theorem	metcl 24160	Closure of the distance function of a metric space. Part of Property M1 of [Kreyszig] p. 3. (Contributed by NM, 30-Aug-2006.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ)
Theorem	ismet2 24161	An extended metric is a metric exactly when it takes real values for all values of the arguments. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐷 ∈ (Met‘𝑋) ↔ (𝐷 ∈ (∞Met‘𝑋) ∧ 𝐷:(𝑋 × 𝑋)⟶ℝ))
Theorem	metxmet 24162	A metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
Theorem	xmetdmdm 24163	Recover the base set from an extended metric. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = dom dom 𝐷)
Theorem	metdmdm 24164	Recover the base set from a metric. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (𝐷 ∈ (Met‘𝑋) → 𝑋 = dom dom 𝐷)
Theorem	xmetunirn 24165	Two ways to express an extended metric on an unspecified base. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (𝐷 ∈ ∪ ran ∞Met ↔ 𝐷 ∈ (∞Met‘dom dom 𝐷))
Theorem	xmeteq0 24166	The value of an extended metric is zero iff its arguments are equal. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵) = 0 ↔ 𝐴 = 𝐵))
Theorem	meteq0 24167	The value of a metric is zero iff its arguments are equal. Property M2 of [Kreyszig] p. 4. (Contributed by NM, 30-Aug-2006.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵) = 0 ↔ 𝐴 = 𝐵))
Theorem	xmettri2 24168	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵)))
Theorem	mettri2 24169	Triangle inequality for the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) + (𝐶𝐷𝐵)))
Theorem	xmet0 24170	The distance function of a metric space is zero if its arguments are equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0)
Theorem	met0 24171	The distance function of a metric space is zero if its arguments are equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by NM, 30-Aug-2006.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0)
Theorem	xmetge0 24172	The distance function of a metric space is nonnegative. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵))
Theorem	metge0 24173	The distance function of a metric space is nonnegative. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵))
Theorem	xmetlecl 24174	Real closure of an extended metric value that is upper bounded by a real. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ ℝ ∧ (𝐴𝐷𝐵) ≤ 𝐶)) → (𝐴𝐷𝐵) ∈ ℝ)
Theorem	xmetsym 24175	The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
Theorem	xmetpsmet 24176	An extended metric is a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ (PsMet‘𝑋))
Theorem	xmettpos 24177	The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → tpos 𝐷 = 𝐷)
Theorem	metsym 24178	The distance function of a metric space is symmetric. Definition 14-1.1(c) of [Gleason] p. 223. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
Theorem	xmettri 24179	Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐶𝐷𝐵)))
Theorem	mettri 24180	Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by NM, 27-Aug-2006.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐶𝐷𝐵)))
Theorem	xmettri3 24181	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶)))
Theorem	mettri3 24182	Triangle inequality for the distance function of a metric space. (Contributed by NM, 13-Mar-2007.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶)))
Theorem	xmetrtri 24183	One half of the reverse triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐶) +𝑒 -𝑒(𝐵𝐷𝐶)) ≤ (𝐴𝐷𝐵))
Theorem	xmetrtri2 24184	The reverse triangle inequality for the distance function of an extended metric. In order to express the "extended absolute value function", we use the distance function xrsdsval 21273 defined on the extended real structure. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐾 = (dist‘ℝ*𝑠)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐶)𝐾(𝐵𝐷𝐶)) ≤ (𝐴𝐷𝐵))
Theorem	metrtri 24185	Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 5-May-2014.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵))
Theorem	xmetgt0 24186	The distance function of an extended metric space is positive for unequal points. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ≠ 𝐵 ↔ 0 < (𝐴𝐷𝐵)))
Theorem	metgt0 24187	The distance function of a metric space is positive for unequal points. Definition 14-1.1(b) of [Gleason] p. 223 and its converse. (Contributed by NM, 27-Aug-2006.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ≠ 𝐵 ↔ 0 < (𝐴𝐷𝐵)))
Theorem	metn0 24188	A metric space is nonempty iff its base set is nonempty. (Contributed by NM, 4-Oct-2007.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ (𝐷 ∈ (Met‘𝑋) → (𝐷 ≠ ∅ ↔ 𝑋 ≠ ∅))
Theorem	xmetres2 24189	Restriction of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (∞Met‘𝑅))
Theorem	metreslem 24190	Lemma for metres 24193. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ (dom 𝐷 = (𝑋 × 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) = (𝐷 ↾ ((𝑋 ∩ 𝑅) × (𝑋 ∩ 𝑅))))
Theorem	metres2 24191	Lemma for metres 24193. (Contributed by FL, 12-Oct-2006.) (Proof shortened by Mario Carneiro, 14-Aug-2015.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (Met‘𝑅))
Theorem	xmetres 24192	A restriction of an extended metric is an extended metric. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (∞Met‘(𝑋 ∩ 𝑅)))
Theorem	metres 24193	A restriction of a metric is a metric. (Contributed by NM, 26-Aug-2007.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ (𝐷 ∈ (Met‘𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (Met‘(𝑋 ∩ 𝑅)))
Theorem	0met 24194	The empty metric. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ ∅ ∈ (Met‘∅)
Theorem	prdsdsf 24195*	The product metric is a function into the nonnegative extended reals. In general this means that it is not a metric but rather an *extended* metric (even when all the factors are metrics), but it will be a metric when restricted to regions where it does not take infinite values. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))    ⇒   ⊢ (𝜑 → 𝐷:(𝐵 × 𝐵)⟶(0[,]+∞))
Theorem	prdsxmetlem 24196*	The product metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵))
Theorem	prdsxmet 24197*	The product metric is an extended metric. Eliminate disjoint variable conditions from prdsxmetlem 24196. (Contributed by Mario Carneiro, 26-Sep-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵))
Theorem	prdsmet 24198*	The product metric is a metric when the index set is finite. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵))
Theorem	ressprdsds 24199*	Restriction of a product metric. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)))    &   ⊢ (𝜑 → 𝐻 = (𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴))))    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝐸 = (dist‘𝐻)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐴 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐸 = (𝐷 ↾ (𝐵 × 𝐵)))
Theorem	resspwsds 24200	Restriction of a power metric. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ (𝜑 → 𝑌 = (𝑅 ↑s 𝐼))    &   ⊢ (𝜑 → 𝐻 = ((𝑅 ↾s 𝐴) ↑s 𝐼))    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝐸 = (dist‘𝐻)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐸 = (𝐷 ↾ (𝐵 × 𝐵)))