P. 198 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19701-19800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	evl1vard 19701	Polynomial evaluation builder for the variable. (Contributed by Mario Carneiro, 4-Jul-2015.)
|- O = (eval1 ` R )   &    |- X = (var1 ` R )   &    |- B = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- U = ( Base ` P )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X e. U /\ ( ( O ` X ) ` Y ) = Y ) )
Theorem	evls1var 19702	Univariate polynomial evaluation for subrings maps the variable to the identity function. (Contributed by AV, 13-Sep-2019.)
|- Q = ( S evalSub1 R )   &    |- X = (var1 ` U )   &    |- U = ( S ↾s R )   &    |- B = ( Base ` S )   &    |- ( ph -> S e. CRing )   &    |- ( ph -> R e. (SubRing ` S ) )   =>    |- ( ph -> ( Q ` X ) = ( _I |` B ) )
Theorem	evls1scasrng 19703	The evaluation of a scalar of a subring yields the same result as evaluated as a scalar over the ring itself. (Contributed by AV, 13-Sep-2019.)
|- Q = ( S evalSub1 R )   &    |- O = (eval1 ` S )   &    |- W = (Poly1 ` U )   &    |- U = ( S ↾s R )   &    |- P = (Poly1 ` S )   &    |- B = ( Base ` S )   &    |- A = (algSc ` W )   &    |- C = (algSc ` P )   &    |- ( ph -> S e. CRing )   &    |- ( ph -> R e. (SubRing ` S ) )   &    |- ( ph -> X e. R )   =>    |- ( ph -> ( Q ` ( A ` X ) ) = ( O ` ( C ` X ) ) )
Theorem	evls1varsrng 19704	The evaluation of the variable of univariate polynomials over subring yields the same result as evaluated as variable of the polynomials over the ring itself. (Contributed by AV, 12-Sep-2019.)
|- Q = ( S evalSub1 R )   &    |- O = (eval1 ` S )   &    |- V = (var1 ` U )   &    |- U = ( S ↾s R )   &    |- B = ( Base ` S )   &    |- ( ph -> S e. CRing )   &    |- ( ph -> R e. (SubRing ` S ) )   =>    |- ( ph -> ( Q ` V ) = ( O ` V ) )
Theorem	evl1addd 19705	Polynomial evaluation builder for addition of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
|- O = (eval1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` R )   &    |- U = ( Base ` P )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> Y e. B )   &    |- ( ph -> ( M e. U /\ ( ( O ` M ) ` Y ) = V ) )   &    |- ( ph -> ( N e. U /\ ( ( O ` N ) ` Y ) = W ) )   &    |- .+b = ( +g ` P )   &    |- .+ = ( +g ` R )   =>    |- ( ph -> ( ( M .+b N ) e. U /\ ( ( O ` ( M .+b N ) ) ` Y ) = ( V .+ W ) ) )
Theorem	evl1subd 19706	Polynomial evaluation builder for subtraction of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
|- O = (eval1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` R )   &    |- U = ( Base ` P )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> Y e. B )   &    |- ( ph -> ( M e. U /\ ( ( O ` M ) ` Y ) = V ) )   &    |- ( ph -> ( N e. U /\ ( ( O ` N ) ` Y ) = W ) )   &    |- .- = ( -g ` P )   &    |- D = ( -g ` R )   =>    |- ( ph -> ( ( M .- N ) e. U /\ ( ( O ` ( M .- N ) ) ` Y ) = ( V D W ) ) )
Theorem	evl1muld 19707	Polynomial evaluation builder for multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
|- O = (eval1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` R )   &    |- U = ( Base ` P )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> Y e. B )   &    |- ( ph -> ( M e. U /\ ( ( O ` M ) ` Y ) = V ) )   &    |- ( ph -> ( N e. U /\ ( ( O ` N ) ` Y ) = W ) )   &    |- .xb = ( .r ` P )   &    |- .x. = ( .r ` R )   =>    |- ( ph -> ( ( M .xb N ) e. U /\ ( ( O ` ( M .xb N ) ) ` Y ) = ( V .x. W ) ) )
Theorem	evl1vsd 19708	Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
|- O = (eval1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` R )   &    |- U = ( Base ` P )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> Y e. B )   &    |- ( ph -> ( M e. U /\ ( ( O ` M ) ` Y ) = V ) )   &    |- ( ph -> N e. B )   &    |- .xb = ( .s ` P )   &    |- .x. = ( .r ` R )   =>    |- ( ph -> ( ( N .xb M ) e. U /\ ( ( O ` ( N .xb M ) ) ` Y ) = ( N .x. V ) ) )
Theorem	evl1expd 19709	Polynomial evaluation builder for an exponential. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- O = (eval1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` R )   &    |- U = ( Base ` P )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> Y e. B )   &    |- ( ph -> ( M e. U /\ ( ( O ` M ) ` Y ) = V ) )   &    |- .xb = (.g ` (mulGrp ` P ) )   &    |- .^ = (.g ` (mulGrp ` R ) )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( ( N .xb M ) e. U /\ ( ( O ` ( N .xb M ) ) ` Y ) = ( N .^ V ) ) )
Theorem	pf1const 19710	Constants are polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- B = ( Base ` R )   &    |- Q = ran (eval1 ` R )   =>    |- ( ( R e. CRing /\ X e. B ) -> ( B X. { X } ) e. Q )
Theorem	pf1id 19711	The identity is a polynomial function. (Contributed by Mario Carneiro, 20-Mar-2015.)
|- B = ( Base ` R )   &    |- Q = ran (eval1 ` R )   =>    |- ( R e. CRing -> ( _I |` B ) e. Q )
Theorem	pf1subrg 19712	Polynomial functions are a subring. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- B = ( Base ` R )   &    |- Q = ran (eval1 ` R )   =>    |- ( R e. CRing -> Q e. (SubRing ` ( R ^s B ) ) )
Theorem	pf1rcl 19713	Reverse closure for the set of polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- Q = ran (eval1 ` R )   =>    |- ( X e. Q -> R e. CRing )
Theorem	pf1f 19714	Polynomial functions are functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- Q = ran (eval1 ` R )   &    |- B = ( Base ` R )   =>    |- ( F e. Q -> F : B --> B )
Theorem	mpfpf1 19715*	Convert a multivariate polynomial function to univariate. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- Q = ran (eval1 ` R )   &    |- B = ( Base ` R )   &    |- E = ran ( 1o eval R )   =>    |- ( F e. E -> ( F o. ( y e. B |-> ( 1o X. { y } ) ) ) e. Q )
Theorem	pf1mpf 19716*	Convert a univariate polynomial function to multivariate. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- Q = ran (eval1 ` R )   &    |- B = ( Base ` R )   &    |- E = ran ( 1o eval R )   =>    |- ( F e. Q -> ( F o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) e. E )
Theorem	pf1addcl 19717	The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- Q = ran (eval1 ` R )   &    |- .+ = ( +g ` R )   =>    |- ( ( F e. Q /\ G e. Q ) -> ( F oF .+ G ) e. Q )
Theorem	pf1mulcl 19718	The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- Q = ran (eval1 ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( F e. Q /\ G e. Q ) -> ( F oF .x. G ) e. Q )
Theorem	pf1ind 19719*	Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- Q = ran (eval1 ` R )   &    |- ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> ze )   &    |- ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> si )   &    |- ( x = ( B X. { f } ) -> ( ps <-> ch ) )   &    |- ( x = ( _I |` B ) -> ( ps <-> th ) )   &    |- ( x = f -> ( ps <-> ta ) )   &    |- ( x = g -> ( ps <-> et ) )   &    |- ( x = ( f oF .+ g ) -> ( ps <-> ze ) )   &    |- ( x = ( f oF .x. g ) -> ( ps <-> si ) )   &    |- ( x = A -> ( ps <-> rh ) )   &    |- ( ( ph /\ f e. B ) -> ch )   &    |- ( ph -> th )   &    |- ( ph -> A e. Q )   =>    |- ( ph -> rh )
Theorem	evl1gsumdlem 19720*	Lemma for evl1gsumd 19721 (induction step). (Contributed by AV, 17-Sep-2019.)
|- O = (eval1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` R )   &    |- U = ( Base ` P )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> Y e. B )   =>    |- ( ( m e. Fin /\ -. a e. m /\ ph ) -> ( ( A. x e. m M e. U -> ( ( O ` ( P gsumg ( x e. m |-> M ) ) ) ` Y ) = ( R gsumg ( x e. m |-> ( ( O ` M ) ` Y ) ) ) ) -> ( A. x e. ( m u. { a } ) M e. U -> ( ( O ` ( P gsumg ( x e. ( m u. { a } ) |-> M ) ) ) ` Y ) = ( R gsumg ( x e. ( m u. { a } ) |-> ( ( O ` M ) ` Y ) ) ) ) ) )
Theorem	evl1gsumd 19721*	Polynomial evaluation builder for a finite group sum of polynomials. (Contributed by AV, 17-Sep-2019.)
|- O = (eval1 ` R )   &    |- P = (Poly1 ` R )   &    |- B = ( Base ` R )   &    |- U = ( Base ` P )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> Y e. B )   &    |- ( ph -> A. x e. N M e. U )   &    |- ( ph -> N e. Fin )   =>    |- ( ph -> ( ( O ` ( P gsumg ( x e. N |-> M ) ) ) ` Y ) = ( R gsumg ( x e. N |-> ( ( O ` M ) ` Y ) ) ) )
Theorem	evl1gsumadd 19722*	Univariate polynomial evaluation maps (additive) group sums to group sums. Remark: the proof would be shorter if the theorem is proved directly instead of using evls1gsumadd 19689. (Contributed by AV, 15-Sep-2019.)
|- Q = (eval1 ` R )   &    |- K = ( Base ` R )   &    |- W = (Poly1 ` R )   &    |- P = ( R ^s K )   &    |- B = ( Base ` W )   &    |- ( ph -> R e. CRing )   &    |- ( ( ph /\ x e. N ) -> Y e. B )   &    |- ( ph -> N C_ NN0 )   &    |- .0. = ( 0g ` W )   &    |- ( ph -> ( x e. N |-> Y ) finSupp .0. )   =>    |- ( ph -> ( Q ` ( W gsumg ( x e. N |-> Y ) ) ) = ( P gsumg ( x e. N |-> ( Q ` Y ) ) ) )
Theorem	evl1gsumaddval 19723*	Value of a univariate polynomial evaluation mapping an additive group sum to a group sum of the evaluated variable. (Contributed by AV, 17-Sep-2019.)
|- Q = (eval1 ` R )   &    |- K = ( Base ` R )   &    |- W = (Poly1 ` R )   &    |- P = ( R ^s K )   &    |- B = ( Base ` W )   &    |- ( ph -> R e. CRing )   &    |- ( ( ph /\ x e. N ) -> Y e. B )   &    |- ( ph -> N C_ NN0 )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> C e. K )   =>    |- ( ph -> ( ( Q ` ( W gsumg ( x e. N |-> Y ) ) ) ` C ) = ( R gsumg ( x e. N |-> ( ( Q ` Y ) ` C ) ) ) )
Theorem	evl1gsummul 19724*	Univariate polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by AV, 15-Sep-2019.)
|- Q = (eval1 ` R )   &    |- K = ( Base ` R )   &    |- W = (Poly1 ` R )   &    |- P = ( R ^s K )   &    |- B = ( Base ` W )   &    |- ( ph -> R e. CRing )   &    |- ( ( ph /\ x e. N ) -> Y e. B )   &    |- ( ph -> N C_ NN0 )   &    |- .1. = ( 1r ` W )   &    |- G = (mulGrp ` W )   &    |- H = (mulGrp ` P )   &    |- ( ph -> ( x e. N |-> Y ) finSupp .1. )   =>    |- ( ph -> ( Q ` ( G gsumg ( x e. N |-> Y ) ) ) = ( H gsumg ( x e. N |-> ( Q ` Y ) ) ) )
Theorem	evl1varpw 19725	Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd 19722, the proof is shorter using evls1varpw 19691 instead of proving it directly. (Contributed by AV, 15-Sep-2019.)
|- Q = (eval1 ` R )   &    |- W = (Poly1 ` R )   &    |- G = (mulGrp ` W )   &    |- X = (var1 ` R )   &    |- B = ( Base ` R )   &    |- .^ = (.g ` G )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( Q ` ( N .^ X ) ) = ( N (.g ` (mulGrp ` ( R ^s B ) ) ) ( Q ` X ) ) )
Theorem	evl1varpwval 19726	Value of a univariate polynomial evaluation mapping the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-Sep-2019.)
|- Q = (eval1 ` R )   &    |- W = (Poly1 ` R )   &    |- G = (mulGrp ` W )   &    |- X = (var1 ` R )   &    |- B = ( Base ` R )   &    |- .^ = (.g ` G )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> C e. B )   &    |- H = (mulGrp ` R )   &    |- E = (.g ` H )   =>    |- ( ph -> ( ( Q ` ( N .^ X ) ) ` C ) = ( N E C ) )
Theorem	evl1scvarpw 19727	Univariate polynomial evaluation maps a multiple of an exponentiation of a variable to the multiple of an exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019.)
|- Q = (eval1 ` R )   &    |- W = (Poly1 ` R )   &    |- G = (mulGrp ` W )   &    |- X = (var1 ` R )   &    |- B = ( Base ` R )   &    |- .^ = (.g ` G )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. NN0 )   &    |- .X. = ( .s ` W )   &    |- ( ph -> A e. B )   &    |- S = ( R ^s B )   &    |- .xb = ( .r ` S )   &    |- M = (mulGrp ` S )   &    |- F = (.g ` M )   =>    |- ( ph -> ( Q ` ( A .X. ( N .^ X ) ) ) = ( ( B X. { A } ) .xb ( N F ( Q ` X ) ) ) )
Theorem	evl1scvarpwval 19728	Value of a univariate polynomial evaluation mapping a multiple of an exponentiation of a variable to the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019.)
|- Q = (eval1 ` R )   &    |- W = (Poly1 ` R )   &    |- G = (mulGrp ` W )   &    |- X = (var1 ` R )   &    |- B = ( Base ` R )   &    |- .^ = (.g ` G )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. NN0 )   &    |- .X. = ( .s ` W )   &    |- ( ph -> A e. B )   &    |- ( ph -> C e. B )   &    |- H = (mulGrp ` R )   &    |- E = (.g ` H )   &    |- .x. = ( .r ` R )   =>    |- ( ph -> ( ( Q ` ( A .X. ( N .^ X ) ) ) ` C ) = ( A .x. ( N E C ) ) )
Theorem	evl1gsummon 19729*	Value of a univariate polynomial evaluation mapping an additive group sum of a multiple of an exponentiation of a variable to a group sum of the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019.)
|- Q = (eval1 ` R )   &    |- K = ( Base ` R )   &    |- W = (Poly1 ` R )   &    |- B = ( Base ` W )   &    |- X = (var1 ` R )   &    |- H = (mulGrp ` R )   &    |- E = (.g ` H )   &    |- G = (mulGrp ` W )   &    |- .^ = (.g ` G )   &    |- .X. = ( .s ` W )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> A. x e. M A e. K )   &    |- ( ph -> M C_ NN0 )   &    |- ( ph -> M e. Fin )   &    |- ( ph -> A. x e. M N e. NN0 )   &    |- ( ph -> C e. K )   =>    |- ( ph -> ( ( Q ` ( W gsumg ( x e. M |-> ( A .X. ( N .^ X ) ) ) ) ) ` C ) = ( R gsumg ( x e. M |-> ( A .x. ( N E C ) ) ) ) )
10.11  The complex numbers as an algebraic extensible structure
10.11.1  Definition and basic properties
Syntax	cpsmet 19730	Extend class notation with the class of all pseudometric spaces.
class PsMet
Syntax	cxmt 19731	Extend class notation with the class of all extended metric spaces.
class *Met
Syntax	cme 19732	Extend class notation with the class of all metrics.
class Met
Syntax	cbl 19733	Extend class notation with the metric space ball function.
class ball
Syntax	cfbas 19734	Extend class definition to include the class of filter bases.
class fBas
Syntax	cfg 19735	Extend class definition to include the filter generating function.
class filGen
Syntax	cmopn 19736	Extend class notation with a function mapping each metric space to the family of its open sets.
class MetOpen
Syntax	cmetu 19737	Extend class notation with the function mapping metrics to the uniform structure generated by that metric.
class metUnif
Definition	df-psmet 19738*	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 19739*	Define the set of all extended metrics on a given base set. The definition is similar to df-met 19740, 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 19740*	Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 22126. However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of [Gleason] p. 223. The 4 properties in Gleason's definition are shown by met0 22148, metgt0 22164, metsym 22155, and mettri 22157. (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 19741*	Define the metric space ball function. See blval 22191 for its value. (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 19742	Define a function whose value is the family of open sets of a metric space. See elmopn 22247 for its main property. (Contributed by NM, 1-Sep-2006.)
|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
Definition	df-fbas 19743*	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 19744*	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 19745*	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 ) ) ) ) )
Syntax	ccnfld 19746	Extend class notation with the field of complex numbers.
class ℂfld
Definition	df-cnfld 19747	The field of complex numbers. Other number fields and rings can be constructed by applying the ↾s restriction operator, for instance (ℂfld |` AA ) is the field of algebraic numbers. The contract of this set is defined entirely by cnfldex 19749, cnfldadd 19751, cnfldmul 19752, cnfldcj 19753, cnfldtset 19754, cnfldle 19755, cnfldds 19756, and cnfldbas 19750. 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.) (New usage is discouraged.)
|- ℂfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. } ) )
Theorem	cnfldstr 19748	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 19749	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 19750	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	cnfldadd 19751	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.)
|- + = ( +g ` ℂfld )
Theorem	cnfldmul 19752	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.)
|- x. = ( .r ` ℂfld )
Theorem	cnfldcj 19753	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 19754	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.)
|- ( MetOpen ` ( abs o. - ) ) = (TopSet ` ℂfld )
Theorem	cnfldle 19755	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.)
|- <_ = ( le ` ℂfld )
Theorem	cnfldds 19756	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.)
|- ( abs o. - ) = ( dist ` ℂfld )
Theorem	cnfldunif 19757	The uniform structure component of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.)
|- (metUnif ` ( abs o. - ) ) = ( UnifSet ` ℂfld )
Theorem	cnfldfun 19758	The field of complex numbers is a function. (Contributed by AV, 14-Nov-2021.)
|- Fun ℂfld
Theorem	cnfldfunALT 19759	Alternate proof of cnfldfun 19758 (much shorter proof, using cnfldstr 19748 and structn0fun 15869: in addition, it must be shown that (/) e/ ℂfld). (Contributed by AV, 18-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
|- Fun ℂfld
Theorem	xrsstr 19760	The extended real structure is a structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- RR*s Struct <. 1 , ; 1 2 >.
Theorem	xrsex 19761	The extended real structure is a set. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- RR*s e. _V
Theorem	xrsbas 19762	The base set of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- RR* = ( Base ` RR*s )
Theorem	xrsadd 19763	The addition operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- +e = ( +g ` RR*s )
Theorem	xrsmul 19764	The multiplication operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- xe = ( .r ` RR*s )
Theorem	xrstset 19765	The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- (ordTop ` <_ ) = (TopSet ` RR*s )
Theorem	xrsle 19766	The ordering of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- <_ = ( le ` RR*s )
Theorem	cncrng 19767	The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.)
|- ℂfld e. CRing
Theorem	cnring 19768	The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- ℂfld e. Ring
Theorem	xrsmcmn 19769	The multiplicative group of the extended reals forms a commutative monoid (even though the additive group is not, see xrsmgmdifsgrp 19783.) (Contributed by Mario Carneiro, 21-Aug-2015.)
|- (mulGrp ` RR*s ) e. CMnd
Theorem	cnfld0 19770	The zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- 0 = ( 0g ` ℂfld )
Theorem	cnfld1 19771	The unit element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- 1 = ( 1r ` ℂfld )
Theorem	cnfldneg 19772	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 19773	The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- + = ( +f ` ℂfld )
Theorem	cnfldsub 19774	The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- - = ( -g ` ℂfld )
Theorem	cndrng 19775	The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- ℂfld e. DivRing
Theorem	cnflddiv 19776	The division operation in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- / = (/r ` ℂfld )
Theorem	cnfldinv 19777	The multiplicative inverse in the field of complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ( ( X e. CC /\ X =/= 0 ) -> ( ( invr ` ℂfld ) ` X ) = ( 1 / X ) )
Theorem	cnfldmulg 19778	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 19779	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	cnsrng 19780	The complex numbers form a *-ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ℂfld e. *Ring
Theorem	xrsmgm 19781	The (additive group of the) extended reals is a magma. (Contributed by AV, 30-Jan-2020.)
|- RR*s e. Mgm
Theorem	xrsnsgrp 19782	The (additive group of the) extended reals is not a semigroup. (Contributed by AV, 30-Jan-2020.)
|- RR*s e/ SGrp
Theorem	xrsmgmdifsgrp 19783	The (additive group of the) extended reals is a magma, but not a semigroup, and therefore also no monoid and no group, in contrast to the multiplicative group, see xrsmcmn 19769. (Contributed by AV, 30-Jan-2020.)
|- RR*s e. (Mgm \ SGrp )
Theorem	xrs1mnd 19784	The extended real numbers, restricted to RR* \ { -oo }, form a monoid - in contrast to the full structure, see xrsmgmdifsgrp 19783. (Contributed by Mario Carneiro, 27-Nov-2014.)
|- R = ( RR*s ↾s ( RR* \ { -oo } ) )   =>    |- R e. Mnd
Theorem	xrs10 19785	The zero of the extended real number monoid. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- R = ( RR*s ↾s ( RR* \ { -oo } ) )   =>    |- 0 = ( 0g ` R )
Theorem	xrs1cmn 19786	The extended real numbers restricted to RR* \ { -oo } form a commutative monoid. They are not a group because 1 + +oo = 2 + +oo even though 1 =/= 2. (Contributed by Mario Carneiro, 27-Nov-2014.)
|- R = ( RR*s ↾s ( RR* \ { -oo } ) )   =>    |- R e. CMnd
Theorem	xrge0subm 19787	The nonnegative extended real numbers are a submonoid of the nonnegative-infinite extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- R = ( RR*s ↾s ( RR* \ { -oo } ) )   =>    |- ( 0 [,] +oo ) e. (SubMnd ` R )
Theorem	xrge0cmn 19788	The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- ( RR*s ↾s ( 0 [,] +oo ) ) e. CMnd
Theorem	xrsds 19789*	The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- D = ( dist ` RR*s )   =>    |- D = ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) )
Theorem	xrsdsval 19790	The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- D = ( dist ` RR*s )   =>    |- ( ( A e. RR* /\ B e. RR* ) -> ( A D B ) = if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) )
Theorem	xrsdsreval 19791	The metric of the extended real number structure coincides with the real number metric on the reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- D = ( dist ` RR*s )   =>    |- ( ( A e. RR /\ B e. RR ) -> ( A D B ) = ( abs ` ( A - B ) ) )
Theorem	xrsdsreclblem 19792	Lemma for xrsdsreclb 19793. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- D = ( dist ` RR*s )   =>    |- ( ( ( A e. RR* /\ B e. RR* /\ A =/= B ) /\ A <_ B ) -> ( ( B +e -e A ) e. RR -> ( A e. RR /\ B e. RR ) ) )
Theorem	xrsdsreclb 19793	The metric of the extended real number structure is only real when both arguments are real. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- D = ( dist ` RR*s )   =>    |- ( ( A e. RR* /\ B e. RR* /\ A =/= B ) -> ( ( A D B ) e. RR <-> ( A e. RR /\ B e. RR ) ) )
Theorem	cnsubmlem 19794*	Lemma for nn0subm 19801 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 19795*	Lemma for resubdrg 19954 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 19796*	Lemma for resubdrg 19954 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	cnsubdrglem 19797*	Lemma for resubdrg 19954 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 )   &    |- ( ( x e. A /\ x =/= 0 ) -> ( 1 / x ) e. A )   =>    |- ( A e. (SubRing ` ℂfld ) /\ (ℂfld ↾s A ) e. DivRing )
Theorem	qsubdrg 19798	The rational numbers form a division subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ( QQ e. (SubRing ` ℂfld ) /\ (ℂfld ↾s QQ ) e. DivRing )
Theorem	zsubrg 19799	The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ZZ e. (SubRing ` ℂfld )
Theorem	gzsubrg 19800	The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ZZ[_i] e. (SubRing ` ℂfld )