P. 345 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34401-34500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rspectps 34401	The spectrum of a ring 𝑅 is a topological space. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑆 ∈ TopSp)
Theorem	rhmpreimacnlem 34402*	Lemma for rhmpreimacn 34403. (Contributed by Thierry Arnoux, 7-Jul-2024.)
⊢ 𝑇 = (Spec‘𝑅)    &   ⊢ 𝑈 = (Spec‘𝑆)    &   ⊢ 𝐴 = (PrmIdeal‘𝑅)    &   ⊢ 𝐵 = (PrmIdeal‘𝑆)    &   ⊢ 𝐽 = (TopOpen‘𝑇)    &   ⊢ 𝐾 = (TopOpen‘𝑈)    &   ⊢ 𝐺 = (𝑖 ∈ 𝐵 ↦ (◡𝐹 “ 𝑖))    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → ran 𝐹 = (Base‘𝑆))    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ 𝑉 = (𝑗 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘})    &   ⊢ 𝑊 = (𝑗 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘})    ⇒   ⊢ (𝜑 → (𝑊‘(𝐹 “ 𝐼)) = (◡𝐺 “ (𝑉‘𝐼)))
Theorem	rhmpreimacn 34403*	The function mapping a prime ideal to its preimage by a surjective ring homomorphism is continuous, when considering the Zariski topology. Corollary 1.2.3 of [EGA], p. 83. Notice that the direction of the continuous map 𝐺 is reverse: the original ring homomorphism 𝐹 goes from 𝑅 to 𝑆, but the continuous map 𝐺 goes from 𝐵 to 𝐴. This mapping is also called "induced map on prime spectra" or "pullback on primes". (Contributed by Thierry Arnoux, 8-Jul-2024.)
⊢ 𝑇 = (Spec‘𝑅)    &   ⊢ 𝑈 = (Spec‘𝑆)    &   ⊢ 𝐴 = (PrmIdeal‘𝑅)    &   ⊢ 𝐵 = (PrmIdeal‘𝑆)    &   ⊢ 𝐽 = (TopOpen‘𝑇)    &   ⊢ 𝐾 = (TopOpen‘𝑈)    &   ⊢ 𝐺 = (𝑖 ∈ 𝐵 ↦ (◡𝐹 “ 𝑖))    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → ran 𝐹 = (Base‘𝑆))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))
21.3.14.8  Pseudometrics
Syntax	cmetid 34404	Extend class notation with the class of metric identifications.
class ~Met
Syntax	cpstm 34405	Extend class notation with the metric induced by a pseudometric.
class pstoMet
Definition	df-metid 34406*	Define the metric identification relation for a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ~Met = (𝑑 ∈ ∪ ran PsMet ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)})
Definition	df-pstm 34407*	Define the metric induced by a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ pstoMet = (𝑑 ∈ ∪ ran PsMet ↦ (𝑎 ∈ (dom dom 𝑑 / (~Met‘𝑑)), 𝑏 ∈ (dom dom 𝑑 / (~Met‘𝑑)) ↦ ∪ {𝑧 ∣ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑧 = (𝑥𝑑𝑦)}))
Theorem	metidval 34408*	Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)})
Theorem	metidss 34409	As a relation, the metric identification is a subset of a Cartesian product. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) ⊆ (𝑋 × 𝑋))
Theorem	metidv 34410	𝐴 and 𝐵 identify by the metric 𝐷 if their distance is zero. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴(~Met‘𝐷)𝐵 ↔ (𝐴𝐷𝐵) = 0))
Theorem	metideq 34411	Basic property of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐸) = (𝐵𝐷𝐹))
Theorem	metider 34412	The metric identification is an equivalence relation. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) Er 𝑋)
Theorem	pstmval 34413*	Value of the metric induced by a pseudometric 𝐷. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ∼ = (~Met‘𝐷)    ⇒   ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) = (𝑎 ∈ (𝑋 / ∼ ), 𝑏 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧 ∣ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑧 = (𝑥𝐷𝑦)}))
Theorem	pstmfval 34414	Function value of the metric induced by a pseudometric 𝐷 (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ∼ = (~Met‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼ (pstoMet‘𝐷)[𝐵] ∼ ) = (𝐴𝐷𝐵))
Theorem	pstmxmet 34415	The metric induced by a pseudometric is a full-fledged metric on the equivalence classes of the metric identification. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ∼ = (~Met‘𝐷)    ⇒   ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) ∈ (∞Met‘(𝑋 / ∼ )))
21.3.14.9  Continuity - misc additions
Theorem	hauseqcn 34416	In a Hausdorff topology, two continuous functions which agree on a dense set agree everywhere. (Contributed by Thierry Arnoux, 28-Dec-2017.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝑋)    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
21.3.14.10  Topology of the closed unit interval
Theorem	elunitge0 34417	An element of the closed unit interval is positive. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 20-Dec-2016.)
⊢ (𝐴 ∈ (0[,]1) → 0 ≤ 𝐴)
Theorem	unitssxrge0 34418	The closed unit interval is a subset of the set of the extended nonnegative reals. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 12-Dec-2016.)
⊢ (0[,]1) ⊆ (0[,]+∞)
Theorem	unitdivcld 34419	Necessary conditions for a quotient to be in the closed unit interval. (somewhat too strong, it would be sufficient that A and B are in RR+) (Contributed by Thierry Arnoux, 20-Dec-2016.)
⊢ ((𝐴 ∈ (0[,]1) ∧ 𝐵 ∈ (0[,]1) ∧ 𝐵 ≠ 0) → (𝐴 ≤ 𝐵 ↔ (𝐴 / 𝐵) ∈ (0[,]1)))
Theorem	iistmd 34420	The closed unit interval forms a topological monoid under multiplication. (Contributed by Thierry Arnoux, 25-Mar-2017.)
⊢ 𝐼 = ((mulGrp‘ℂfld) ↾s (0[,]1))    ⇒   ⊢ 𝐼 ∈ TopMnd
21.3.14.11  Topology of ` ( RR X. RR ) `
Theorem	unicls 34421	The union of the closed set is the underlying set of the topology. (Contributed by Thierry Arnoux, 21-Sep-2017.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ∪ (Clsd‘𝐽) = 𝑋
Theorem	tpr2tp 34422	The usual topology on (ℝ × ℝ) is the product topology of the usual topology on ℝ. (Contributed by Thierry Arnoux, 21-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    ⇒   ⊢ (𝐽 ×t 𝐽) ∈ (TopOn‘(ℝ × ℝ))
Theorem	tpr2uni 34423	The usual topology on (ℝ × ℝ) is the product topology of the usual topology on ℝ. (Contributed by Thierry Arnoux, 21-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    ⇒   ⊢ ∪ (𝐽 ×t 𝐽) = (ℝ × ℝ)
Theorem	xpinpreima 34424	Rewrite the cartesian product of two sets as the intersection of their preimage by 1st and 2nd, the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ (𝐴 × 𝐵) = ((◡(1st ↾ (V × V)) “ 𝐴) ∩ (◡(2nd ↾ (V × V)) “ 𝐵))
Theorem	xpinpreima2 34425	Rewrite the cartesian product of two sets as the intersection of their preimage by 1st and 2nd, the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → (𝐴 × 𝐵) = ((◡(1st ↾ (𝐸 × 𝐹)) “ 𝐴) ∩ (◡(2nd ↾ (𝐸 × 𝐹)) “ 𝐵)))
Theorem	sqsscirc1 34426	The complex square of side 𝐷 is a subset of the complex circle of radius 𝐷. (Contributed by Thierry Arnoux, 25-Sep-2017.)
⊢ ((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ+) → ((𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2)) → (√‘((𝑋↑2) + (𝑌↑2))) < 𝐷))
Theorem	sqsscirc2 34427	The complex square of side 𝐷 is a subset of the complex disc of radius 𝐷. (Contributed by Thierry Arnoux, 25-Sep-2017.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝐷 ∈ ℝ+) → (((abs‘(ℜ‘(𝐵 − 𝐴))) < (𝐷 / 2) ∧ (abs‘(ℑ‘(𝐵 − 𝐴))) < (𝐷 / 2)) → (abs‘(𝐵 − 𝐴)) < 𝐷))
Theorem	cnre2csqlem 34428*	Lemma for cnre2csqima 34429. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ (𝐺 ↾ (ℝ × ℝ)) = (𝐻 ∘ 𝐹)    &   ⊢ 𝐹 Fn (ℝ × ℝ)    &   ⊢ 𝐺 Fn V    &   ⊢ (𝑥 ∈ (ℝ × ℝ) → (𝐺‘𝑥) ∈ ℝ)    &   ⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝐻‘(𝑥 − 𝑦)) = ((𝐻‘𝑥) − (𝐻‘𝑦)))    ⇒   ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑌 ∈ (ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(𝐺 ↾ (ℝ × ℝ)) “ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → (abs‘(𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷))
Theorem	cnre2csqima 34429*	Image of a centered square by the canonical bijection from (ℝ × ℝ) to ℂ. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    ⇒   ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑌 ∈ (ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ ((((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷)) × (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))) → ((abs‘(ℜ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷 ∧ (abs‘(ℑ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷)))
Theorem	tpr2rico 34430*	For any point of an open set of the usual topology on (ℝ × ℝ) there is an open square which contains that point and is entirely in the open set. This is square is actually a ball by the (𝑙↑+∞) norm 𝑋. (Contributed by Thierry Arnoux, 21-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐺 = (𝑢 ∈ ℝ, 𝑣 ∈ ℝ ↦ (𝑢 + (i · 𝑣)))    &   ⊢ 𝐵 = ran (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦))    ⇒   ⊢ ((𝐴 ∈ (𝐽 ×t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑟 ∈ 𝐵 (𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴))
21.3.14.12  Order topology - misc. additions
Theorem	cnvordtrestixx 34431*	The restriction of the 'greater than' order to an interval gives the same topology as the subspace topology. (Contributed by Thierry Arnoux, 1-Apr-2017.)
⊢ 𝐴 ⊆ ℝ*    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥[,]𝑦) ⊆ 𝐴)    ⇒   ⊢ ((ordTop‘ ≤ ) ↾t 𝐴) = (ordTop‘(◡ ≤ ∩ (𝐴 × 𝐴)))
Theorem	prsdm 34432	Domain of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵)
Theorem	prsrn 34433	Range of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ (𝐾 ∈ Proset → ran ≤ = 𝐵)
Theorem	prsss 34434	Relation of a subproset. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘𝐾) ∩ (𝐴 × 𝐴)))
Theorem	prsssdm 34435	Domain of a subproset relation. (Contributed by Thierry Arnoux, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴)
Theorem	ordtprsval 34436*	Value of the order topology for a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})    &   ⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})    ⇒   ⊢ (𝐾 ∈ Proset → (ordTop‘ ≤ ) = (topGen‘(fi‘({𝐵} ∪ (𝐸 ∪ 𝐹)))))
Theorem	ordtprsuni 34437*	Value of the order topology. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})    &   ⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})    ⇒   ⊢ (𝐾 ∈ Proset → 𝐵 = ∪ ({𝐵} ∪ (𝐸 ∪ 𝐹)))
Theorem	ordtcnvNEW 34438	The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015.) (Revised by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ (𝐾 ∈ Proset → (ordTop‘◡ ≤ ) = (ordTop‘ ≤ ))
Theorem	ordtrestNEW 34439	The subspace topology of an order topology is in general finer than the topology generated by the restricted order, but we do have inclusion in one direction. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘ ≤ ) ↾t 𝐴))
Theorem	ordtrest2NEWlem 34440*	Lemma for ordtrest2NEW 34441. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
Theorem	ordtrest2NEW 34441*	An interval-closed set 𝐴 in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in ℝ, but in other sets like ℚ there are interval-closed sets like (π, +∞) ∩ ℚ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) = ((ordTop‘ ≤ ) ↾t 𝐴))
Theorem	ordtconnlem1 34442*	Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 34443. See also reconnlem1 25059. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ 𝐽 = (ordTop‘ ≤ )    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → ((𝐽 ↾t 𝐴) ∈ Conn → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)))
Theorem	ordtconn 34443	Connectedness in the order topology of a complete uniform totally ordered space. (Contributed by Thierry Arnoux, 15-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ 𝐽 = (ordTop‘ ≤ )    ⇒   ⊢ ⊤
21.3.14.13  Continuity in topological spaces - misc. additions
Theorem	mndpluscn 34444*	A mapping that is both a homeomorphism and a monoid homomorphism preserves the "continuousness" of the operation. (Contributed by Thierry Arnoux, 25-Mar-2017.)
⊢ 𝐹 ∈ (𝐽Homeo𝐾)    &   ⊢ + :(𝐵 × 𝐵)⟶𝐵    &   ⊢ ∗ :(𝐶 × 𝐶)⟶𝐶    &   ⊢ 𝐽 ∈ (TopOn‘𝐵)    &   ⊢ 𝐾 ∈ (TopOn‘𝐶)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ∗ (𝐹‘𝑦)))    &   ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)    ⇒   ⊢ ∗ ∈ ((𝐾 ×t 𝐾) Cn 𝐾)
Theorem	mhmhmeotmd 34445	Deduce a Topological Monoid using mapping that is both a homeomorphism and a monoid homomorphism. (Contributed by Thierry Arnoux, 21-Jun-2017.)
⊢ 𝐹 ∈ (𝑆 MndHom 𝑇)    &   ⊢ 𝐹 ∈ ((TopOpen‘𝑆)Homeo(TopOpen‘𝑇))    &   ⊢ 𝑆 ∈ TopMnd    &   ⊢ 𝑇 ∈ TopSp    ⇒   ⊢ 𝑇 ∈ TopMnd
Theorem	rmulccn 34446*	Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) Avoid ax-mulf 11208. (Revised by GG, 16-Mar-2025.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 · 𝐶)) ∈ (𝐽 Cn 𝐽))
Theorem	raddcn 34447*	Addition in the real numbers is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.)
⊢ 𝐽 = (topGen‘ran (,))    ⇒   ⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + 𝑦)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	xrmulc1cn 34448*	The operation multiplying an extended real number by a nonnegative constant is continuous. (Contributed by Thierry Arnoux, 5-Jul-2017.)
⊢ 𝐽 = (ordTop‘ ≤ )    &   ⊢ 𝐹 = (𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐽))
Theorem	fmcncfil 34449	The image of a Cauchy filter by a continuous filter map is a Cauchy filter. (Contributed by Thierry Arnoux, 12-Nov-2017.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = (MetOpen‘𝐸)    ⇒   ⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝐸 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝐵 ∈ (CauFil‘𝐷)) → ((𝑌 FilMap 𝐹)‘𝐵) ∈ (CauFil‘𝐸))
21.3.14.14  Topology of the extended nonnegative real numbers ordered monoid
Theorem	xrge0hmph 34450	The extended nonnegative reals are homeomorphic to the closed unit interval. (Contributed by Thierry Arnoux, 24-Mar-2017.)
⊢ II ≃ ((ordTop‘ ≤ ) ↾t (0[,]+∞))
Theorem	xrge0iifcnv 34451*	Define a bijection from [0, 1] onto [0, +∞]. (Contributed by Thierry Arnoux, 29-Mar-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    ⇒   ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,]+∞) ↦ if(𝑦 = +∞, 0, (exp‘-𝑦))))
Theorem	xrge0iifcv 34452*	The defined function's value in the real. (Contributed by Thierry Arnoux, 1-Apr-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    ⇒   ⊢ (𝑋 ∈ (0(,]1) → (𝐹‘𝑋) = -(log‘𝑋))
Theorem	xrge0iifiso 34453*	The defined bijection from the closed unit interval onto the extended nonnegative reals is an order isomorphism. (Contributed by Thierry Arnoux, 31-Mar-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    ⇒   ⊢ 𝐹 Isom < , ◡ < ((0[,]1), (0[,]+∞))
Theorem	xrge0iifhmeo 34454*	Expose a homeomorphism from the closed unit interval to the extended nonnegative reals. (Contributed by Thierry Arnoux, 1-Apr-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    &   ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    ⇒   ⊢ 𝐹 ∈ (IIHomeo𝐽)
Theorem	xrge0iifhom 34455*	The defined function from the closed unit interval to the extended nonnegative reals is a monoid homomorphism. (Contributed by Thierry Arnoux, 5-Apr-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    &   ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    ⇒   ⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0[,]1)) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) +𝑒 (𝐹‘𝑌)))
Theorem	xrge0iif1 34456*	Condition for the defined function, -(log‘𝑥) to be a monoid homomorphism. (Contributed by Thierry Arnoux, 20-Jun-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    &   ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    ⇒   ⊢ (𝐹‘1) = 0
Theorem	xrge0iifmhm 34457*	The defined function from the closed unit interval to the extended nonnegative reals is a monoid homomorphism. (Contributed by Thierry Arnoux, 21-Jun-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    &   ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    ⇒   ⊢ 𝐹 ∈ (((mulGrp‘ℂfld) ↾s (0[,]1)) MndHom (ℝ*𝑠 ↾s (0[,]+∞)))
Theorem	xrge0pluscn 34458*	The addition operation of the extended nonnegative real numbers monoid is continuous. (Contributed by Thierry Arnoux, 24-Mar-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    &   ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    &   ⊢ + = ( +𝑒 ↾ ((0[,]+∞) × (0[,]+∞)))    ⇒   ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	xrge0mulc1cn 34459*	The operation multiplying a nonnegative real numbers by a nonnegative constant is continuous. (Contributed by Thierry Arnoux, 6-Jul-2017.)
⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    &   ⊢ 𝐹 = (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐽))
Theorem	xrge0tps 34460	The extended nonnegative real numbers monoid forms a topological space. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp
Theorem	xrge0topn 34461	The topology of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 20-Jun-2017.)
⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) = ((ordTop‘ ≤ ) ↾t (0[,]+∞))
Theorem	xrge0haus 34462	The topology of the extended nonnegative real numbers is Hausdorff. (Contributed by Thierry Arnoux, 26-Jul-2017.)
⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) ∈ Haus
Theorem	xrge0tmd 34463	The extended nonnegative real numbers monoid is a topological monoid. (Contributed by Thierry Arnoux, 26-Mar-2017.) (Proof Shortened by Thierry Arnoux, 21-Jun-2017.)
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopMnd
Theorem	xrge0tmdALT 34464	Alternate proof of xrge0tmd 34463. (Contributed by Thierry Arnoux, 26-Mar-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopMnd
21.3.14.15  Limits - misc additions
Theorem	lmlim 34465	Relate a limit in a given topology to a complex number limit, provided that topology agrees with the common topology on ℂ on the required subset. (Contributed by Thierry Arnoux, 11-Jul-2017.)
⊢ 𝐽 ∈ (TopOn‘𝑌)    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    &   ⊢ (𝐽 ↾t 𝑋) = ((TopOpen‘ℂfld) ↾t 𝑋)    &   ⊢ 𝑋 ⊆ ℂ    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹 ⇝ 𝑃))
Theorem	lmlimxrge0 34466	Relate a limit in the nonnegative extended reals to a complex limit, provided the considered function is a real function. (Contributed by Thierry Arnoux, 11-Jul-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    &   ⊢ 𝑋 ⊆ (0[,)+∞)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹 ⇝ 𝑃))
Theorem	rge0scvg 34467	Implication of convergence for a nonnegative series. This could be used to shorten prmreclem6 17019. (Contributed by Thierry Arnoux, 28-Jul-2017.)
⊢ ((𝐹:ℕ⟶(0[,)+∞) ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ)
Theorem	fsumcvg4 34468	A serie with finite support is a finite sum, and therefore converges. (Contributed by Thierry Arnoux, 6-Sep-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝑆 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑆⟶ℂ)    &   ⊢ (𝜑 → (◡𝐹 “ (ℂ ∖ {0})) ∈ Fin)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Theorem	pnfneige0 34469*	A neighborhood of +∞ contains an unbounded interval based at a real number. See pnfnei 23451. (Contributed by Thierry Arnoux, 31-Jul-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    ⇒   ⊢ ((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)
Theorem	lmxrge0 34470*	Express "sequence 𝐹 converges to plus infinity" (i.e. diverges), for a sequence of nonnegative extended real numbers. (Contributed by Thierry Arnoux, 2-Aug-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    &   ⊢ (𝜑 → 𝐹:ℕ⟶(0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = 𝐴)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)+∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < 𝐴))
Theorem	lmdvg 34471*	If a monotonic sequence of real numbers diverges, it is unbounded. (Contributed by Thierry Arnoux, 4-Aug-2017.)
⊢ (𝜑 → 𝐹:ℕ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)))    &   ⊢ (𝜑 → ¬ 𝐹 ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))
Theorem	lmdvglim 34472*	If a monotonic real number sequence 𝐹 diverges, it converges in the extended real numbers and its limit is plus infinity. (Contributed by Thierry Arnoux, 3-Aug-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    &   ⊢ (𝜑 → 𝐹:ℕ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)))    &   ⊢ (𝜑 → ¬ 𝐹 ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)+∞)
21.3.14.16  Univariate polynomials
Theorem	pl1cn 34473	A univariate polynomial is continuous. (Contributed by Thierry Arnoux, 17-Sep-2018.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐸 = (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ TopRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐸‘𝐹) ∈ (𝐽 Cn 𝐽))
21.3.15  Uniform Stuctures and Spaces
21.3.15.1  Hausdorff uniform completion
Syntax	chcmp 34474	Extend class notation with the Hausdorff uniform completion relation.
class HCmp
Definition	df-hcmp 34475*	Definition of the Hausdorff completion. In this definition, a structure 𝑤 is a Hausdorff completion of a uniform structure 𝑢 if 𝑤 is a complete uniform space, in which 𝑢 is dense, and which admits the same uniform structure. Theorem 3 of [BourbakiTop1] p. II.21. states the existence and uniqueness of such a completion. (Contributed by Thierry Arnoux, 5-Mar-2018.)
⊢ HCmp = {⟨𝑢, 𝑤⟩ ∣ ((𝑢 ∈ ∪ ran UnifOn ∧ 𝑤 ∈ CUnifSp) ∧ ((UnifSt‘𝑤) ↾t dom ∪ 𝑢) = 𝑢 ∧ ((cls‘(TopOpen‘𝑤))‘dom ∪ 𝑢) = (Base‘𝑤))}
21.3.16  Topology and algebraic structures
21.3.16.1  The norm on the ring of the integer numbers
Theorem	zringnm 34476	The norm (function) for a ring of integers is the absolute value function (restricted to the integers). (Contributed by AV, 13-Jun-2019.)
⊢ (norm‘ℤring) = (abs ↾ ℤ)
Theorem	zzsnm 34477	The norm of the ring of the integers. (Contributed by Thierry Arnoux, 8-Nov-2017.) (Revised by AV, 13-Jun-2019.)
⊢ (𝑀 ∈ ℤ → (abs‘𝑀) = ((norm‘ℤring)‘𝑀))
21.3.16.2  Topological ` ZZ ` -modules
Theorem	zlm0 34478	Zero of a ℤ-module. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ 0 = (0g‘𝑊)
Theorem	zlm1 34479	Unity element of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 1 = (1r‘𝐺)    ⇒   ⊢ 1 = (1r‘𝑊)
Theorem	zlmds 34480	Distance in a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) (Proof shortened by AV, 11-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝐷 = (dist‘𝑊))
Theorem	zlmtset 34481	Topology in a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) (Proof shortened by AV, 12-Nov-2024.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝐽 = (TopSet‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝐽 = (TopSet‘𝑊))
Theorem	zlmnm 34482	Norm of a ℤ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝑁 = (norm‘𝑊))
Theorem	zhmnrg 34483	The ℤ-module built from a normed ring is also a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝑊 = (ℤMod‘𝐺)    ⇒   ⊢ (𝐺 ∈ NrmRing → 𝑊 ∈ NrmRing)
Theorem	nmmulg 34484	The norm of a group product, provided the ℤ-module is normed. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ 𝑍 = (ℤMod‘𝑅)    &   ⊢ · = (.g‘𝑅)    ⇒   ⊢ ((𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁‘(𝑀 · 𝑋)) = ((abs‘𝑀) · (𝑁‘𝑋)))
Theorem	zrhnm 34485	The norm of the image by ℤRHom of an integer in a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑁 = (norm‘𝑅)    &   ⊢ 𝑍 = (ℤMod‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (((𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ 𝑀 ∈ ℤ) → (𝑁‘(𝐿‘𝑀)) = (abs‘𝑀))
Theorem	cnzh 34486	The ℤ-module of ℂ is a normed module. (Contributed by Thierry Arnoux, 25-Feb-2018.)
⊢ (ℤMod‘ℂfld) ∈ NrmMod
Theorem	rezh 34487	The ℤ-module of ℝ is a normed module. (Contributed by Thierry Arnoux, 14-Feb-2018.)
⊢ (ℤMod‘ℝfld) ∈ NrmMod
21.3.16.3  Canonical embedding of the field of the rational numbers into a division ring
Syntax	cqqh 34488	Map the rationals into a field.
class ℚHom
Definition	df-qqh 34489*	Define the canonical homomorphism from the rationals into any field. (Contributed by Mario Carneiro, 22-Oct-2017.) (Revised by Thierry Arnoux, 23-Oct-2017.)
⊢ ℚHom = (𝑟 ∈ V ↦ ran (𝑥 ∈ ℤ, 𝑦 ∈ (◡(ℤRHom‘𝑟) “ (Unit‘𝑟)) ↦ ⟨(𝑥 / 𝑦), (((ℤRHom‘𝑟)‘𝑥)(/r‘𝑟)((ℤRHom‘𝑟)‘𝑦))⟩))
Theorem	qqhval 34490*	Value of the canonical homormorphism from the rational number to a field. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ / = (/r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (𝑅 ∈ V → (ℚHom‘𝑅) = ran (𝑥 ∈ ℤ, 𝑦 ∈ (◡𝐿 “ (Unit‘𝑅)) ↦ ⟨(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))⟩))
Theorem	zrhf1ker 34491	The kernel of the homomorphism from the integers to a ring, if it is injective. (Contributed by Thierry Arnoux, 26-Oct-2017.) (Revised by Thierry Arnoux, 23-May-2023.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐿:ℤ–1-1→𝐵 ↔ (◡𝐿 “ { 0 }) = {0}))
Theorem	zrhchr 34492	The kernel of the homomorphism from the integers to a ring is injective if and only if the ring has characteristic 0 . (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → ((chr‘𝑅) = 0 ↔ 𝐿:ℤ–1-1→𝐵))
Theorem	zrhker 34493	The kernel of the homomorphism from the integers to a ring with characteristic 0. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → ((chr‘𝑅) = 0 ↔ (◡𝐿 “ { 0 }) = {0}))
Theorem	zrhunitpreima 34494	The preimage by ℤRHom of the units of a division ring is (ℤ ∖ {0}). (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (◡𝐿 “ (Unit‘𝑅)) = (ℤ ∖ {0}))
Theorem	elzrhunit 34495	Condition for the image by ℤRHom to be a unit. (Contributed by Thierry Arnoux, 30-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → (𝐿‘𝑀) ∈ (Unit‘𝑅))
Theorem	zrhneg 34496	The canonical homomorphism from the integers to a ring 𝑅 maps additive inverses to additive inverses. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ 𝐼 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐿‘-𝑁) = (𝐼‘(𝐿‘𝑁)))
Theorem	zrhcntr 34497	The canonical representation of an integer 𝑁 in a ring 𝑅 is in the centralizer of the ring's multiplicative monoid. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝐶 = (Cntr‘𝑀)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐿‘𝑁) ∈ 𝐶)
Theorem	elzdif0 34498	Lemma for qqhval2 34500. (Contributed by Thierry Arnoux, 29-Oct-2017.)
⊢ (𝑀 ∈ (ℤ ∖ {0}) → (𝑀 ∈ ℕ ∨ -𝑀 ∈ ℕ))
Theorem	qqhval2lem 34499	Lemma for qqhval2 34500. (Contributed by Thierry Arnoux, 29-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0)) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌)))
Theorem	qqhval2 34500*	Value of the canonical homormorphism from the rational number when the target ring is a division ring. (Contributed by Thierry Arnoux, 26-Oct-2017.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝐿 = (ℤRHom‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅) = (𝑞 ∈ ℚ ↦ ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))