P. 301 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30001-30100   *Has distinct variable group(s)

Type	Label	Description
Statement
20.3.11.15  Univariate polynomials
Theorem	pl1cn 30001	A univariate polynomial is continuous. (Contributed by Thierry Arnoux, 17-Sep-2018.)
|- P = (Poly1 ` R )   &    |- E = (eval1 ` R )   &    |- B = ( Base ` P )   &    |- K = ( Base ` R )   &    |- J = ( TopOpen ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> R e. TopRing )   &    |- ( ph -> F e. B )   =>    |- ( ph -> ( E ` F ) e. ( J Cn J ) )
20.3.12  Uniform Stuctures and Spaces
20.3.12.1  Hausdorff uniform completion
Syntax	chcmp 30002	Extend class notation with the Hausdorff uniform completion relation.
class HCmp
Definition	df-hcmp 30003*	Definition of the Hausdorff completion. In this definition, a structure w is a Hausdorff completion of a uniform structure u if w is a complete uniform space, in which u is dense, and which admits the same uniform structure. Theorem 3 of [BourbakiTop1] p. II.21. states the existence and unicity of such a completion. (Contributed by Thierry Arnoux, 5-Mar-2018.)
|- HCmp = { <. u , w >. | ( ( u e. U. ran UnifOn /\ w e. CUnifSp ) /\ ( (UnifSt ` w ) ↾t dom U. u ) = u /\ ( ( cls ` ( TopOpen ` w ) ) ` dom U. u ) = ( Base ` w ) ) }
20.3.13  Topology and algebraic structures
20.3.13.1  The norm on the ring of the integer numbers
Theorem	zringnm 30004	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 |` ZZ )
Theorem	zzsnm 30005	The norm of the ring of the integers. (Contributed by Thierry Arnoux, 8-Nov-2017.) (Revised by AV, 13-Jun-2019.)
|- ( M e. ZZ -> ( abs ` M ) = ( ( norm ` ℤring ) ` M ) )
20.3.13.2  Topological ` ZZ ` -modules
Theorem	zlm0 30006	Zero of a ZZ-module. (Contributed by Thierry Arnoux, 8-Nov-2017.)
|- W = ( ZMod ` G )   &    |- .0. = ( 0g ` G )   =>    |- .0. = ( 0g ` W )
Theorem	zlm1 30007	Unit of a ZZ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.)
|- W = ( ZMod ` G )   &    |- .1. = ( 1r ` G )   =>    |- .1. = ( 1r ` W )
Theorem	zlmds 30008	Distance in a ZZ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.)
|- W = ( ZMod ` G )   &    |- D = ( dist ` G )   =>    |- ( G e. V -> D = ( dist ` W ) )
Theorem	zlmtset 30009	Topology in a ZZ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.)
|- W = ( ZMod ` G )   &    |- J = (TopSet ` G )   =>    |- ( G e. V -> J = (TopSet ` W ) )
Theorem	zlmnm 30010	Norm of a ZZ-module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.)
|- W = ( ZMod ` G )   &    |- N = ( norm ` G )   =>    |- ( G e. V -> N = ( norm ` W ) )
Theorem	zhmnrg 30011	The ZZ-module built from a normed ring is also a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017.)
|- W = ( ZMod ` G )   =>    |- ( G e. NrmRing -> W e. NrmRing )
Theorem	nmmulg 30012	The norm of a group product, provided the ZZ-module is normed. (Contributed by Thierry Arnoux, 8-Nov-2017.)
|- B = ( Base ` R )   &    |- N = ( norm ` R )   &    |- Z = ( ZMod ` R )   &    |- .x. = (.g ` R )   =>    |- ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> ( N ` ( M .x. X ) ) = ( ( abs ` M ) x. ( N ` X ) ) )
Theorem	zrhnm 30013	The norm of the image by ZRHom of an integer in a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017.)
|- B = ( Base ` R )   &    |- N = ( norm ` R )   &    |- Z = ( ZMod ` R )   &    |- L = ( ZRHom ` R )   =>    |- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> ( N ` ( L ` M ) ) = ( abs ` M ) )
Theorem	cnzh 30014	The ZZ-module of CC is a normed module. (Contributed by Thierry Arnoux, 25-Feb-2018.)
|- ( ZMod ` ℂfld ) e. NrmMod
Theorem	rezh 30015	The ZZ-module of RR is a normed module. (Contributed by Thierry Arnoux, 14-Feb-2018.)
|- ( ZMod ` RRfld ) e. NrmMod
20.3.13.3  Canonical embedding of the field of the rational numbers into a division ring
Syntax	cqqh 30016	Map the rationals into a field.
class QQHom
Definition	df-qqh 30017*	Define the canonical homomorphism from the rationals into any field. (Contributed by Mario Carneiro, 22-Oct-2017.) (Revised by Thierry Arnoux, 23-Oct-2017.)
|- QQHom = ( r e. _V |-> ran ( x e. ZZ , y e. ( `' ( ZRHom ` r ) " (Unit ` r ) ) |-> <. ( x / y ) , ( ( ( ZRHom ` r ) ` x ) (/r ` r ) ( ( ZRHom ` r ) ` y ) ) >. ) )
Theorem	qqhval 30018*	Value of the canonical homormorphism from the rational number to a field. (Contributed by Thierry Arnoux, 22-Oct-2017.)
|- ./ = (/r ` R )   &    |- .1. = ( 1r ` R )   &    |- L = ( ZRHom ` R )   =>    |- ( R e. _V -> (QQHom ` R ) = ran ( x e. ZZ , y e. ( `' L " (Unit ` R ) ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) )
Theorem	zrhf1ker 30019	The kernel of the homomorphism from the integers to a ring, if it is injective. (Contributed by Thierry Arnoux, 26-Oct-2017.)
|- B = ( Base ` R )   &    |- L = ( ZRHom ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> ( L : ZZ -1-1-> B <-> ( `' L " { .0. } ) = { 0 } ) )
Theorem	zrhchr 30020	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.)
|- B = ( Base ` R )   &    |- L = ( ZRHom ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> ( (chr ` R ) = 0 <-> L : ZZ -1-1-> B ) )
Theorem	zrhker 30021	The kernel of the homomorphism from the integers to a ring with characteristic 0. (Contributed by Thierry Arnoux, 8-Nov-2017.)
|- B = ( Base ` R )   &    |- L = ( ZRHom ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> ( (chr ` R ) = 0 <-> ( `' L " { .0. } ) = { 0 } ) )
Theorem	zrhunitpreima 30022	The preimage by ZRHom of the unit of a division ring is ( ZZ \ { 0 } ). (Contributed by Thierry Arnoux, 22-Oct-2017.)
|- B = ( Base ` R )   &    |- L = ( ZRHom ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. DivRing /\ (chr ` R ) = 0 ) -> ( `' L " (Unit ` R ) ) = ( ZZ \ { 0 } ) )
Theorem	elzrhunit 30023	Condition for the image by ZRHom to be a unit. (Contributed by Thierry Arnoux, 30-Oct-2017.)
|- B = ( Base ` R )   &    |- L = ( ZRHom ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( M e. ZZ /\ M =/= 0 ) ) -> ( L ` M ) e. (Unit ` R ) )
Theorem	elzdif0 30024	Lemma for qqhval2 30026. (Contributed by Thierry Arnoux, 29-Oct-2017.)
|- ( M e. ( ZZ \ { 0 } ) -> ( M e. NN \/ -u M e. NN ) )
Theorem	qqhval2lem 30025	Lemma for qqhval2 30026. (Contributed by Thierry Arnoux, 29-Oct-2017.)
|- B = ( Base ` R )   &    |- ./ = (/r ` R )   &    |- L = ( ZRHom ` R )   =>    |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( L ` (numer ` ( X / Y ) ) ) ./ ( L ` (denom ` ( X / Y ) ) ) ) = ( ( L ` X ) ./ ( L ` Y ) ) )
Theorem	qqhval2 30026*	Value of the canonical homormorphism from the rational number when the target ring is a division ring. (Contributed by Thierry Arnoux, 26-Oct-2017.)
|- B = ( Base ` R )   &    |- ./ = (/r ` R )   &    |- L = ( ZRHom ` R )   =>    |- ( ( R e. DivRing /\ (chr ` R ) = 0 ) -> (QQHom ` R ) = ( q e. QQ |-> ( ( L ` (numer ` q ) ) ./ ( L ` (denom ` q ) ) ) ) )
Theorem	qqhvval 30027	Value of the canonical homormorphism from the rational number when the target ring is a division ring. (Contributed by Thierry Arnoux, 30-Oct-2017.)
|- B = ( Base ` R )   &    |- ./ = (/r ` R )   &    |- L = ( ZRHom ` R )   =>    |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ Q e. QQ ) -> ( (QQHom ` R ) ` Q ) = ( ( L ` (numer ` Q ) ) ./ ( L ` (denom ` Q ) ) ) )
Theorem	qqh0 30028	The image of 0 by the QQHom homomorphism is the ring's zero. (Contributed by Thierry Arnoux, 22-Oct-2017.)
|- B = ( Base ` R )   &    |- ./ = (/r ` R )   &    |- L = ( ZRHom ` R )   =>    |- ( ( R e. DivRing /\ (chr ` R ) = 0 ) -> ( (QQHom ` R ) ` 0 ) = ( 0g ` R ) )
Theorem	qqh1 30029	The image of 1 by the QQHom homomorphism is the ring's unit. (Contributed by Thierry Arnoux, 22-Oct-2017.)
|- B = ( Base ` R )   &    |- ./ = (/r ` R )   &    |- L = ( ZRHom ` R )   =>    |- ( ( R e. DivRing /\ (chr ` R ) = 0 ) -> ( (QQHom ` R ) ` 1 ) = ( 1r ` R ) )
Theorem	qqhf 30030	QQHom as a function. (Contributed by Thierry Arnoux, 28-Oct-2017.)
|- B = ( Base ` R )   &    |- ./ = (/r ` R )   &    |- L = ( ZRHom ` R )   =>    |- ( ( R e. DivRing /\ (chr ` R ) = 0 ) -> (QQHom ` R ) : QQ --> B )
Theorem	qqhvq 30031	The image of a quotient by the QQHom homomorphism. (Contributed by Thierry Arnoux, 28-Oct-2017.)
|- B = ( Base ` R )   &    |- ./ = (/r ` R )   &    |- L = ( ZRHom ` R )   =>    |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( (QQHom ` R ) ` ( X / Y ) ) = ( ( L ` X ) ./ ( L ` Y ) ) )
Theorem	qqhghm 30032	The QQHom homomorphism is a group homomorphism if the target structure is a division ring. (Contributed by Thierry Arnoux, 9-Nov-2017.)
|- B = ( Base ` R )   &    |- ./ = (/r ` R )   &    |- L = ( ZRHom ` R )   &    |- Q = (ℂfld ↾s QQ )   =>    |- ( ( R e. DivRing /\ (chr ` R ) = 0 ) -> (QQHom ` R ) e. ( Q GrpHom R ) )
Theorem	qqhrhm 30033	The QQHom homomorphism is a ring homomorphism if the target structure is a field. If the target structure is a division ring, it is a group homomorphism, but not a ring homomorphism, because it does not preserve the ring multiplication operation. (Contributed by Thierry Arnoux, 29-Oct-2017.)
|- B = ( Base ` R )   &    |- ./ = (/r ` R )   &    |- L = ( ZRHom ` R )   &    |- Q = (ℂfld ↾s QQ )   =>    |- ( ( R e. Field /\ (chr ` R ) = 0 ) -> (QQHom ` R ) e. ( Q RingHom R ) )
Theorem	qqhnm 30034	The norm of the image by QQHom of a rational number in a topological division ring. (Contributed by Thierry Arnoux, 8-Nov-2017.)
|- N = ( norm ` R )   &    |- Z = ( ZMod ` R )   =>    |- ( ( ( R e. (NrmRing i^i DivRing ) /\ Z e. NrmMod /\ (chr ` R ) = 0 ) /\ Q e. QQ ) -> ( N ` ( (QQHom ` R ) ` Q ) ) = ( abs ` Q ) )
Theorem	qqhcn 30035	The QQHom homomorphism is a continuous function. (Contributed by Thierry Arnoux, 9-Nov-2017.)
|- Q = (ℂfld ↾s QQ )   &    |- J = ( TopOpen ` Q )   &    |- Z = ( ZMod ` R )   &    |- K = ( TopOpen ` R )   =>    |- ( ( R e. (NrmRing i^i DivRing ) /\ Z e. NrmMod /\ (chr ` R ) = 0 ) -> (QQHom ` R ) e. ( J Cn K ) )
Theorem	qqhucn 30036	The QQHom homomorphism is uniformly continuous. (Contributed by Thierry Arnoux, 28-Jan-2018.)
|- B = ( Base ` R )   &    |- Q = (ℂfld ↾s QQ )   &    |- U = (UnifSt ` Q )   &    |- V = (metUnif ` ( ( dist ` R ) |` ( B X. B ) ) )   &    |- Z = ( ZMod ` R )   &    |- ( ph -> R e. NrmRing )   &    |- ( ph -> R e. DivRing )   &    |- ( ph -> Z e. NrmMod )   &    |- ( ph -> (chr ` R ) = 0 )   =>    |- ( ph -> (QQHom ` R ) e. ( U Cnu V ) )
20.3.13.4  Canonical embedding of the real numbers into a complete ordered field
Syntax	crrh 30037	Map the real numbers into a complete field.
class RRHom
Syntax	crrext 30038	Extend class notation with the class of extension fields of RR.
class ℝExt
Definition	df-rrh 30039	Define the canonical homomorphism from the real numbers to any complete field, as the extension by continuity of the canonical homomorphism from the rational numbers. (Contributed by Mario Carneiro, 22-Oct-2017.) (Revised by Thierry Arnoux, 23-Oct-2017.)
|- RRHom = ( r e. _V |-> ( ( ( topGen ` ran (,) )CnExt ( TopOpen ` r ) ) ` (QQHom ` r ) ) )
Theorem	rrhval 30040	Value of the canonical homormorphism from the real numbers to a complete space. (Contributed by Thierry Arnoux, 2-Nov-2017.)
|- J = ( topGen ` ran (,) )   &    |- K = ( TopOpen ` R )   =>    |- ( R e. V -> (RRHom ` R ) = ( ( JCnExt K ) ` (QQHom ` R ) ) )
Theorem	rrhcn 30041	If the topology of R is Hausdorff, and R is a complete uniform space, then the canonical homomorphism from the real numbers to R is continuous. (Contributed by Thierry Arnoux, 17-Jan-2018.)
|- D = ( ( dist ` R ) |` ( B X. B ) )   &    |- J = ( topGen ` ran (,) )   &    |- B = ( Base ` R )   &    |- K = ( TopOpen ` R )   &    |- Z = ( ZMod ` R )   &    |- ( ph -> R e. DivRing )   &    |- ( ph -> R e. NrmRing )   &    |- ( ph -> Z e. NrmMod )   &    |- ( ph -> (chr ` R ) = 0 )   &    |- ( ph -> R e. CUnifSp )   &    |- ( ph -> (UnifSt ` R ) = (metUnif ` D ) )   =>    |- ( ph -> (RRHom ` R ) e. ( J Cn K ) )
Theorem	rrhf 30042	If the topology of R is Hausdorff, Cauchy sequences have at most one limit, i.e. the canonical homomorphism of RR into R is a function. (Contributed by Thierry Arnoux, 2-Nov-2017.)
|- D = ( ( dist ` R ) |` ( B X. B ) )   &    |- J = ( topGen ` ran (,) )   &    |- B = ( Base ` R )   &    |- K = ( TopOpen ` R )   &    |- Z = ( ZMod ` R )   &    |- ( ph -> R e. DivRing )   &    |- ( ph -> R e. NrmRing )   &    |- ( ph -> Z e. NrmMod )   &    |- ( ph -> (chr ` R ) = 0 )   &    |- ( ph -> R e. CUnifSp )   &    |- ( ph -> (UnifSt ` R ) = (metUnif ` D ) )   =>    |- ( ph -> (RRHom ` R ) : RR --> B )
Definition	df-rrext 30043	Define the class of extensions of RR. This is a shorthand for listing the necessary conditions for a structure to admit a canonical embedding of RR into it. Interestingly, this is not coming from a mathematical reference, but was from the necessary conditions to build the embedding at each step ( ZZ, QQ and RR). It would be interesting see if this is formally treated in the literature. See isrrext 30044 for a better readable version. (Contributed by Thierry Arnoux, 2-May-2018.)
|- ℝExt = { r e. (NrmRing i^i DivRing ) | ( ( ( ZMod ` r ) e. NrmMod /\ (chr ` r ) = 0 ) /\ ( r e. CUnifSp /\ (UnifSt ` r ) = (metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) ) ) ) }
Theorem	isrrext 30044	Express the property " R is an extension of RR". (Contributed by Thierry Arnoux, 2-May-2018.)
|- B = ( Base ` R )   &    |- D = ( ( dist ` R ) |` ( B X. B ) )   &    |- Z = ( ZMod ` R )   =>    |- ( R e. ℝExt <-> ( ( R e. NrmRing /\ R e. DivRing ) /\ ( Z e. NrmMod /\ (chr ` R ) = 0 ) /\ ( R e. CUnifSp /\ (UnifSt ` R ) = (metUnif ` D ) ) ) )
Theorem	rrextnrg 30045	An extension of RR is a normed ring. (Contributed by Thierry Arnoux, 2-May-2018.)
|- ( R e. ℝExt -> R e. NrmRing )
Theorem	rrextdrg 30046	An extension of RR is a division ring. (Contributed by Thierry Arnoux, 2-May-2018.)
|- ( R e. ℝExt -> R e. DivRing )
Theorem	rrextnlm 30047	The norm of an extension of RR is absolutely homogeneous. (Contributed by Thierry Arnoux, 2-May-2018.)
|- Z = ( ZMod ` R )   =>    |- ( R e. ℝExt -> Z e. NrmMod )
Theorem	rrextchr 30048	The ring characteristic of an extension of RR is zero. (Contributed by Thierry Arnoux, 2-May-2018.)
|- ( R e. ℝExt -> (chr ` R ) = 0 )
Theorem	rrextcusp 30049	An extension of RR is a complete uniform space. (Contributed by Thierry Arnoux, 2-May-2018.)
|- ( R e. ℝExt -> R e. CUnifSp )
Theorem	rrexttps 30050	An extension of RR is a topological space. (Contributed by Thierry Arnoux, 7-Sep-2018.)
|- ( R e. ℝExt -> R e. TopSp )
Theorem	rrexthaus 30051	The topology of an extension of RR is Hausdorff. (Contributed by Thierry Arnoux, 7-Sep-2018.)
|- K = ( TopOpen ` R )   =>    |- ( R e. ℝExt -> K e. Haus )
Theorem	rrextust 30052	The uniformity of an extension of RR is the uniformity generated by its distance. (Contributed by Thierry Arnoux, 2-May-2018.)
|- B = ( Base ` R )   &    |- D = ( ( dist ` R ) |` ( B X. B ) )   =>    |- ( R e. ℝExt -> (UnifSt ` R ) = (metUnif ` D ) )
Theorem	rerrext 30053	The field of the real numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.)
|- RRfld e. ℝExt
Theorem	cnrrext 30054	The field of the complex numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018.)
|- ℂfld e. ℝExt
Theorem	qqtopn 30055	The topology of the field of the rational numbers. (Contributed by Thierry Arnoux, 29-Aug-2020.)
|- ( ( TopOpen ` RRfld ) ↾t QQ ) = ( TopOpen ` (ℂfld ↾s QQ ) )
Theorem	rrhfe 30056	If R is an extension of RR, then the canonical homomorphism of RR into R is a function. (Contributed by Thierry Arnoux, 2-May-2018.)
|- B = ( Base ` R )   =>    |- ( R e. ℝExt -> (RRHom ` R ) : RR --> B )
Theorem	rrhcne 30057	If R is an extension of RR, then the canonical homomorphism of RR into R is continuous. (Contributed by Thierry Arnoux, 2-May-2018.)
|- J = ( topGen ` ran (,) )   &    |- K = ( TopOpen ` R )   =>    |- ( R e. ℝExt -> (RRHom ` R ) e. ( J Cn K ) )
Theorem	rrhqima 30058	The RRHom homomorphism leaves rational numbers unchanged. (Contributed by Thierry Arnoux, 27-Mar-2018.)
|- ( ( R e. ℝExt /\ Q e. QQ ) -> ( (RRHom ` R ) ` Q ) = ( (QQHom ` R ) ` Q ) )
Theorem	rrh0 30059	The image of 0 by the RRHom homomorphism is the ring's zero. (Contributed by Thierry Arnoux, 22-Oct-2017.)
|- ( R e. ℝExt -> ( (RRHom ` R ) ` 0 ) = ( 0g ` R ) )
20.3.13.5  Embedding from the extended real numbers into a complete lattice
Syntax	cxrh 30060	Map the extended real numbers into a complete lattice.
class RR*Hom
Definition	df-xrh 30061*	Define an embedding from the extended real number into a complete lattice. (Contributed by Thierry Arnoux, 19-Feb-2018.)
|- RR*Hom = ( r e. _V |-> ( x e. RR* |-> if ( x e. RR , ( (RRHom ` r ) ` x ) , if ( x = +oo , ( ( lub ` r ) ` ( (RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( (RRHom ` r ) " RR ) ) ) ) ) )
Theorem	xrhval 30062*	The value of the embedding from the extended real numbers into a complete lattice. (Contributed by Thierry Arnoux, 19-Feb-2018.)
|- B = ( (RRHom ` R ) " RR )   &    |- L = ( glb ` R )   &    |- U = ( lub ` R )   =>    |- ( R e. V -> (RR*Hom ` R ) = ( x e. RR* |-> if ( x e. RR , ( (RRHom ` R ) ` x ) , if ( x = +oo , ( U ` B ) , ( L ` B ) ) ) ) )
20.3.13.6  Canonical embeddings into the ordered field of the real numbers
Theorem	zrhre 30063	The ZRHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017.)
|- ( ZRHom ` RRfld ) = ( _I |` ZZ )
Theorem	qqhre 30064	The QQHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017.)
|- (QQHom ` RRfld ) = ( _I |` QQ )
Theorem	rrhre 30065	The RRHom homomorphism for the real numbers structure is the identity. (Contributed by Thierry Arnoux, 22-Oct-2017.)
|- (RRHom ` RRfld ) = ( _I |` RR )
20.3.13.7  Topological Manifolds Found this and was curious about how manifolds would be expressed in set.mm: https://mathoverflow.net/questions/336367/real-manifolds-in-a-theorem-prover This chapter proposes to define first Manifold topologies, which characterise topological manifold, and then to extends the structure with presentations, i.e. equivalence classes of atlases for a given topological space. We suggest to use the extensible structures to define the "topological space" aspect of topological manifolds, and then extend it with charts/presentations.
Syntax	cmntop 30066	The class of n-manifold topologies.
class ManTop
Definition	df-mntop 30067*	Define the class of N-manifold topologies, as 2nd countable, Hausdorff topologies, locally homeomorphic to a ball of the Euclidean space of dimension N. (Contributed by Thierry Arnoux, 22-Dec-2019.)
|- ManTop = { <. n , j >. | ( n e. NN0 /\ ( j e. 2ndc /\ j e. Haus /\ j e. Locally [ ( TopOpen ` (𝔼hil ` n ) ) ] ~= ) ) }
Theorem	relmntop 30068	Manifold is a relation. (Contributed by Thierry Arnoux, 28-Dec-2019.)
|- Rel ManTop
Theorem	ismntoplly 30069	Property of being a manifold. (Contributed by Thierry Arnoux, 28-Dec-2019.)
|- ( ( N e. NN0 /\ J e. V ) -> ( NManTop J <-> ( J e. 2ndc /\ J e. Haus /\ J e. Locally [ ( TopOpen ` (𝔼hil ` N ) ) ] ~= ) ) )
Theorem	ismntop 30070*	Property of being a manifold. (Contributed by Thierry Arnoux, 5-Jan-2020.)
|- ( ( N e. NN0 /\ J e. V ) -> ( NManTop J <-> ( J e. 2ndc /\ J e. Haus /\ A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J ↾t u ) ~= ( TopOpen ` (𝔼hil ` N ) ) ) ) ) )
20.3.14  Real and complex functions
20.3.14.1  Integer powers - misc. additions
Theorem	nexple 30071	A lower bound for an exponentiation. (Contributed by Thierry Arnoux, 19-Aug-2017.)
|- ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) -> A <_ ( B ^ A ) )
20.3.14.2  Indicator Functions
Syntax	cind 30072	Extend class notation with the indicator function generator.
class 𝟭
Definition	df-ind 30073*	Define the indicator function generator. (Contributed by Thierry Arnoux, 20-Jan-2017.)
|- 𝟭 = ( o e. _V |-> ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) )
Theorem	indv 30074*	Value of the indicator function generator with domain O. (Contributed by Thierry Arnoux, 23-Aug-2017.)
|- ( O e. V -> (𝟭 ` O ) = ( a e. ~P O |-> ( x e. O |-> if ( x e. a , 1 , 0 ) ) ) )
Theorem	indval 30075*	Value of the indicator function generator for a set A and a domain O. (Contributed by Thierry Arnoux, 2-Feb-2017.)
|- ( ( O e. V /\ A C_ O ) -> ( (𝟭 ` O ) ` A ) = ( x e. O |-> if ( x e. A , 1 , 0 ) ) )
Theorem	indval2 30076	Alternate value of the indicator function generator. (Contributed by Thierry Arnoux, 2-Feb-2017.)
|- ( ( O e. V /\ A C_ O ) -> ( (𝟭 ` O ) ` A ) = ( ( A X. { 1 } ) u. ( ( O \ A ) X. { 0 } ) ) )
Theorem	indf 30077	An indicator function as a function with domain and codomain. (Contributed by Thierry Arnoux, 13-Aug-2017.)
|- ( ( O e. V /\ A C_ O ) -> ( (𝟭 ` O ) ` A ) : O --> { 0 , 1 } )
Theorem	indfval 30078	Value of the indicator function. (Contributed by Thierry Arnoux, 13-Aug-2017.)
|- ( ( O e. V /\ A C_ O /\ X e. O ) -> ( ( (𝟭 ` O ) ` A ) ` X ) = if ( X e. A , 1 , 0 ) )
Theorem	ind1 30079	Value of the indicator function where it is 1. (Contributed by Thierry Arnoux, 14-Aug-2017.)
|- ( ( O e. V /\ A C_ O /\ X e. A ) -> ( ( (𝟭 ` O ) ` A ) ` X ) = 1 )
Theorem	ind0 30080	Value of the indicator function where it is 0. (Contributed by Thierry Arnoux, 14-Aug-2017.)
|- ( ( O e. V /\ A C_ O /\ X e. ( O \ A ) ) -> ( ( (𝟭 ` O ) ` A ) ` X ) = 0 )
Theorem	ind1a 30081	Value of the indicator function where it is 1. (Contributed by Thierry Arnoux, 22-Aug-2017.)
|- ( ( O e. V /\ A C_ O /\ X e. O ) -> ( ( ( (𝟭 ` O ) ` A ) ` X ) = 1 <-> X e. A ) )
Theorem	indpi1 30082	Preimage of the singleton { 1 } by the indicator function. See i1f1lem 23456. (Contributed by Thierry Arnoux, 21-Aug-2017.)
|- ( ( O e. V /\ A C_ O ) -> ( `' ( (𝟭 ` O ) ` A ) " { 1 } ) = A )
Theorem	indsum 30083*	Finite sum of a product with the indicator function / Cartesian product with the indicator function. (Contributed by Thierry Arnoux, 14-Aug-2017.)
|- ( ph -> O e. Fin )   &    |- ( ph -> A C_ O )   &    |- ( ( ph /\ x e. O ) -> B e. CC )   =>    |- ( ph -> sum_ x e. O ( ( ( (𝟭 ` O ) ` A ) ` x ) x. B ) = sum_ x e. A B )
Theorem	indsumin 30084*	Finite sum of a product with the indicator function / Cartesian product with the indicator function. (Contributed by Thierry Arnoux, 11-Dec-2021.)
|- ( ph -> O e. V )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A C_ O )   &    |- ( ph -> B C_ O )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   =>    |- ( ph -> sum_ k e. A ( ( ( (𝟭 ` O ) ` B ) ` k ) x. C ) = sum_ k e. ( A i^i B ) C )
Theorem	prodindf 30085*	The product of indicators is one if and only if all values are in the set. (Contributed by Thierry Arnoux, 11-Dec-2021.)
|- ( ph -> O e. V )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B C_ O )   &    |- ( ph -> F : A --> O )   =>    |- ( ph -> prod_ k e. A ( ( (𝟭 ` O ) ` B ) ` ( F ` k ) ) = if ( ran F C_ B , 1 , 0 ) )
Theorem	indf1o 30086	The bijection between a power set and the set of indicator functions. (Contributed by Thierry Arnoux, 14-Aug-2017.)
|- ( O e. V -> (𝟭 ` O ) : ~P O -1-1-onto-> ( { 0 , 1 } ^m O ) )
Theorem	indpreima 30087	A function with range { 0 , 1 } as an indicator of the preimage of { 1 }. (Contributed by Thierry Arnoux, 23-Aug-2017.)
|- ( ( O e. V /\ F : O --> { 0 , 1 } ) -> F = ( (𝟭 ` O ) ` ( `' F " { 1 } ) ) )
Theorem	indf1ofs 30088*	The bijection between finite subsets and the indicator functions with finite support. (Contributed by Thierry Arnoux, 22-Aug-2017.)
|- ( O e. V -> ( (𝟭 ` O ) |` Fin ) : ( ~P O i^i Fin ) -1-1-onto-> { f e. ( { 0 , 1 } ^m O ) | ( `' f " { 1 } ) e. Fin } )
20.3.14.3  Extended sum
Syntax	cesum 30089	Extend class notation to include infinite summations.
class Σ* k e. A B
Definition	df-esum 30090	Define a short-hand for the possibly infinite sum over the extended nonnegative reals. Σ* is relying on the properties of the tsums, developped by Mario Carneiro. (Contributed by Thierry Arnoux, 21-Sep-2016.)
|- Σ* k e. A B = U. ( ( RR*s ↾s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )
Theorem	esumex 30091	An extended sum is a set by definition. (Contributed by Thierry Arnoux, 5-Sep-2017.)
|- Σ* k e. A B e. _V
Theorem	esumcl 30092*	Closure for extended sum in the extended positive reals. (Contributed by Thierry Arnoux, 2-Jan-2017.)
|- F/_ k A   =>    |- ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> Σ* k e. A B e. ( 0 [,] +oo ) )
Theorem	esumeq12dvaf 30093	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 26-Mar-2017.)
|- F/ k ph   &    |- ( ph -> A = B )   &    |- ( ( ph /\ k e. A ) -> C = D )   =>    |- ( ph -> Σ* k e. A C = Σ* k e. B D )
Theorem	esumeq12dva 30094*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.) (Revised by Thierry Arnoux, 29-Jun-2017.)
|- ( ph -> A = B )   &    |- ( ( ph /\ k e. A ) -> C = D )   =>    |- ( ph -> Σ* k e. A C = Σ* k e. B D )
Theorem	esumeq12d 30095*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> Σ* k e. A C = Σ* k e. B D )
Theorem	esumeq1 30096*	Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.)
|- ( A = B -> Σ* k e. A C = Σ* k e. B C )
Theorem	esumeq1d 30097	Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.)
|- F/ k ph   &    |- ( ph -> A = B )   =>    |- ( ph -> Σ* k e. A C = Σ* k e. B C )
Theorem	esumeq2 30098*	Equality theorem for extended sum. (Contributed by Thierry Arnoux, 24-Dec-2016.)
|- ( A. k e. A B = C -> Σ* k e. A B = Σ* k e. A C )
Theorem	esumeq2d 30099	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 21-Sep-2016.)
|- F/ k ph   &    |- ( ph -> A. k e. A B = C )   =>    |- ( ph -> Σ* k e. A B = Σ* k e. A C )
Theorem	esumeq2dv 30100*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 2-Jan-2017.)
|- ( ( ph /\ k e. A ) -> B = C )   =>    |- ( ph -> Σ* k e. A B = Σ* k e. A C )