P. 246 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24501-24600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tsmssplit 24501	Split a topological group sum into two parts. (Contributed by Mario Carneiro, 19-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐺 ∈ TopMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums (𝐹 ↾ 𝐶)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐺 tsums (𝐹 ↾ 𝐷)))    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷))    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐺 tsums 𝐹))
Theorem	tsmsxplem1 24502*	Lemma for tsmsxp 24504. (Contributed by Mario Carneiro, 21-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐺 ∈ TopGrp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵)    &   ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))    &   ⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐿 ∈ 𝐽)    &   ⊢ (𝜑 → 0 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐴 ∩ Fin))    &   ⊢ (𝜑 → dom 𝐷 ⊆ 𝐾)    &   ⊢ (𝜑 → 𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
Theorem	tsmsxplem2 24503*	Lemma for tsmsxp 24504. (Contributed by Mario Carneiro, 21-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐺 ∈ TopGrp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵)    &   ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))    &   ⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐿 ∈ 𝐽)    &   ⊢ (𝜑 → 0 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐴 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑐 ∈ 𝑆 ∀𝑑 ∈ 𝑇 (𝑐 + 𝑑) ∈ 𝑈)    &   ⊢ (𝜑 → 𝑁 ∈ (𝒫 𝐶 ∩ Fin))    &   ⊢ (𝜑 → 𝐷 ⊆ (𝐾 × 𝑁))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁)))) ∈ 𝐿)    &   ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) ∈ 𝑆)    &   ⊢ (𝜑 → ∀𝑔 ∈ (𝐿 ↑m 𝐾)(𝐺 Σg 𝑔) ∈ 𝑇)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐻 ↾ 𝐾)) ∈ 𝑈)
Theorem	tsmsxp 24504*	Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 20220 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 24502 for the main proof; this part mostly sets up the local assumptions. (Contributed by Mario Carneiro, 21-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐺 ∈ TopGrp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵)    &   ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))    ⇒   ⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ (𝐺 tsums 𝐻))
12.2.8  Topological rings, fields, vector spaces
Syntax	ctrg 24505	The class of all topological division rings.
class TopRing
Syntax	ctdrg 24506	The class of all topological division rings.
class TopDRing
Syntax	ctlm 24507	The class of all topological modules.
class TopMod
Syntax	ctvc 24508	The class of all topological vector spaces.
class TopVec
Definition	df-trg 24509	Define a topological ring, which is a ring such that the addition is a topological group operation and the multiplication is continuous. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ TopRing = {𝑟 ∈ (TopGrp ∩ Ring) ∣ (mulGrp‘𝑟) ∈ TopMnd}
Definition	df-tdrg 24510	Define a topological division ring (which differs from a topological field only in being potentially noncommutative), which is a division ring and topological ring such that the unit group of the division ring (which is the set of nonzero elements) is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ TopDRing = {𝑟 ∈ (TopRing ∩ DivRing) ∣ ((mulGrp‘𝑟) ↾s (Unit‘𝑟)) ∈ TopGrp}
Definition	df-tlm 24511	Define a topological left module, which is just what its name suggests: instead of a group over a ring with a scalar product connecting them, it is a topological group over a topological ring with a continuous scalar product. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ TopMod = {𝑤 ∈ (TopMnd ∩ LMod) ∣ ((Scalar‘𝑤) ∈ TopRing ∧ ( ·sf ‘𝑤) ∈ (((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤)) Cn (TopOpen‘𝑤)))}
Definition	df-tvc 24512	Define a topological left vector space, which is a topological module over a topological division ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ TopVec = {𝑤 ∈ TopMod ∣ (Scalar‘𝑤) ∈ TopDRing}
Theorem	istrg 24513	Express the predicate "𝑅 is a topological ring". (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ TopRing ↔ (𝑅 ∈ TopGrp ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ TopMnd))
Theorem	trgtmd 24514	The multiplicative monoid of a topological ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ TopRing → 𝑀 ∈ TopMnd)
Theorem	istdrg 24515	Express the predicate "𝑅 is a topological ring". (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑅 ∈ TopDRing ↔ (𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 ↾s 𝑈) ∈ TopGrp))
Theorem	tdrgunit 24516	The unit group of a topological division ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑅 ∈ TopDRing → (𝑀 ↾s 𝑈) ∈ TopGrp)
Theorem	trgtgp 24517	A topological ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopGrp)
Theorem	trgtmd2 24518	A topological ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopMnd)
Theorem	trgtps 24519	A topological ring is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopSp)
Theorem	trgring 24520	A topological ring is a ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ Ring)
Theorem	trggrp 24521	A topological ring is a group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ Grp)
Theorem	tdrgtrg 24522	A topological division ring is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ TopRing)
Theorem	tdrgdrng 24523	A topological division ring is a division ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ DivRing)
Theorem	tdrgring 24524	A topological division ring is a ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ Ring)
Theorem	tdrgtmd 24525	A topological division ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ TopMnd)
Theorem	tdrgtps 24526	A topological division ring is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ TopSp)
Theorem	istdrg2 24527	A topological-ring division ring is a topological division ring iff the group of nonzero elements is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ TopDRing ↔ (𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 ↾s (𝐵 ∖ { 0 })) ∈ TopGrp))
Theorem	mulrcn 24528	The functionalization of the ring multiplication operation is a continuous function in a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ 𝑇 = (+𝑓‘(mulGrp‘𝑅))    ⇒   ⊢ (𝑅 ∈ TopRing → 𝑇 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
Theorem	invrcn2 24529	The multiplicative inverse function is a continuous function from the unit group (that is, the nonzero numbers) to itself. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑅 ∈ TopDRing → 𝐼 ∈ ((𝐽 ↾t 𝑈) Cn (𝐽 ↾t 𝑈)))
Theorem	invrcn 24530	The multiplicative inverse function is a continuous function from the unit group (that is, the nonzero numbers) to the field. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑅 ∈ TopDRing → 𝐼 ∈ ((𝐽 ↾t 𝑈) Cn 𝐽))
Theorem	cnmpt1mulr 24531*	Continuity of ring multiplication; analogue of cnmpt12f 24015 which cannot be used directly because .r is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ TopRing)    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐾 Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝐾 Cn 𝐽))
Theorem	cnmpt2mulr 24532*	Continuity of ring multiplication; analogue of cnmpt22f 24024 which cannot be used directly because .r is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ TopRing)    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴 · 𝐵)) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))
Theorem	dvrcn 24533	The division function is continuous in a topological field. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑅 ∈ TopDRing → / ∈ ((𝐽 ×t (𝐽 ↾t 𝑈)) Cn 𝐽))
Theorem	istlm 24534	The predicate "𝑊 is a topological left module". (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ · = ( ·sf ‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (TopOpen‘𝐹)    ⇒   ⊢ (𝑊 ∈ TopMod ↔ ((𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ TopRing) ∧ · ∈ ((𝐾 ×t 𝐽) Cn 𝐽)))
Theorem	vscacn 24535	The scalar multiplication is continuous in a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ · = ( ·sf ‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (TopOpen‘𝐹)    ⇒   ⊢ (𝑊 ∈ TopMod → · ∈ ((𝐾 ×t 𝐽) Cn 𝐽))
Theorem	tlmtmd 24536	A topological module is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopMnd)
Theorem	tlmtps 24537	A topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopSp)
Theorem	tlmlmod 24538	A topological module is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ LMod)
Theorem	tlmtrg 24539	The scalar ring of a topological module is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopRing)
Theorem	tlmscatps 24540	The scalar ring of a topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopSp)
Theorem	istvc 24541	A topological vector space is a topological module over a topological division ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ TopVec ↔ (𝑊 ∈ TopMod ∧ 𝐹 ∈ TopDRing))
Theorem	tvctdrg 24542	The scalar field of a topological vector space is a topological division ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ TopVec → 𝐹 ∈ TopDRing)
Theorem	cnmpt1vsca 24543*	Continuity of scalar multiplication; analogue of cnmpt12f 24015 which cannot be used directly because ·𝑠 is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐾 = (TopOpen‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ TopMod)    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐿 Cn 𝐾))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐿 Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝐿 Cn 𝐽))
Theorem	cnmpt2vsca 24544*	Continuity of scalar multiplication; analogue of cnmpt22f 24024 which cannot be used directly because ·𝑠 is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐾 = (TopOpen‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ TopMod)    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐿 ×t 𝑀) Cn 𝐾))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐿 ×t 𝑀) Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴 · 𝐵)) ∈ ((𝐿 ×t 𝑀) Cn 𝐽))
Theorem	tlmtgp 24545	A topological vector space is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopGrp)
Theorem	tvctlm 24546	A topological vector space is a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ TopMod)
Theorem	tvclmod 24547	A topological vector space is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LMod)
Theorem	tvclvec 24548	A topological vector space is a vector space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LVec)
12.3  Uniform Structures and Spaces
12.3.1  Uniform structures
Syntax	cust 24549	Extend class notation with the class function of uniform structures.
class UnifOn
Definition	df-ust 24550*	Definition of a uniform structure. Definition 1 of [BourbakiTop1] p. II.1. A uniform structure is used to give a generalization of the idea of Cauchy's sequence. This definition is analogous to TopOn. Elements of an uniform structure are called entourages. (Contributed by FL, 29-May-2014.) (Revised by Thierry Arnoux, 15-Nov-2017.)
⊢ UnifOn = (𝑥 ∈ V ↦ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))})
Theorem	ustfn 24551	The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017.)
⊢ UnifOn Fn V
Theorem	ustval 24552*	The class of all uniform structures for a base 𝑋. (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.)
⊢ (𝑋 ∈ 𝑉 → (UnifOn‘𝑋) = {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))})
Theorem	isust 24553*	The predicate "𝑈 is a uniform structure with base 𝑋". (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.)
⊢ (𝑋 ∈ 𝑉 → (𝑈 ∈ (UnifOn‘𝑋) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣)))))
Theorem	ustssxp 24554	Entourages are subsets of the Cartesian product of the base set. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → 𝑉 ⊆ (𝑋 × 𝑋))
Theorem	ustssel 24555	A uniform structure is upward closed. Condition FI of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.) (Proof shortened by AV, 17-Sep-2021.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ (𝑋 × 𝑋)) → (𝑉 ⊆ 𝑊 → 𝑊 ∈ 𝑈))
Theorem	ustbasel 24556	The full set is always an entourage. Condition FIIb of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
Theorem	ustincl 24557	A uniform structure is closed under finite intersection. Condition FII of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 30-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ∈ 𝑈) → (𝑉 ∩ 𝑊) ∈ 𝑈)
Theorem	ustdiag 24558	The diagonal set is included in any entourage, i.e. any point is 𝑉 -close to itself. Condition UI of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ( I ↾ 𝑋) ⊆ 𝑉)
Theorem	ustinvel 24559	If 𝑉 is an entourage, so is its inverse. Condition UII of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ◡𝑉 ∈ 𝑈)
Theorem	ustexhalf 24560*	For each entourage 𝑉 there is an entourage 𝑤 that is "not more than half as large". Condition UIII of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑉)
Theorem	ustrel 24561	The elements of uniform structures, called entourages, are relations. (Contributed by Thierry Arnoux, 15-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → Rel 𝑉)
Theorem	ustfilxp 24562	A uniform structure on a nonempty base is a filter. Remark 3 of [BourbakiTop1] p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → 𝑈 ∈ (Fil‘(𝑋 × 𝑋)))
Theorem	ustne0 24563	A uniform structure cannot be empty. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ≠ ∅)
Theorem	ustssco 24564	In an uniform structure, any entourage 𝑉 is a subset of its composition with itself. (Contributed by Thierry Arnoux, 5-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → 𝑉 ⊆ (𝑉 ∘ 𝑉))
Theorem	ustexsym 24565*	In an uniform structure, for any entourage 𝑉, there exists a smaller symmetrical entourage. (Contributed by Thierry Arnoux, 4-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑉))
Theorem	ustex2sym 24566*	In an uniform structure, for any entourage 𝑉, there exists a symmetrical entourage smaller than half 𝑉. (Contributed by Thierry Arnoux, 16-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑉))
Theorem	ustex3sym 24567*	In an uniform structure, for any entourage 𝑉, there exists a symmetrical entourage smaller than a third of 𝑉. (Contributed by Thierry Arnoux, 16-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ (𝑤 ∘ (𝑤 ∘ 𝑤)) ⊆ 𝑉))
Theorem	ustref 24568	Any element of the base set is "near" itself, i.e. entourages are reflexive. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋) → 𝐴𝑉𝐴)
Theorem	ust0 24569	The unique uniform structure of the empty set is the empty set. Remark 3 of [BourbakiTop1] p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017.)
⊢ (UnifOn‘∅) = {{∅}}
Theorem	ustn0 24570	The empty set is not an uniform structure. (Contributed by Thierry Arnoux, 3-Dec-2017.)
⊢ ¬ ∅ ∈ ∪ ran UnifOn
Theorem	ustund 24571	If two intersecting sets 𝐴 and 𝐵 are both small in 𝑉, their union is small in (𝑉↑2). Proposition 1 of [BourbakiTop1] p. II.12. This proposition actually does not require any axiom of the definition of uniform structures. (Contributed by Thierry Arnoux, 17-Nov-2017.)
⊢ (𝜑 → (𝐴 × 𝐴) ⊆ 𝑉)    &   ⊢ (𝜑 → (𝐵 × 𝐵) ⊆ 𝑉)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ≠ ∅)    ⇒   ⊢ (𝜑 → ((𝐴 ∪ 𝐵) × (𝐴 ∪ 𝐵)) ⊆ (𝑉 ∘ 𝑉))
Theorem	ustelimasn 24572	Any point 𝐴 is near enough to itself. (Contributed by Thierry Arnoux, 18-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ (𝑉 “ {𝐴}))
Theorem	ustneism 24573	For a point 𝐴 in 𝑋, (𝑉 “ {𝐴}) is small enough in (𝑉 ∘ ◡𝑉). This proposition actually does not require any axiom of the definition of uniform structures. (Contributed by Thierry Arnoux, 18-Nov-2017.)
⊢ ((𝑉 ⊆ (𝑋 × 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑉 “ {𝐴}) × (𝑉 “ {𝐴})) ⊆ (𝑉 ∘ ◡𝑉))
Theorem	ustbas2 24574	Second direction for ustbas 24576. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = dom ∪ 𝑈)
Theorem	ustuni 24575	The set union of a uniform structure is the Cartesian product of its base. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ 𝑈 = (𝑋 × 𝑋))
Theorem	ustbas 24576	Recover the base of an uniform structure 𝑈. ∪ ran UnifOn is to UnifOn what Top is to TopOn. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ 𝑋 = dom ∪ 𝑈    ⇒   ⊢ (𝑈 ∈ ∪ ran UnifOn ↔ 𝑈 ∈ (UnifOn‘𝑋))
Theorem	ustimasn 24577	Lemma for ustuqtop 24595. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋) → (𝑉 “ {𝑃}) ⊆ 𝑋)
Theorem	trust 24578	The trace of a uniform structure 𝑈 on a subset 𝐴 is a uniform structure on 𝐴. Definition 3 of [BourbakiTop1] p. II.9. (Contributed by Thierry Arnoux, 2-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))
12.3.2  The topology induced by an uniform structure
Syntax	cutop 24579	Extend class notation with the function inducing a topology from a uniform structure.
class unifTop
Definition	df-utop 24580*	Definition of a topology induced by a uniform structure. Definition 3 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017.)
⊢ unifTop = (𝑢 ∈ ∪ ran UnifOn ↦ {𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
Theorem	utopval 24581*	The topology induced by a uniform structure 𝑈. (Contributed by Thierry Arnoux, 30-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎})
Theorem	elutop 24582*	Open sets in the topology induced by an uniform structure 𝑈 on 𝑋 (Contributed by Thierry Arnoux, 30-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴)))
Theorem	utoptop 24583	The topology induced by a uniform structure 𝑈 is a topology. (Contributed by Thierry Arnoux, 30-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ Top)
Theorem	utopbas 24584	The base of the topology induced by a uniform structure 𝑈. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪ (unifTop‘𝑈))
Theorem	utoptopon 24585	Topology induced by a uniform structure 𝑈 with its base set. (Contributed by Thierry Arnoux, 5-Jan-2018.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ (TopOn‘𝑋))
Theorem	restutop 24586	Restriction of a topology induced by an uniform structure. (Contributed by Thierry Arnoux, 12-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))))
Theorem	restutopopn 24587	The restriction of the topology induced by an uniform structure to an open set. (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → ((unifTop‘𝑈) ↾t 𝐴) = (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))))
Theorem	ustuqtoplem 24588*	Lemma for ustuqtop 24595. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ (𝑁‘𝑃) ↔ ∃𝑤 ∈ 𝑈 𝐴 = (𝑤 “ {𝑃})))
Theorem	ustuqtop0 24589*	Lemma for ustuqtop 24595. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁:𝑋⟶𝒫 𝒫 𝑋)
Theorem	ustuqtop1 24590*	Lemma for ustuqtop 24595, similar to ssnei2 23464. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))
Theorem	ustuqtop2 24591*	Lemma for ustuqtop 24595. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))
Theorem	ustuqtop3 24592*	Lemma for ustuqtop 24595, similar to elnei 23459. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)
Theorem	ustuqtop4 24593*	Lemma for ustuqtop 24595. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
Theorem	ustuqtop5 24594*	Lemma for ustuqtop 24595. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))
Theorem	ustuqtop 24595*	For a given uniform structure 𝑈 on a set 𝑋, there is a unique topology 𝑗 such that the set ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) is the filter of the neighborhoods of 𝑝 for that topology. Proposition 1 of [BourbakiTop1] p. II.3. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∃!𝑗 ∈ (TopOn‘𝑋)∀𝑝 ∈ 𝑋 (𝑁‘𝑝) = ((nei‘𝑗)‘{𝑝}))
Theorem	utopsnneiplem 24596*	The neighborhoods of a point 𝑃 for the topology induced by an uniform space 𝑈. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    &   ⊢ 𝐾 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}    &   ⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
Theorem	utopsnneip 24597*	The neighborhoods of a point 𝑃 for the topology induced by an uniform space 𝑈. (Contributed by Thierry Arnoux, 13-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
Theorem	utopsnnei 24598	Images of singletons by entourages 𝑉 are neighborhoods of those singletons. (Contributed by Thierry Arnoux, 13-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋) → (𝑉 “ {𝑃}) ∈ ((nei‘𝐽)‘{𝑃}))
Theorem	utop2nei 24599	For any symmetrical entourage 𝑉 and any relation 𝑀, build a neighborhood of 𝑀. First part of proposition 2 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 14-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×t 𝐽))‘𝑀))
Theorem	utop3cls 24600	Relation between a topological closure and a symmetric entourage in an uniform space. Second part of proposition 2 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝑉 ∘ (𝑀 ∘ 𝑉)))