P. 247 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24601-24700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	reldmnmhm 24601	Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ Rel dom NMHom
Theorem	nmofval 24602*	Value of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 26-Sep-2020.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → 𝑁 = (𝑓 ∈ (𝑆 GrpHom 𝑇) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ 𝑉 (𝑀‘(𝑓‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥))}, ℝ*, < )))
Theorem	nmoval 24603*	Value of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 26-Sep-2020.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝑁‘𝐹) = inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ 𝑉 (𝑀‘(𝐹‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥))}, ℝ*, < ))
Theorem	nmogelb 24604*	Property of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    ⇒   ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝐴 ∈ ℝ*) → (𝐴 ≤ (𝑁‘𝐹) ↔ ∀𝑟 ∈ (0[,)+∞)(∀𝑥 ∈ 𝑉 (𝑀‘(𝐹‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥)) → 𝐴 ≤ 𝑟)))
Theorem	nmolb 24605*	Any upper bound on the values of a linear operator translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    ⇒   ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (∀𝑥 ∈ 𝑉 (𝑀‘(𝐹‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) → (𝑁‘𝐹) ≤ 𝐴))
Theorem	nmolb2d 24606*	Any upper bound on the values of a linear operator at nonzero vectors translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ NrmGrp)    &   ⊢ (𝜑 → 𝑇 ∈ NrmGrp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → (𝑀‘(𝐹‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)))    ⇒   ⊢ (𝜑 → (𝑁‘𝐹) ≤ 𝐴)
Theorem	nmof 24607	The operator norm is a function into the extended reals. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → 𝑁:(𝑆 GrpHom 𝑇)⟶ℝ*)
Theorem	nmocl 24608	The operator norm of an operator is an extended real. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝑁‘𝐹) ∈ ℝ*)
Theorem	nmoge0 24609	The operator norm of an operator is nonnegative. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → 0 ≤ (𝑁‘𝐹))
Theorem	nghmfval 24610	A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (𝑆 NGHom 𝑇) = (◡𝑁 “ ℝ)
Theorem	isnghm 24611	A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑁‘𝐹) ∈ ℝ)))
Theorem	isnghm2 24612	A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ (𝑁‘𝐹) ∈ ℝ))
Theorem	isnghm3 24613	A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ (𝑁‘𝐹) < +∞))
Theorem	bddnghm 24614	A bounded group homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝐴 ∈ ℝ ∧ (𝑁‘𝐹) ≤ 𝐴)) → 𝐹 ∈ (𝑆 NGHom 𝑇))
Theorem	nghmcl 24615	A normed group homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → (𝑁‘𝐹) ∈ ℝ)
Theorem	nmoi 24616	The operator norm achieves the minimum of the set of upper bounds, if the operator is bounded. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) · (𝐿‘𝑋)))
Theorem	nmoix 24617	The operator norm is a bound on the size of an operator, even when it is infinite (using extended real multiplication). (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    ⇒   ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) ·e (𝐿‘𝑋)))
Theorem	nmoi2 24618	The operator norm is a bound on the growth of a vector under the action of the operator. (Contributed by Mario Carneiro, 19-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    ⇒   ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 )) → ((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ≤ (𝑁‘𝐹))
Theorem	nmoleub 24619*	The operator norm, defined as an infimum of upper bounds, can also be defined as a supremum of norms of 𝐹(𝑥) away from zero. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐿 = (norm‘𝑆)    &   ⊢ 𝑀 = (norm‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ NrmGrp)    &   ⊢ (𝜑 → 𝑇 ∈ NrmGrp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 (𝑥 ≠ 0 → ((𝑀‘(𝐹‘𝑥)) / (𝐿‘𝑥)) ≤ 𝐴)))
Theorem	nghmrcl1 24620	Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑆 ∈ NrmGrp)
Theorem	nghmrcl2 24621	Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑇 ∈ NrmGrp)
Theorem	nghmghm 24622	A normed group homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	nmo0 24623	The operator norm of the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑁‘(𝑉 × { 0 })) = 0)
Theorem	nmoeq0 24624	The operator norm is zero only for the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → ((𝑁‘𝐹) = 0 ↔ 𝐹 = (𝑉 × { 0 })))
Theorem	nmoco 24625	An upper bound on the operator norm of a composition. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑈)    &   ⊢ 𝐿 = (𝑇 normOp 𝑈)    &   ⊢ 𝑀 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘ 𝐺)) ≤ ((𝐿‘𝐹) · (𝑀‘𝐺)))
Theorem	nghmco 24626	The composition of normed group homomorphisms is a normed group homomorphism. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NGHom 𝑈))
Theorem	nmotri 24627	Triangle inequality for the operator norm. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ + = (+g‘𝑇)    ⇒   ⊢ ((𝑇 ∈ Abel ∧ 𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘f + 𝐺)) ≤ ((𝑁‘𝐹) + (𝑁‘𝐺)))
Theorem	nghmplusg 24628	The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ + = (+g‘𝑇)    ⇒   ⊢ ((𝑇 ∈ Abel ∧ 𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝐹 ∘f + 𝐺) ∈ (𝑆 NGHom 𝑇))
Theorem	0nghm 24629	The zero operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑉 × { 0 }) ∈ (𝑆 NGHom 𝑇))
Theorem	nmoid 24630	The operator norm of the identity function on a nontrivial group. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑆)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    ⇒   ⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉) → (𝑁‘( I ↾ 𝑉)) = 1)
Theorem	idnghm 24631	The identity operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑉 = (Base‘𝑆)    ⇒   ⊢ (𝑆 ∈ NrmGrp → ( I ↾ 𝑉) ∈ (𝑆 NGHom 𝑆))
Theorem	nmods 24632	Upper bound for the distance between the values of a bounded linear operator. (Contributed by Mario Carneiro, 22-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    &   ⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 𝐶 = (dist‘𝑆)    &   ⊢ 𝐷 = (dist‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐹‘𝐴)𝐷(𝐹‘𝐵)) ≤ ((𝑁‘𝐹) · (𝐴𝐶𝐵)))
Theorem	nghmcn 24633	A normed group homomorphism is a continuous function. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝐾 = (TopOpen‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	isnmhm 24634	A normed module homomorphism is a left module homomorphism which is also a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod) ∧ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇))))
Theorem	nmhmrcl1 24635	Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑆 ∈ NrmMod)
Theorem	nmhmrcl2 24636	Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑇 ∈ NrmMod)
Theorem	nmhmlmhm 24637	A normed module homomorphism is a left module homomorphism (a linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 LMHom 𝑇))
Theorem	nmhmnghm 24638	A normed module homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 NGHom 𝑇))
Theorem	nmhmghm 24639	A normed module homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	isnmhm2 24640	A normed module homomorphism is a left module homomorphism with bounded norm (a bounded linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝑁‘𝐹) ∈ ℝ))
Theorem	nmhmcl 24641	A normed module homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.)
⊢ 𝑁 = (𝑆 normOp 𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → (𝑁‘𝐹) ∈ ℝ)
Theorem	idnmhm 24642	The identity operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑉 = (Base‘𝑆)    ⇒   ⊢ (𝑆 ∈ NrmMod → ( I ↾ 𝑉) ∈ (𝑆 NMHom 𝑆))
Theorem	0nmhm 24643	The zero operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑉 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐹 = (Scalar‘𝑆)    &   ⊢ 𝐺 = (Scalar‘𝑇)    ⇒   ⊢ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 = 𝐺) → (𝑉 × { 0 }) ∈ (𝑆 NMHom 𝑇))
Theorem	nmhmco 24644	The composition of bounded linear operators is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ ((𝐹 ∈ (𝑇 NMHom 𝑈) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NMHom 𝑈))
Theorem	nmhmplusg 24645	The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ + = (+g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 NMHom 𝑇) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘f + 𝐺) ∈ (𝑆 NMHom 𝑇))
12.4.10  Topology on the reals
Theorem	qtopbaslem 24646	The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ 𝑆 ⊆ ℝ*    ⇒   ⊢ ((,) “ (𝑆 × 𝑆)) ∈ TopBases
Theorem	qtopbas 24647	The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.)
⊢ ((,) “ (ℚ × ℚ)) ∈ TopBases
Theorem	retopbas 24648	A basis for the standard topology on the reals. (Contributed by NM, 6-Feb-2007.) (Proof shortened by Mario Carneiro, 17-Jun-2014.)
⊢ ran (,) ∈ TopBases
Theorem	retop 24649	The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
⊢ (topGen‘ran (,)) ∈ Top
Theorem	uniretop 24650	The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.)
⊢ ℝ = ∪ (topGen‘ran (,))
Theorem	retopon 24651	The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
Theorem	retps 24652	The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐾 = {⟨(Base‘ndx), ℝ⟩, ⟨(TopSet‘ndx), (topGen‘ran (,))⟩}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	iooretop 24653	Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.)
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
Theorem	icccld 24654	Closed intervals are closed sets of the standard topology on ℝ. (Contributed by FL, 14-Sep-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ (Clsd‘(topGen‘ran (,))))
Theorem	icopnfcld 24655	Right-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ (Clsd‘(topGen‘ran (,))))
Theorem	iocmnfcld 24656	Left-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ (𝐴 ∈ ℝ → (-∞(,]𝐴) ∈ (Clsd‘(topGen‘ran (,))))
Theorem	qdensere 24657	ℚ is dense in the standard topology on ℝ. (Contributed by NM, 1-Mar-2007.)
⊢ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ
Theorem	cnmetdval 24658	Value of the distance function of the metric space of complex numbers. (Contributed by NM, 9-Dec-2006.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐷 = (abs ∘ − )    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵)))
Theorem	cnmet 24659	The absolute value metric determines a metric space on the complex numbers. This theorem provides a link between complex numbers and metrics spaces, making metric space theorems available for use with complex numbers. (Contributed by FL, 9-Oct-2006.)
⊢ (abs ∘ − ) ∈ (Met‘ℂ)
Theorem	cnxmet 24660	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
Theorem	cnbl0 24661	Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐷 = (abs ∘ − )    ⇒   ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,)𝑅)) = (0(ball‘𝐷)𝑅))
Theorem	cnblcld 24662*	Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐷 = (abs ∘ − )    ⇒   ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,]𝑅)) = {𝑥 ∈ ℂ ∣ (0𝐷𝑥) ≤ 𝑅})
Theorem	cnfldms 24663	The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ ℂfld ∈ MetSp
Theorem	cnfldxms 24664	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ ℂfld ∈ ∞MetSp
Theorem	cnfldtps 24665	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ ℂfld ∈ TopSp
Theorem	cnfldnm 24666	The norm of the field of complex numbers. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ abs = (norm‘ℂfld)
Theorem	cnngp 24667	The complex numbers form a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ ℂfld ∈ NrmGrp
Theorem	cnnrg 24668	The complex numbers form a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ ℂfld ∈ NrmRing
Theorem	cnfldtopn 24669	The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
Theorem	cnfldtopon 24670	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ (TopOn‘ℂ)
Theorem	cnfldtop 24671	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ Top
Theorem	cnfldhaus 24672	The topology of the complex numbers is Hausdorff. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ Haus
Theorem	unicntop 24673	The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ℂ = ∪ (TopOpen‘ℂfld)
Theorem	cnopn 24674	The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ℂ ∈ (TopOpen‘ℂfld)
Theorem	cnn0opn 24675	The set of nonzero complex numbers is open with respect to the standard topology on complex numbers. (Contributed by SN, 7-Oct-2025.)
⊢ (ℂ ∖ {0}) ∈ (TopOpen‘ℂfld)
Theorem	zringnrg 24676	The ring of integers is a normed ring. (Contributed by AV, 13-Jun-2019.)
⊢ ℤring ∈ NrmRing
Theorem	remetdval 24677	Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵)))
Theorem	remet 24678	The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ 𝐷 ∈ (Met‘ℝ)
Theorem	rexmet 24679	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ 𝐷 ∈ (∞Met‘ℝ)
Theorem	bl2ioo 24680	A ball in terms of an open interval of reals. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(ball‘𝐷)𝐵) = ((𝐴 − 𝐵)(,)(𝐴 + 𝐵)))
Theorem	ioo2bl 24681	An open interval of reals in terms of a ball. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) = (((𝐴 + 𝐵) / 2)(ball‘𝐷)((𝐵 − 𝐴) / 2)))
Theorem	ioo2blex 24682	An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) ∈ ran (ball‘𝐷))
Theorem	blssioo 24683	The balls of the standard real metric space are included in the open real intervals. (Contributed by NM, 8-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ran (ball‘𝐷) ⊆ ran (,)
Theorem	tgioo 24684	The topology generated by open intervals of reals is the same as the open sets of the standard metric space on the reals. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (topGen‘ran (,)) = 𝐽
Theorem	qdensere2 24685	ℚ is dense in ℝ. (Contributed by NM, 24-Aug-2007.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((cls‘𝐽)‘ℚ) = ℝ
Theorem	blcvx 24686	An open ball in the complex numbers is a convex set. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
⊢ 𝑆 = (𝑃(ball‘(abs ∘ − ))𝑅)    ⇒   ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ 𝑆)
Theorem	rehaus 24687	The standard topology on the reals is Hausdorff. (Contributed by NM, 8-Mar-2007.)
⊢ (topGen‘ran (,)) ∈ Haus
Theorem	tgqioo 24688	The topology generated by open intervals of reals with rational endpoints is the same as the open sets of the standard metric space on the reals. In particular, this proves that the standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ 𝑄 = (topGen‘((,) “ (ℚ × ℚ)))    ⇒   ⊢ (topGen‘ran (,)) = 𝑄
Theorem	re2ndc 24689	The standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (topGen‘ran (,)) ∈ 2ndω
Theorem	resubmet 24690	The subspace topology induced by a subset of the reals. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Aug-2014.)
⊢ 𝑅 = (topGen‘ran (,))    &   ⊢ 𝐽 = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴)))    ⇒   ⊢ (𝐴 ⊆ ℝ → 𝐽 = (𝑅 ↾t 𝐴))
Theorem	tgioo2 24691	The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (topGen‘ran (,)) = (𝐽 ↾t ℝ)
Theorem	rerest 24692	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑅 = (topGen‘ran (,))    ⇒   ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑅 ↾t 𝐴))
Theorem	tgioo4 24693	The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
Theorem	tgioo3 24694	The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Thierry Arnoux, 3-Jul-2019.)
⊢ 𝐽 = (TopOpen‘ℝfld)    ⇒   ⊢ (topGen‘ran (,)) = 𝐽
Theorem	xrtgioo 24695	The topology on the extended reals coincides with the standard topology on the reals, when restricted to ℝ. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t ℝ)    ⇒   ⊢ (topGen‘ran (,)) = 𝐽
Theorem	xrrest 24696	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = (ordTop‘ ≤ )    &   ⊢ 𝑅 = (topGen‘ran (,))    ⇒   ⊢ (𝐴 ⊆ ℝ → (𝑋 ↾t 𝐴) = (𝑅 ↾t 𝐴))
Theorem	xrrest2 24697	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑋 = (ordTop‘ ≤ )    ⇒   ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑋 ↾t 𝐴))
Theorem	xrsxmet 24698	The metric on the extended reals is a proper extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ 𝐷 ∈ (∞Met‘ℝ*)
Theorem	xrsdsre 24699	The metric on the extended reals coincides with the usual metric on the reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ (𝐷 ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
Theorem	xrsblre 24700	Any ball of the metric of the extended reals centered on an element of ℝ is entirely contained in ℝ. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ ((𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ⊆ ℝ)