P. 167 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 16601-16700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ply1lmod 16601	Univariate polynomials form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. Ring -> P e. LMod )
Theorem	ply1sca 16602	Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. V -> R = (Scalar ` P ) )
Theorem	ply1sca2 16603	Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015.)
|- P = (Poly1 ` R )   =>    |- ( _I ` R ) = (Scalar ` P )
Theorem	ply1mpl0 16604	The univariate polynomial ring has the same zero as the corresponding multivariate polynomial ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 3-Oct-2015.)
|- M = ( 1o mPoly R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   =>    |- .0. = ( 0g ` M )
Theorem	ply1mpl1 16605	The univariate polynomial ring has the same one as the corresponding multivariate polynomial ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 3-Oct-2015.)
|- M = ( 1o mPoly R )   &    |- P = (Poly1 ` R )   &    |- .1. = ( 1r ` P )   =>    |- .1. = ( 1r ` M )
Theorem	ply1ascl 16606	The univariate polynomial ring inherits the multivariate ring's scalar function. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by Fan Zheng, 26-Jun-2016.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   =>    |- A = (algSc ` ( 1o mPoly R ) )
Theorem	subrg1ascl 16607	The scalar injection function in a subring algebra is the same up to a restriction to the subring. (Contributed by Mario Carneiro, 4-Jul-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- H = ( R ↾s T )   &    |- U = (Poly1 ` H )   &    |- ( ph -> T e. (SubRing ` R ) )   &    |- C = (algSc ` U )   =>    |- ( ph -> C = ( A |` T ) )
Theorem	subrg1asclcl 16608	The scalars in a polynomial algebra are in the subring algebra iff the scalar value is in the subring. (Contributed by Mario Carneiro, 4-Jul-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- H = ( R ↾s T )   &    |- U = (Poly1 ` H )   &    |- ( ph -> T e. (SubRing ` R ) )   &    |- B = ( Base ` U )   &    |- K = ( Base ` R )   &    |- ( ph -> X e. K )   =>    |- ( ph -> ( ( A ` X ) e. B <-> X e. T ) )
Theorem	subrgvr1 16609	The variables in a subring polynomial algebra are the same as the original ring. (Contributed by Mario Carneiro, 5-Jul-2015.)
|- X = (var1 ` R )   &    |- ( ph -> T e. (SubRing ` R ) )   &    |- H = ( R ↾s T )   =>    |- ( ph -> X = (var1 ` H ) )
Theorem	subrgvr1cl 16610	The variables in a polynomial algebra are contained in every subring algebra. (Contributed by Mario Carneiro, 5-Jul-2015.)
|- X = (var1 ` R )   &    |- ( ph -> T e. (SubRing ` R ) )   &    |- H = ( R ↾s T )   &    |- U = (Poly1 ` H )   &    |- B = ( Base ` U )   =>    |- ( ph -> X e. B )
Theorem	coe1z 16611	The coefficient vector of 0. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- Y = ( 0g ` R )   =>    |- ( R e. Ring -> (coe1 ` .0. ) = ( NN0 X. { Y } ) )
Theorem	coe1add 16612	The coefficient vector of an addition. (Contributed by Stefan O'Rear, 24-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- B = ( Base ` Y )   &    |- .+b = ( +g ` Y )   &    |- .+ = ( +g ` R )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. B ) -> (coe1 ` ( F .+b G ) ) = ( (coe1 ` F ) o F .+ (coe1 ` G ) ) )
Theorem	coe1addfv 16613	A particular coefficient of an addition. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- B = ( Base ` Y )   &    |- .+b = ( +g ` Y )   &    |- .+ = ( +g ` R )   =>    |- ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( (coe1 ` ( F .+b G ) ) ` X ) = ( ( (coe1 ` F ) ` X ) .+ ( (coe1 ` G ) ` X ) ) )
Theorem	coe1subfv 16614	A particular coefficient of a subtraction. (Contributed by Stefan O'Rear, 23-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- B = ( Base ` Y )   &    |- .- = ( -g ` Y )   &    |- N = ( -g ` R )   =>    |- ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( (coe1 ` ( F .- G ) ) ` X ) = ( ( (coe1 ` F ) ` X ) N ( (coe1 ` G ) ` X ) ) )
Theorem	coe1mul2lem1 16615	An equivalence for coe1mul2 16617. (Contributed by Stefan O'Rear, 25-Mar-2015.)
|- ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) -> ( X o R <_ ( 1o X. { A } ) <-> ( X ` (/) ) e. ( 0 ... A ) ) )
Theorem	coe1mul2lem2 16616*	An equivalence for coe1mul2 16617. (Contributed by Stefan O'Rear, 25-Mar-2015.)
|- H = { d e. ( NN0 ^m 1o ) | d o R <_ ( 1o X. { k } ) }   =>    |- ( k e. NN0 -> ( c e. H |-> ( c ` (/) ) ) : H -1-1-onto-> ( 0 ... k ) )
Theorem	coe1mul2 16617*	The coefficient vector of multiplication in the univariate power series ring. (Contributed by Stefan O'Rear, 25-Mar-2015.)
|- S = (PwSer1 ` R )   &    |- .xb = ( .r ` S )   &    |- .x. = ( .r ` R )   &    |- B = ( Base ` S )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. B ) -> (coe1 ` ( F .xb G ) ) = ( k e. NN0 |-> ( R gsumg ( x e. ( 0 ... k ) |-> ( ( (coe1 ` F ) ` x ) .x. ( (coe1 ` G ) ` ( k - x ) ) ) ) ) ) )
Theorem	coe1mul 16618*	The coefficient vector of multiplication in the univariate polynomial ring. (Contributed by Stefan O'Rear, 25-Mar-2015.)
|- Y = (Poly1 ` R )   &    |- .xb = ( .r ` Y )   &    |- .x. = ( .r ` R )   &    |- B = ( Base ` Y )   =>    |- ( ( R e. Ring /\ F e. B /\ G e. B ) -> (coe1 ` ( F .xb G ) ) = ( k e. NN0 |-> ( R gsumg ( x e. ( 0 ... k ) |-> ( ( (coe1 ` F ) ` x ) .x. ( (coe1 ` G ) ` ( k - x ) ) ) ) ) ) )
Theorem	ply1tmcl 16619	Closure of the expression for a univariate polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- B = ( Base ` P )   =>    |- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( C .x. ( D .^ X ) ) e. B )
Theorem	coe1tm 16620*	Coefficient vector of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- .0. = ( 0g ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   =>    |- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> (coe1 ` ( C .x. ( D .^ X ) ) ) = ( x e. NN0 |-> if ( x = D , C , .0. ) ) )
Theorem	coe1tmfv1 16621	Nonzero coefficient of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- .0. = ( 0g ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   =>    |- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( (coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) = C )
Theorem	coe1tmfv2 16622	Zero coefficient of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- .0. = ( 0g ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> C e. K )   &    |- ( ph -> D e. NN0 )   &    |- ( ph -> F e. NN0 )   &    |- ( ph -> D =/= F )   =>    |- ( ph -> ( (coe1 ` ( C .x. ( D .^ X ) ) ) ` F ) = .0. )
Theorem	coe1tmmul2 16623*	Coefficient vector of a polynomial multiplied on the right by a term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- .0. = ( 0g ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- B = ( Base ` P )   &    |- .xb = ( .r ` P )   &    |- .X. = ( .r ` R )   &    |- ( ph -> A e. B )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> C e. K )   &    |- ( ph -> D e. NN0 )   =>    |- ( ph -> (coe1 ` ( A .xb ( C .x. ( D .^ X ) ) ) ) = ( x e. NN0 |-> if ( D <_ x , ( ( (coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) ) )
Theorem	coe1tmmul 16624*	Coefficient vector of a polynomial multiplied on the left by a term. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- .0. = ( 0g ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- B = ( Base ` P )   &    |- .xb = ( .r ` P )   &    |- .X. = ( .r ` R )   &    |- ( ph -> A e. B )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> C e. K )   &    |- ( ph -> D e. NN0 )   =>    |- ( ph -> (coe1 ` ( ( C .x. ( D .^ X ) ) .xb A ) ) = ( x e. NN0 |-> if ( D <_ x , ( C .X. ( (coe1 ` A ) ` ( x - D ) ) ) , .0. ) ) )
Theorem	coe1tmmul2fv 16625	Function value of a right-multiplication by a term in the shifted domain. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- .0. = ( 0g ` R )   &    |- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- B = ( Base ` P )   &    |- .xb = ( .r ` P )   &    |- .X. = ( .r ` R )   &    |- ( ph -> A e. B )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> C e. K )   &    |- ( ph -> D e. NN0 )   &    |- ( ph -> Y e. NN0 )   =>    |- ( ph -> ( (coe1 ` ( A .xb ( C .x. ( D .^ X ) ) ) ) ` ( D + Y ) ) = ( ( (coe1 ` A ) ` Y ) .X. C ) )
Theorem	coe1pwmul 16626*	Coefficient vector of a polynomial multiplied on the left by a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- .0. = ( 0g ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- B = ( Base ` P )   &    |- .x. = ( .r ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> A e. B )   &    |- ( ph -> D e. NN0 )   =>    |- ( ph -> (coe1 ` ( ( D .^ X ) .x. A ) ) = ( x e. NN0 |-> if ( D <_ x , ( (coe1 ` A ) ` ( x - D ) ) , .0. ) ) )
Theorem	coe1pwmulfv 16627	Function value of a right-multiplication by a variable power in the shifted domain. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- .0. = ( 0g ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- B = ( Base ` P )   &    |- .x. = ( .r ` P )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> A e. B )   &    |- ( ph -> D e. NN0 )   &    |- ( ph -> Y e. NN0 )   =>    |- ( ph -> ( (coe1 ` ( ( D .^ X ) .x. A ) ) ` ( D + Y ) ) = ( (coe1 ` A ) ` Y ) )
Theorem	ply1scltm 16628	A scalar is a term with zero exponent. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- K = ( Base ` R )   &    |- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` P )   &    |- N = (mulGrp ` P )   &    |- .^ = (.g ` N )   &    |- A = (algSc ` P )   =>    |- ( ( R e. Ring /\ F e. K ) -> ( A ` F ) = ( F .x. ( 0 .^ X ) ) )
Theorem	coe1sclmul 16629	Coefficient vector of a polynomial multiplied on the left by a scalar. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- K = ( Base ` R )   &    |- A = (algSc ` P )   &    |- .xb = ( .r ` P )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. K /\ Y e. B ) -> (coe1 ` ( ( A ` X ) .xb Y ) ) = ( ( NN0 X. { X } ) o F .x. (coe1 ` Y ) ) )
Theorem	coe1sclmulfv 16630	A single coefficient of a polynomial multiplied on the left by a scalar. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- K = ( Base ` R )   &    |- A = (algSc ` P )   &    |- .xb = ( .r ` P )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ .0. e. NN0 ) -> ( (coe1 ` ( ( A ` X ) .xb Y ) ) ` .0. ) = ( X .x. ( (coe1 ` Y ) ` .0. ) ) )
Theorem	coe1sclmul2 16631	Coefficient vector of a polynomial multiplied on the right by a scalar. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- K = ( Base ` R )   &    |- A = (algSc ` P )   &    |- .xb = ( .r ` P )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. K /\ Y e. B ) -> (coe1 ` ( Y .xb ( A ` X ) ) ) = ( (coe1 ` Y ) o F .x. ( NN0 X. { X } ) ) )
Theorem	ply1sclf 16632	A scalar polynomial is a polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- K = ( Base ` R )   &    |- B = ( Base ` P )   =>    |- ( R e. Ring -> A : K --> B )
Theorem	coe1scl 16633*	Coefficient vector of a scalar. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. K ) -> (coe1 ` ( A ` X ) ) = ( x e. NN0 |-> if ( x = 0 , X , .0. ) ) )
Theorem	ply1sclid 16634	Recover the base scalar from a scalar polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- K = ( Base ` R )   =>    |- ( ( R e. Ring /\ X e. K ) -> X = ( (coe1 ` ( A ` X ) ) ` 0 ) )
Theorem	ply1sclf1 16635	The polynomial scalar function is injective. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- K = ( Base ` R )   &    |- B = ( Base ` P )   =>    |- ( R e. Ring -> A : K -1-1-> B )
Theorem	ply1scl0 16636	The zero scalar is zero. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- .0. = ( 0g ` R )   &    |- Y = ( 0g ` P )   =>    |- ( R e. Ring -> ( A ` .0. ) = Y )
Theorem	ply1scln0 16637	Nonzero scalars create nonzero polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- .0. = ( 0g ` R )   &    |- Y = ( 0g ` P )   &    |- K = ( Base ` R )   =>    |- ( ( R e. Ring /\ X e. K /\ X =/= .0. ) -> ( A ` X ) =/= Y )
Theorem	ply1scl1 16638	The one scalar is the unit polynomial. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- P = (Poly1 ` R )   &    |- A = (algSc ` P )   &    |- .1. = ( 1r ` R )   &    |- N = ( 1r ` P )   =>    |- ( R e. Ring -> ( A ` .1. ) = N )
Theorem	ply1coe 16639*	Decompose a univariate polynomial as a sum of powers. (Contributed by Stefan O'Rear, 21-Mar-2015.)
|- P = (Poly1 ` R )   &    |- X = (var1 ` R )   &    |- B = ( Base ` P )   &    |- .x. = ( .s ` P )   &    |- M = (mulGrp ` P )   &    |- .^ = (.g ` M )   &    |- A = (coe1 ` K )   &    |- R e. _V   =>    |- ( ( R e. CRing /\ K e. B ) -> K = ( P gsumg ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) )
10.11  The complex numbers as an extensible structure
10.11.1  Definition and basic properties
Syntax	cpsmet 16640	Extend class notation with the class of all pseudometric spaces.
class PsMet
Syntax	cxmt 16641	Extend class notation with the class of all extended metric spaces.
class * Met
Syntax	cme 16642	Extend class notation with the class of all metrics.
class Met
Syntax	cbl 16643	Extend class notation with the metric space ball function.
class ball
Syntax	cfbas 16644	Extend class definition to include the class of filter bases.
class fBas
Syntax	cfg 16645	Extend class definition to include the filter generating function.
class filGen
Syntax	cmopn 16646	Extend class notation with a function mapping each metric space to the family of its open sets.
class MetOpen
Syntax	cmetuOLD 16647	Extend class notation with the function mapping metrics to the uniform structure generated by that metric.
class metUnifOLD
Syntax	cmetu 16648	Extend class notation with the function mapping metrics to the uniform structure generated by that metric.
class metUnif
Definition	df-psmet 16649*	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 16650*	Define the set of all extended metrics on a given base set. The definition is similar to df-met 16651, 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 16651*	Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 18304. 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 18326, metgt0 18342, metsym 18333, and mettri 18335. (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 16652*	Define the metric space ball function. See blval 18369 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 16653	Define a function whose value is the family of open sets of a metric space. See elmopn 18425 for its main property. (Contributed by NM, 1-Sep-2006.)
|- MetOpen = ( d e. U. ran * Met |-> ( topGen ` ran ( ball ` d ) ) )
Definition	df-fbas 16654*	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 16655*	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-metuOLD 16656*	Define the function mapping metrics to the uniform structure generated by that metric. (Contributed by Thierry Arnoux, 1-Dec-2017.) (New usage is discouraged.)
|- metUnifOLD = ( d e. U. ran * Met |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
Definition	df-metu 16657*	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 16658	Extend class notation with the field of complex numbers.
class ℂfld
Definition	df-cnfld 16659	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 16661, cnfldadd 16663, cnfldmul 16664, cnfldcj 16665, cnfldtset 16666, cnfldle 16667, cnfldds 16668, and cnfldbas 16662. 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 16660	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 16661	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 16662	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 16663	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 16664	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 16665	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 16666	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 16667	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 16668	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 16669	The uniform structure component of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.)
|- (metUnif ` ( abs o. - ) ) = ( UnifSet ` ℂfld )
Theorem	xrsstr 16670	The extended real structure is a structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- RR* s Struct <. 1 , ; 1 2 >.
Theorem	xrsex 16671	The extended real structure is a set. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- RR* s e. _V
Theorem	xrsbas 16672	The base set of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- RR* = ( Base ` RR* s )
Theorem	xrsadd 16673	The addition operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- + e = ( +g ` RR* s )
Theorem	xrsmul 16674	The multiplication operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- x e = ( .r ` RR* s )
Theorem	xrstset 16675	The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- (ordTop ` <_ ) = (TopSet ` RR* s )
Theorem	xrsle 16676	The ordering of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- <_ = ( le ` RR* s )
Theorem	cncrng 16677	The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.)
|- ℂfld e. CRing
Theorem	cnrng 16678	The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- ℂfld e. Ring
Theorem	xrsmcmn 16679	The multiplicative group of the extended reals forms a commutative monoid (even though the additive group is not, see xrs1mnd 16691.) (Contributed by Mario Carneiro, 21-Aug-2015.)
|- (mulGrp ` RR* s ) e. CMnd
Theorem	cnfld0 16680	The zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- 0 = ( 0g ` ℂfld )
Theorem	cnfld1 16681	The unit element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- 1 = ( 1r ` ℂfld )
Theorem	cnfldneg 16682	The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- ( X e. CC -> ( ( inv g ` ℂfld ) ` X ) = -u X )
Theorem	cnfldplusf 16683	The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- + = ( + f ` ℂfld )
Theorem	cnfldsub 16684	The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- - = ( -g ` ℂfld )
Theorem	cndrng 16685	The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- ℂfld e. DivRing
Theorem	cnflddiv 16686	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 16687	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 16688	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 16689	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 16690	The complex numbers form a *-ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ℂfld e. *Ring
Theorem	xrs1mnd 16691	The extended real numbers, restricted to RR* \ { -oo }, form a monoid. The full structure is not a monoid or even a semigroup because associativity fails for 1 + ( -oo + +oo ) = 1 =/= ( 1 + -oo ) + +oo = 0. (Contributed by Mario Carneiro, 27-Nov-2014.)
|- R = ( RR* s ↾s ( RR* \ { -oo } ) )   =>    |- R e. Mnd
Theorem	xrs10 16692	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 16693	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 16694	The nonnegative extended real numbers are a submonoid of the non-negative-infinite extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- R = ( RR* s ↾s ( RR* \ { -oo } ) )   =>    |- ( 0 [,] +oo ) e. (SubMnd ` R )
Theorem	xrge0cmn 16695	The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- ( RR* s ↾s ( 0 [,] +oo ) ) e. CMnd
Theorem	xrsds 16696*	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 16697	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 16698	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 16699	Lemma for xrsdsreclb 16700. (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 16700	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 ) ) )