P. 149 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14801-14900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rspssid 14801	The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- K = (RSpan ` R )   &    |- B = ( Base ` R )   =>    |- ( ( R e. Ring /\ G C_ B ) -> G C_ ( K ` G ) )
Theorem	rsp0 14802	The span of the zero element is the zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- K = (RSpan ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> ( K ` { .0. } ) = { .0. } )
Theorem	rspssp 14803	The ideal span of a set of elements in a ring is contained in any subring which contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- K = (RSpan ` R )   &    |- U = (LIdeal ` R )   =>    |- ( ( R e. Ring /\ I e. U /\ G C_ I ) -> ( K ` G ) C_ I )
Theorem	lidlrsppropdg 14804*	The left ideals and ring span of a ring depend only on the ring components. Here W is expected to be either B (when closure is available) or _V (when strong equality is available). (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> B C_ W )   &    |- ( ( ph /\ ( x e. W /\ y e. W ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) e. W )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   &    |- ( ph -> K e. X )   &    |- ( ph -> L e. Y )   =>    |- ( ph -> ( (LIdeal ` K ) = (LIdeal ` L ) /\ (RSpan ` K ) = (RSpan ` L ) ) )
Theorem	rnglidlmmgm 14805	The multiplicative group of a (left) ideal of a non-unital ring is a magma. (Contributed by AV, 17-Feb-2020.) Generalization for non-unital rings. The assumption .0. e. U is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> (mulGrp ` I ) e. Mgm )
Theorem	rnglidlmsgrp 14806	The multiplicative group of a (left) ideal of a non-unital ring is a semigroup. (Contributed by AV, 17-Feb-2020.) Generalization for non-unital rings. The assumption .0. e. U is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> (mulGrp ` I ) e. Smgrp )
Theorem	rnglidlrng 14807	A (left) ideal of a non-unital ring is a non-unital ring. (Contributed by AV, 17-Feb-2020.) Generalization for non-unital rings. The assumption U e. (SubGrp ` R ) is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   =>    |- ( ( R e. Rng /\ U e. L /\ U e. (SubGrp ` R ) ) -> I e. Rng )
7.6.3  Two-sided ideals and quotient rings
Syntax	c2idl 14808	Ring two-sided ideal function.
class 2Ideal
Definition	df-2idl 14809	Define the class of two-sided ideals of a ring. A two-sided ideal is a left ideal which is also a right ideal (or a left ideal over the opposite ring). (Contributed by Mario Carneiro, 14-Jun-2015.)
|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
Theorem	2idlmex 14810	Existence of the set a two-sided ideal is built from (when the ideal is inhabited). (Contributed by Jim Kingdon, 18-Apr-2025.)
|- T = (2Ideal ` W )   =>    |- ( U e. T -> W e. _V )
Theorem	2idlval 14811	Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- I = (LIdeal ` R )   &    |- O = (oppr ` R )   &    |- J = (LIdeal ` O )   &    |- T = (2Ideal ` R )   =>    |- T = ( I i^i J )
Theorem	2idlvalg 14812	Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- I = (LIdeal ` R )   &    |- O = (oppr ` R )   &    |- J = (LIdeal ` O )   &    |- T = (2Ideal ` R )   =>    |- ( R e. V -> T = ( I i^i J ) )
Theorem	isridl 14813*	A right ideal is a left ideal of the opposite ring. This theorem shows that this definition corresponds to the usual textbook definition of a right ideal of a ring to be a subgroup of the additive group of the ring which is closed under right-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.)
|- U = (LIdeal ` (oppr ` R ) )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. Ring -> ( I e. U <-> ( I e. (SubGrp ` R ) /\ A. x e. B A. y e. I ( y .x. x ) e. I ) ) )
Theorem	2idlelb 14814	Membership in a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.)
|- I = (LIdeal ` R )   &    |- O = (oppr ` R )   &    |- J = (LIdeal ` O )   &    |- T = (2Ideal ` R )   =>    |- ( U e. T <-> ( U e. I /\ U e. J ) )
Theorem	2idllidld 14815	A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
|- ( ph -> I e. (2Ideal ` R ) )   =>    |- ( ph -> I e. (LIdeal ` R ) )
Theorem	2idlridld 14816	A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
|- ( ph -> I e. (2Ideal ` R ) )   &    |- O = (oppr ` R )   =>    |- ( ph -> I e. (LIdeal ` O ) )
Theorem	df2idl2rng 14817*	Alternate (the usual textbook) definition of a two-sided ideal of a non-unital ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025.)
|- U = (2Ideal ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Rng /\ I e. (SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) )
Theorem	df2idl2 14818*	Alternate (the usual textbook) definition of a two-sided ideal of a ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.) (Proof shortened by AV, 18-Apr-2025.)
|- U = (2Ideal ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. Ring -> ( I e. U <-> ( I e. (SubGrp ` R ) /\ A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) ) )
Theorem	ridl0 14819	Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.)
|- U = (LIdeal ` (oppr ` R ) )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> { .0. } e. U )
Theorem	ridl1 14820	Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.)
|- U = (LIdeal ` (oppr ` R ) )   &    |- B = ( Base ` R )   =>    |- ( R e. Ring -> B e. U )
Theorem	2idl0 14821	Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.)
|- I = (2Ideal ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> { .0. } e. I )
Theorem	2idl1 14822	Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.)
|- I = (2Ideal ` R )   &    |- B = ( Base ` R )   =>    |- ( R e. Ring -> B e. I )
Theorem	2idlss 14823	A two-sided ideal is a subset of the base set. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.) (Proof shortened by AV, 13-Mar-2025.)
|- B = ( Base ` W )   &    |- I = (2Ideal ` W )   =>    |- ( U e. I -> U C_ B )
Theorem	2idlbas 14824	The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.)
|- ( ph -> I e. (2Ideal ` R ) )   &    |- J = ( R ↾s I )   &    |- B = ( Base ` J )   =>    |- ( ph -> B = I )
Theorem	2idlelbas 14825	The base set of a two-sided ideal as structure is a left and right ideal. (Contributed by AV, 20-Feb-2025.)
|- ( ph -> I e. (2Ideal ` R ) )   &    |- J = ( R ↾s I )   &    |- B = ( Base ` J )   =>    |- ( ph -> ( B e. (LIdeal ` R ) /\ B e. (LIdeal ` (oppr ` R ) ) ) )
Theorem	rng2idlsubrng 14826	A two-sided ideal of a non-unital ring which is a non-unital ring is a subring of the ring. (Contributed by AV, 20-Feb-2025.) (Revised by AV, 11-Mar-2025.)
|- ( ph -> R e. Rng )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> ( R ↾s I ) e. Rng )   =>    |- ( ph -> I e. (SubRng ` R ) )
Theorem	rng2idlnsg 14827	A two-sided ideal of a non-unital ring which is a non-unital ring is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
|- ( ph -> R e. Rng )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> ( R ↾s I ) e. Rng )   =>    |- ( ph -> I e. (NrmSGrp ` R ) )
Theorem	rng2idl0 14828	The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a non-unital ring. (Contributed by AV, 20-Feb-2025.)
|- ( ph -> R e. Rng )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> ( R ↾s I ) e. Rng )   =>    |- ( ph -> ( 0g ` R ) e. I )
Theorem	rng2idlsubgsubrng 14829	A two-sided ideal of a non-unital ring which is a subgroup of the ring is a subring of the ring. (Contributed by AV, 11-Mar-2025.)
|- ( ph -> R e. Rng )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> I e. (SubGrp ` R ) )   =>    |- ( ph -> I e. (SubRng ` R ) )
Theorem	rng2idlsubgnsg 14830	A two-sided ideal of a non-unital ring which is a subgroup of the ring is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
|- ( ph -> R e. Rng )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> I e. (SubGrp ` R ) )   =>    |- ( ph -> I e. (NrmSGrp ` R ) )
Theorem	rng2idlsubg0 14831	The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
|- ( ph -> R e. Rng )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> I e. (SubGrp ` R ) )   =>    |- ( ph -> ( 0g ` R ) e. I )
Theorem	2idlcpblrng 14832	The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) Generalization for non-unital rings and two-sided ideals which are subgroups of the additive group of the non-unital ring. (Revised by AV, 23-Feb-2025.)
|- X = ( Base ` R )   &    |- E = ( R ~QG S )   &    |- I = (2Ideal ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Rng /\ S e. I /\ S e. (SubGrp ` R ) ) -> ( ( A E C /\ B E D ) -> ( A .x. B ) E ( C .x. D ) ) )
Theorem	2idlcpbl 14833	The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) (Proof shortened by AV, 31-Mar-2025.)
|- X = ( Base ` R )   &    |- E = ( R ~QG S )   &    |- I = (2Ideal ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ S e. I ) -> ( ( A E C /\ B E D ) -> ( A .x. B ) E ( C .x. D ) ) )
Theorem	qus2idrng 14834	The quotient of a non-unital ring modulo a two-sided ideal, which is a subgroup of the additive group of the non-unital ring, is a non-unital ring (qusring 14836 analog). (Contributed by AV, 23-Feb-2025.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (2Ideal ` R )   =>    |- ( ( R e. Rng /\ S e. I /\ S e. (SubGrp ` R ) ) -> U e. Rng )
Theorem	qus1 14835	The multiplicative identity of the quotient ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (2Ideal ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ S e. I ) -> ( U e. Ring /\ [ .1. ] ( R ~QG S ) = ( 1r ` U ) ) )
Theorem	qusring 14836	If S is a two-sided ideal in R, then U = R / S is a ring, called the quotient ring of R by S. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (2Ideal ` R )   =>    |- ( ( R e. Ring /\ S e. I ) -> U e. Ring )
Theorem	qusrhm 14837*	If S is a two-sided ideal in R, then the "natural map" from elements to their cosets is a ring homomorphism from R to R / S. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (2Ideal ` R )   &    |- X = ( Base ` R )   &    |- F = ( x e. X |-> [ x ] ( R ~QG S ) )   =>    |- ( ( R e. Ring /\ S e. I ) -> F e. ( R RingHom U ) )
Theorem	qusmul2 14838	Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024.)
|- Q = ( R /.s ( R ~QG I ) )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .X. = ( .r ` Q )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( [ X ] ( R ~QG I ) .X. [ Y ] ( R ~QG I ) ) = [ ( X .x. Y ) ] ( R ~QG I ) )
Theorem	crngridl 14839	In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- I = (LIdeal ` R )   &    |- O = (oppr ` R )   =>    |- ( R e. CRing -> I = (LIdeal ` O ) )
Theorem	crng2idl 14840	In a commutative ring, a two-sided ideal is the same as a left ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- I = (LIdeal ` R )   =>    |- ( R e. CRing -> I = (2Ideal ` R ) )
Theorem	qusmulrng 14841	Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng 14842. Similar to qusmul2 14838. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 28-Feb-2025.)
|- .~ = ( R ~QG S )   &    |- H = ( R /.s .~ )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` H )   =>    |- ( ( ( R e. Rng /\ S e. (2Ideal ` R ) /\ S e. (SubGrp ` R ) ) /\ ( X e. B /\ Y e. B ) ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )
Theorem	quscrng 14842	The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) (Proof shortened by AV, 3-Apr-2025.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (LIdeal ` R )   =>    |- ( ( R e. CRing /\ S e. I ) -> U e. CRing )
7.6.4  Principal ideal rings. Divisibility in the integers
Theorem	rspsn 14843*	Membership in principal ideals is closely related to divisibility. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- B = ( Base ` R )   &    |- K = (RSpan ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. Ring /\ G e. B ) -> ( K ` { G } ) = { x | G .|| x } )
7.7  The complex numbers as an algebraic extensible structure
7.7.1  Definition and basic properties
Syntax	cpsmet 14844	Extend class notation with the class of all pseudometric spaces.
class PsMet
Syntax	cxmet 14845	Extend class notation with the class of all extended metric spaces.
class *Met
Syntax	cmet 14846	Extend class notation with the class of all metrics.
class Met
Syntax	cbl 14847	Extend class notation with the metric space ball function.
class ball
Syntax	cfbas 14848	Extend class definition to include the class of filter bases.
class fBas
Syntax	cfg 14849	Extend class definition to include the filter generating function.
class filGen
Syntax	cmopn 14850	Extend class notation with a function mapping each metric space to the family of its open sets.
class MetOpen
Syntax	cmetu 14851	Extend class notation with the function mapping metrics to the uniform structure generated by that metric.
class metUnif
Definition	df-psmet 14852*	Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- PsMet = ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x ( ( y d y ) = 0 /\ A. z e. x A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } )
Definition	df-xmet 14853*	Define the set of all extended metrics on a given base set. The definition is similar to df-met 14854, but we also allow the metric to take on the value +oo. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- *Met = ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } )
Definition	df-met 14854*	Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric. However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of [Gleason] p. 223. (Contributed by NM, 25-Aug-2006.)
|- Met = ( x e. _V |-> { d e. ( RR ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) ) } )
Definition	df-bl 14855*	Define the metric space ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
Definition	df-mopn 14856	Define a function whose value is the family of open sets of a metric space. (Contributed by NM, 1-Sep-2006.)
|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
Definition	df-fbas 14857*	Define the class of all filter bases. Note that a filter base on one set is also a filter base for any superset, so there is not a unique base set that can be recovered. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
|- fBas = ( w e. _V |-> { x e. ~P ~P w | ( x =/= (/) /\ (/) e/ x /\ A. y e. x A. z e. x ( x i^i ~P ( y i^i z ) ) =/= (/) ) } )
Definition	df-fg 14858*	Define the filter generating function. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
Definition	df-metu 14859*	Define the function mapping metrics to the uniform structure generated by that metric. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
Theorem	blfn 14860	The ball function has universal domain. (Contributed by Jim Kingdon, 24-Sep-2025.)
|- ball Fn _V
Theorem	mopnset 14861	Getting a set by applying MetOpen. (Contributed by Jim Kingdon, 24-Sep-2025.)
|- ( D e. V -> ( MetOpen ` D ) e. _V )
Theorem	cndsex 14862	The standard distance function on the complex numbers is a set. (Contributed by Jim Kingdon, 28-Sep-2025.)
|- ( abs o. - ) e. _V
Theorem	cntopex 14863	The standard topology on the complex numbers is a set. (Contributed by Jim Kingdon, 25-Sep-2025.)
|- ( MetOpen ` ( abs o. - ) ) e. _V
Theorem	metuex 14864	Applying metUnif yields a set. (Contributed by Jim Kingdon, 28-Sep-2025.)
|- ( A e. V -> (metUnif ` A ) e. _V )
Syntax	ccnfld 14865	Extend class notation with the field of complex numbers.
class ℂfld
Definition	df-cnfld 14866*	The field of complex numbers. Other number fields and rings can be constructed by applying the ↾s restriction operator. The contract of this set is defined entirely by cnfldex 14868, cnfldadd 14871, cnfldmul 14873, cnfldcj 14874, cnfldtset 14875, cnfldle 14876, cnfldds 14877, and cnfldbas 14869. We may add additional members to this in the future. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Thierry Arnoux, 15-Dec-2017.) Use maps-to notation for addition and multiplication. (Revised by GG, 31-Mar-2025.) (New usage is discouraged.)
|- ℂfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >. , <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. } ) )
Theorem	cnfldstr 14867	The field of complex numbers is a structure. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.)
|- ℂfld Struct <. 1 , ; 1 3 >.
Theorem	cnfldex 14868	The field of complex numbers is a set. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.)
|- ℂfld e. _V
Theorem	cnfldbas 14869	The base set of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.)
|- CC = ( Base ` ℂfld )
Theorem	mpocnfldadd 14870*	The addition operation of the field of complex numbers. Version of cnfldadd 14871 using maps-to notation, which does not require ax-addf 8291. (Contributed by GG, 31-Mar-2025.)
|- ( x e. CC , y e. CC |-> ( x + y ) ) = ( +g ` ℂfld )
Theorem	cnfldadd 14871	The addition operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 27-Apr-2025.)
|- + = ( +g ` ℂfld )
Theorem	mpocnfldmul 14872*	The multiplication operation of the field of complex numbers. Version of cnfldmul 14873 using maps-to notation, which does not require ax-mulf 8292. (Contributed by GG, 31-Mar-2025.)
|- ( x e. CC , y e. CC |-> ( x x. y ) ) = ( .r ` ℂfld )
Theorem	cnfldmul 14873	The multiplication operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 27-Apr-2025.)
|- x. = ( .r ` ℂfld )
Theorem	cnfldcj 14874	The conjugation operation of the field of complex numbers. (Contributed by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 17-Dec-2017.)
|- * = ( *r ` ℂfld )
Theorem	cnfldtset 14875	The topology component of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 31-Mar-2025.)
|- ( MetOpen ` ( abs o. - ) ) = (TopSet ` ℂfld )
Theorem	cnfldle 14876	The ordering of the field of complex numbers. Note that this is not actually an ordering on CC, but we put it in the structure anyway because restricting to RR does not affect this component, so that (ℂfld ↾s RR ) is an ordered field even though ℂfld itself is not. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 14866. (Revised by GG, 31-Mar-2025.)
|- <_ = ( le ` ℂfld )
Theorem	cnfldds 14877	The metric of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 14866. (Revised by GG, 31-Mar-2025.)
|- ( abs o. - ) = ( dist ` ℂfld )
Theorem	cncrng 14878	The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.)
|- ℂfld e. CRing
Theorem	cnring 14879	The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- ℂfld e. Ring
Theorem	cnfld0 14880	Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- 0 = ( 0g ` ℂfld )
Theorem	cnfld1 14881	One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- 1 = ( 1r ` ℂfld )
Theorem	cnfldneg 14882	The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- ( X e. CC -> ( ( invg ` ℂfld ) ` X ) = -u X )
Theorem	cnfldplusf 14883	The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- + = ( +f ` ℂfld )
Theorem	cnfldsub 14884	The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- - = ( -g ` ℂfld )
Theorem	cnfldmulg 14885	The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( ( A e. ZZ /\ B e. CC ) -> ( A (.g ` ℂfld ) B ) = ( A x. B ) )
Theorem	cnfldexp 14886	The exponentiation operator in the field of complex numbers (for nonnegative exponents). (Contributed by Mario Carneiro, 15-Jun-2015.)
|- ( ( A e. CC /\ B e. NN0 ) -> ( B (.g ` (mulGrp ` ℂfld ) ) A ) = ( A ^ B ) )
Theorem	cnsubmlem 14887*	Lemma for nn0subm 14892 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( x e. A -> x e. CC )   &    |- ( ( x e. A /\ y e. A ) -> ( x + y ) e. A )   &    |- 0 e. A   =>    |- A e. (SubMnd ` ℂfld )
Theorem	cnsubglem 14888*	Lemma for cnsubrglem 14889 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ( x e. A -> x e. CC )   &    |- ( ( x e. A /\ y e. A ) -> ( x + y ) e. A )   &    |- ( x e. A -> -u x e. A )   &    |- B e. A   =>    |- A e. (SubGrp ` ℂfld )
Theorem	cnsubrglem 14889*	Lemma for zsubrg 14890 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ( x e. A -> x e. CC )   &    |- ( ( x e. A /\ y e. A ) -> ( x + y ) e. A )   &    |- ( x e. A -> -u x e. A )   &    |- 1 e. A   &    |- ( ( x e. A /\ y e. A ) -> ( x x. y ) e. A )   =>    |- A e. (SubRing ` ℂfld )
Theorem	zsubrg 14890	The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ZZ e. (SubRing ` ℂfld )
Theorem	gzsubrg 14891	The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ZZ[_i] e. (SubRing ` ℂfld )
Theorem	nn0subm 14892	The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- NN0 e. (SubMnd ` ℂfld )
Theorem	rege0subm 14893	The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- ( 0 [,) +oo ) e. (SubMnd ` ℂfld )
Theorem	zsssubrg 14894	The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( R e. (SubRing ` ℂfld ) -> ZZ C_ R )
Theorem	gsumfsum 14895*	Relate a group sum on ℂfld to a finite sum on the complex numbers. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> (ℂfld gsumg ( k e. A |-> B ) ) = sum_ k e. A B )
Theorem	cnfldui 14896	The invertible complex numbers are exactly those apart from zero. This is recapb 8991 but expressed in terms of ℂfld. (Contributed by Jim Kingdon, 11-Sep-2025.)
|- { z e. CC | z # 0 } = (Unit ` ℂfld )
7.7.2  Ring of integers According to Wikipedia ("Integer", 25-May-2019, https://en.wikipedia.org/wiki/Integer) "The integers form a unital ring which is the most basic one, in the following sense: for any unital ring, there is a unique ring homomorphism from the integers into this ring. This universal property, namely to be an initial object in the category of [unital] rings, characterizes the ring Z." In set.mm, there was no explicit definition for the ring of integers until June 2019, but it was denoted by (ℂfld ↾s ZZ ), the field of complex numbers restricted to the integers. In zringring 14900 it is shown that this restriction is a ring, and zringbas 14903 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring 14898 of the ring of integers. Remark: Instead of using the symbol "ZZrng" analogous to ℂfld used for the field of complex numbers, we have chosen the version with an "i" to indicate that the ring of integers is a unital ring, see also Wikipedia ("Rng (algebra)", 9-Jun-2019, https://en.wikipedia.org/wiki/Rng_(algebra) 14898).
Syntax	czring 14897	Extend class notation with the (unital) ring of integers.
class ℤring
Definition	df-zring 14898	The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.)
|- ℤring = (ℂfld ↾s ZZ )
Theorem	zringcrng 14899	The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.)
|- ℤring e. CRing
Theorem	zringring 14900	The ring of integers is a ring. (Contributed by AV, 20-May-2019.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 13-Jun-2019.)
|- ℤring e. Ring