P. 378 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37701-37800   *Has distinct variable group(s)

Type	Label	Description
Statement
20.25.43  Additional material on polynomials [DEPRECATED]
Syntax	cmnc 37701	Extend class notation with the class of monic polynomials.
class Monic
Syntax	cplylt 37702	Extend class notatin with the class of limited-degree polynomials.
class Poly<
Definition	df-mnc 37703*	Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.)
|- Monic = ( s e. ~P CC |-> { p e. (Poly ` s ) | ( (coeff ` p ) ` (deg ` p ) ) = 1 } )
Definition	df-plylt 37704*	Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.)
|- Poly< = ( s e. ~P CC , x e. NN0 |-> { p e. (Poly ` s ) | ( p = 0p \/ (deg ` p ) < x ) } )
Theorem	dgrsub2 37705	Subtracting two polynomials with the same degree and top coefficient gives a polynomial of strictly lower degree. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- N = (deg ` F )   =>    |- ( ( ( F e. (Poly ` S ) /\ G e. (Poly ` T ) ) /\ ( (deg ` G ) = N /\ N e. NN /\ ( (coeff ` F ) ` N ) = ( (coeff ` G ) ` N ) ) ) -> (deg ` ( F oF - G ) ) < N )
Theorem	elmnc 37706	Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.)
|- ( P e. ( Monic ` S ) <-> ( P e. (Poly ` S ) /\ ( (coeff ` P ) ` (deg ` P ) ) = 1 ) )
Theorem	mncply 37707	A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.)
|- ( P e. ( Monic ` S ) -> P e. (Poly ` S ) )
Theorem	mnccoe 37708	A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014.)
|- ( P e. ( Monic ` S ) -> ( (coeff ` P ) ` (deg ` P ) ) = 1 )
Theorem	mncn0 37709	A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014.)
|- ( P e. ( Monic ` S ) -> P =/= 0p )
20.25.44  Degree and minimal polynomial of algebraic numbers
Syntax	cdgraa 37710	Extend class notation to include the degree function for algebraic numbers.
class degAA
Syntax	cmpaa 37711	Extend class notation to include the minimal polynomial for an algebraic number.
class minPolyAA
Definition	df-dgraa 37712*	Define the degree of an algebraic number as the smallest degree of any nonzero polynomial which has said number as a root. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Revised by AV, 29-Sep-2020.)
|- degAA = ( x e. AA |-> inf ( { d e. NN | E. p e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` p ) = d /\ ( p ` x ) = 0 ) } , RR , < ) )
Definition	df-mpaa 37713*	Define the minimal polynomial of an algebraic number as the unique monic polynomial which achieves the minimum of degAA. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- minPolyAA = ( x e. AA |-> ( iota_ p e. (Poly ` QQ ) ( (deg ` p ) = (degAA ` x ) /\ ( p ` x ) = 0 /\ ( (coeff ` p ) ` (degAA ` x ) ) = 1 ) ) )
Theorem	dgraaval 37714*	Value of the degree function on an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Revised by AV, 29-Sep-2020.)
|- ( A e. AA -> (degAA ` A ) = inf ( { d e. NN | E. p e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` p ) = d /\ ( p ` A ) = 0 ) } , RR , < ) )
Theorem	dgraalem 37715*	Properties of the degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.)
|- ( A e. AA -> ( (degAA ` A ) e. NN /\ E. p e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` p ) = (degAA ` A ) /\ ( p ` A ) = 0 ) ) )
Theorem	dgraacl 37716	Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( A e. AA -> (degAA ` A ) e. NN )
Theorem	dgraaf 37717	Degree function on algebraic numbers is a function. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.)
|- degAA : AA --> NN
Theorem	dgraaub 37718	Upper bound on degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.)
|- ( ( ( P e. (Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> (degAA ` A ) <_ (deg ` P ) )
Theorem	dgraa0p 37719	A rational polynomial of degree less than an algebraic number cannot be zero at that number unless it is the zero polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( ( A e. AA /\ P e. (Poly ` QQ ) /\ (deg ` P ) < (degAA ` A ) ) -> ( ( P ` A ) = 0 <-> P = 0p ) )
Theorem	mpaaeu 37720*	An algebraic number has exactly one monic polynomial of the least degree. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( A e. AA -> E! p e. (Poly ` QQ ) ( (deg ` p ) = (degAA ` A ) /\ ( p ` A ) = 0 /\ ( (coeff ` p ) ` (degAA ` A ) ) = 1 ) )
Theorem	mpaaval 37721*	Value of the minimal polynomial of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( A e. AA -> (minPolyAA ` A ) = ( iota_ p e. (Poly ` QQ ) ( (deg ` p ) = (degAA ` A ) /\ ( p ` A ) = 0 /\ ( (coeff ` p ) ` (degAA ` A ) ) = 1 ) ) )
Theorem	mpaalem 37722	Properties of the minimal polynomial of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( A e. AA -> ( (minPolyAA ` A ) e. (Poly ` QQ ) /\ ( (deg ` (minPolyAA ` A ) ) = (degAA ` A ) /\ ( (minPolyAA ` A ) ` A ) = 0 /\ ( (coeff ` (minPolyAA ` A ) ) ` (degAA ` A ) ) = 1 ) ) )
Theorem	mpaacl 37723	Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( A e. AA -> (minPolyAA ` A ) e. (Poly ` QQ ) )
Theorem	mpaadgr 37724	Minimal polynomial has degree the degree of the number. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( A e. AA -> (deg ` (minPolyAA ` A ) ) = (degAA ` A ) )
Theorem	mpaaroot 37725	The minimal polynomial of an algebraic number has the number as a root. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( A e. AA -> ( (minPolyAA ` A ) ` A ) = 0 )
Theorem	mpaamn 37726	Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( A e. AA -> ( (coeff ` (minPolyAA ` A ) ) ` (degAA ` A ) ) = 1 )
20.25.45  Algebraic integers I
Syntax	citgo 37727	Extend class notation with the integral-over predicate.
class IntgOver
Syntax	cza 37728	Extend class notation with the class of algebraic integers.
class ℤ
Definition	df-itgo 37729*	A complex number is said to be integral over a subset if it is the root of a monic polynomial with coefficients from the subset. This definition is typically not used for fields but it works there, see aaitgo 37732. This definition could work for subsets of an arbitrary ring with a more general definition of polynomials. TODO: use Monic (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- IntgOver = ( s e. ~P CC |-> { x e. CC | E. p e. (Poly ` s ) ( ( p ` x ) = 0 /\ ( (coeff ` p ) ` (deg ` p ) ) = 1 ) } )
Definition	df-za 37730	Define an algebraic integer as a complex number which is the root of a monic integer polynomial. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- ℤ = (IntgOver ` ZZ )
Theorem	itgoval 37731*	Value of the integral-over function. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- ( S C_ CC -> (IntgOver ` S ) = { x e. CC | E. p e. (Poly ` S ) ( ( p ` x ) = 0 /\ ( (coeff ` p ) ` (deg ` p ) ) = 1 ) } )
Theorem	aaitgo 37732	The standard algebraic numbers AA are generated by IntgOver. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- AA = (IntgOver ` QQ )
Theorem	itgoss 37733	An integral element is integral over a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- ( ( S C_ T /\ T C_ CC ) -> (IntgOver ` S ) C_ (IntgOver ` T ) )
Theorem	itgocn 37734	All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- (IntgOver ` S ) C_ CC
Theorem	cnsrexpcl 37735	Exponentiation is closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- ( ph -> S e. (SubRing ` ℂfld ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. NN0 )   =>    |- ( ph -> ( X ^ Y ) e. S )
Theorem	fsumcnsrcl 37736*	Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- ( ph -> S e. (SubRing ` ℂfld ) )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. S )   =>    |- ( ph -> sum_ k e. A B e. S )
Theorem	cnsrplycl 37737	Polynomials are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- ( ph -> S e. (SubRing ` ℂfld ) )   &    |- ( ph -> P e. (Poly ` C ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> C C_ S )   =>    |- ( ph -> ( P ` X ) e. S )
Theorem	rgspnval 37738*	Value of the ring-span of a set of elements in a ring. (Contributed by Stefan O'Rear, 7-Dec-2014.)
|- ( ph -> R e. Ring )   &    |- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> A C_ B )   &    |- ( ph -> N = (RingSpan ` R ) )   &    |- ( ph -> U = ( N ` A ) )   =>    |- ( ph -> U = |^| { t e. (SubRing ` R ) | A C_ t } )
Theorem	rgspncl 37739	The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-2014.)
|- ( ph -> R e. Ring )   &    |- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> A C_ B )   &    |- ( ph -> N = (RingSpan ` R ) )   &    |- ( ph -> U = ( N ` A ) )   =>    |- ( ph -> U e. (SubRing ` R ) )
Theorem	rgspnssid 37740	The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- ( ph -> R e. Ring )   &    |- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> A C_ B )   &    |- ( ph -> N = (RingSpan ` R ) )   &    |- ( ph -> U = ( N ` A ) )   =>    |- ( ph -> A C_ U )
Theorem	rgspnmin 37741	The ring-span is contained in all subspaces which contain all the generators. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- ( ph -> R e. Ring )   &    |- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> A C_ B )   &    |- ( ph -> N = (RingSpan ` R ) )   &    |- ( ph -> U = ( N ` A ) )   &    |- ( ph -> S e. (SubRing ` R ) )   &    |- ( ph -> A C_ S )   =>    |- ( ph -> U C_ S )
Theorem	rgspnid 37742	The span of a subring is itself. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- ( ph -> R e. Ring )   &    |- ( ph -> A e. (SubRing ` R ) )   &    |- ( ph -> S = ( (RingSpan ` R ) ` A ) )   =>    |- ( ph -> S = A )
Theorem	rngunsnply 37743*	Adjoining one element to a ring results in a set of polynomial evaluations. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- ( ph -> B e. (SubRing ` ℂfld ) )   &    |- ( ph -> X e. CC )   &    |- ( ph -> S = ( (RingSpan ` ℂfld ) ` ( B u. { X } ) ) )   =>    |- ( ph -> ( V e. S <-> E. p e. (Poly ` B ) V = ( p ` X ) ) )
Theorem	flcidc 37744*	Finite linear combinations with an indicator function. (Contributed by Stefan O'Rear, 5-Dec-2014.)
|- ( ph -> F = ( j e. S |-> if ( j = K , 1 , 0 ) ) )   &    |- ( ph -> S e. Fin )   &    |- ( ph -> K e. S )   &    |- ( ( ph /\ i e. S ) -> B e. CC )   =>    |- ( ph -> sum_ i e. S ( ( F ` i ) x. B ) = [_ K / i ]_ B )
20.25.46  Endomorphism algebra
Syntax	cmend 37745	Syntax for module endomorphism algebra.
class MEndo
Definition	df-mend 37746*	Define the endomorphism algebra of a module. (Contributed by Stefan O'Rear, 2-Sep-2015.)
|- MEndo = ( m e. _V |-> [_ ( m LMHom m ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. (Scalar ` ndx ) , (Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` (Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } ) )
Theorem	algstr 37747	Lemma to shorten proofs of algbase 37748 through algvsca 37752. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } )   =>    |- A Struct <. 1 , 6 >.
Theorem	algbase 37748	The base set of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } )   =>    |- ( B e. V -> B = ( Base ` A ) )
Theorem	algaddg 37749	The additive operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } )   =>    |- ( .+ e. V -> .+ = ( +g ` A ) )
Theorem	algmulr 37750	The multiplicative operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } )   =>    |- ( .X. e. V -> .X. = ( .r ` A ) )
Theorem	algsca 37751	The set of scalars of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } )   =>    |- ( S e. V -> S = (Scalar ` A ) )
Theorem	algvsca 37752	The scalar product operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } )   =>    |- ( .x. e. V -> .x. = ( .s ` A ) )
Theorem	mendval 37753*	Value of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.)
|- B = ( M LMHom M )   &    |- .+ = ( x e. B , y e. B |-> ( x oF ( +g ` M ) y ) )   &    |- .X. = ( x e. B , y e. B |-> ( x o. y ) )   &    |- S = (Scalar ` M )   &    |- .x. = ( x e. ( Base ` S ) , y e. B |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) )   =>    |- ( M e. X -> (MEndo ` M ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) )
Theorem	mendbas 37754	Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.)
|- A = (MEndo ` M )   =>    |- ( M LMHom M ) = ( Base ` A )
Theorem	mendplusgfval 37755*	Addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.)
|- A = (MEndo ` M )   &    |- B = ( Base ` A )   &    |- .+ = ( +g ` M )   =>    |- ( +g ` A ) = ( x e. B , y e. B |-> ( x oF .+ y ) )
Theorem	mendplusg 37756	A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.)
|- A = (MEndo ` M )   &    |- B = ( Base ` A )   &    |- .+ = ( +g ` M )   &    |- .+b = ( +g ` A )   =>    |- ( ( X e. B /\ Y e. B ) -> ( X .+b Y ) = ( X oF .+ Y ) )
Theorem	mendmulrfval 37757*	Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.)
|- A = (MEndo ` M )   &    |- B = ( Base ` A )   =>    |- ( .r ` A ) = ( x e. B , y e. B |-> ( x o. y ) )
Theorem	mendmulr 37758	A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.)
|- A = (MEndo ` M )   &    |- B = ( Base ` A )   &    |- .x. = ( .r ` A )   =>    |- ( ( X e. B /\ Y e. B ) -> ( X .x. Y ) = ( X o. Y ) )
Theorem	mendsca 37759	The module endomorphism algebra has the same scalars as the underlying module. (Contributed by Stefan O'Rear, 2-Sep-2015.)
|- A = (MEndo ` M )   &    |- S = (Scalar ` M )   =>    |- S = (Scalar ` A )
Theorem	mendvscafval 37760*	Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.)
|- A = (MEndo ` M )   &    |- .x. = ( .s ` M )   &    |- B = ( Base ` A )   &    |- S = (Scalar ` M )   &    |- K = ( Base ` S )   &    |- E = ( Base ` M )   =>    |- ( .s ` A ) = ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) )
Theorem	mendvsca 37761	A specific scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.)
|- A = (MEndo ` M )   &    |- .x. = ( .s ` M )   &    |- B = ( Base ` A )   &    |- S = (Scalar ` M )   &    |- K = ( Base ` S )   &    |- E = ( Base ` M )   &    |- .xb = ( .s ` A )   =>    |- ( ( X e. K /\ Y e. B ) -> ( X .xb Y ) = ( ( E X. { X } ) oF .x. Y ) )
Theorem	mendring 37762	The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- A = (MEndo ` M )   =>    |- ( M e. LMod -> A e. Ring )
Theorem	mendlmod 37763	The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.)
|- A = (MEndo ` M )   &    |- S = (Scalar ` M )   =>    |- ( ( M e. LMod /\ S e. CRing ) -> A e. LMod )
Theorem	mendassa 37764	The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.)
|- A = (MEndo ` M )   &    |- S = (Scalar ` M )   =>    |- ( ( M e. LMod /\ S e. CRing ) -> A e. AssAlg )
20.25.47  Subfields
Syntax	csdrg 37765	Syntax for subfields (sub-division-rings).
class SubDRing
Definition	df-sdrg 37766*	A sub-division-ring is a subset of a division ring's set which is a division ring under the induced operation. If the overring is commutative this is a field; no special consideration is made of the fields in the center of a skew field. (Contributed by Stefan O'Rear, 3-Oct-2015.)
|- SubDRing = ( w e. DivRing |-> { s e. (SubRing ` w ) | ( w ↾s s ) e. DivRing } )
Theorem	issdrg 37767	Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015.)
|- ( S e. (SubDRing ` R ) <-> ( R e. DivRing /\ S e. (SubRing ` R ) /\ ( R ↾s S ) e. DivRing ) )
Theorem	issdrg2 37768*	Property of a division subring (closure version). (Contributed by Mario Carneiro, 3-Oct-2015.)
|- I = ( invr ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( S e. (SubDRing ` R ) <-> ( R e. DivRing /\ S e. (SubRing ` R ) /\ A. x e. ( S \ { .0. } ) ( I ` x ) e. S ) )
Theorem	acsfn1p 37769*	Construction of a closure rule from a one-parameter partial operation. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- ( ( X e. V /\ A. b e. Y E e. X ) -> { a e. ~P X | A. b e. ( a i^i Y ) E e. a } e. (ACS ` X ) )
Theorem	subrgacs 37770	Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- B = ( Base ` R )   =>    |- ( R e. Ring -> (SubRing ` R ) e. (ACS ` B ) )
Theorem	sdrgacs 37771	Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015.)
|- B = ( Base ` R )   =>    |- ( R e. DivRing -> (SubDRing ` R ) e. (ACS ` B ) )
Theorem	cntzsdrg 37772	Centralizers in division rings/fields are subfields. (Contributed by Mario Carneiro, 3-Oct-2015.)
|- B = ( Base ` R )   &    |- M = (mulGrp ` R )   &    |- Z = (Cntz ` M )   =>    |- ( ( R e. DivRing /\ S C_ B ) -> ( Z ` S ) e. (SubDRing ` R ) )
20.25.48  Cyclic groups and order
Theorem	idomrootle 37773*	No element of an integral domain can have more than N N-th roots. (Contributed by Stefan O'Rear, 11-Sep-2015.)
|- B = ( Base ` R )   &    |- .^ = (.g ` (mulGrp ` R ) )   =>    |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( # ` { y e. B | ( N .^ y ) = X } ) <_ N )
Theorem	idomodle 37774*	Limit on the number of N-th roots of unity in an integral domain. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- G = ( (mulGrp ` R ) ↾s (Unit ` R ) )   &    |- B = ( Base ` G )   &    |- O = ( od ` G )   =>    |- ( ( R e. IDomn /\ N e. NN ) -> ( # ` { x e. B | ( O ` x ) || N } ) <_ N )
Theorem	fiuneneq 37775	Two finite sets of equal size have a union of the same size iff they were equal. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- ( ( A ~~ B /\ A e. Fin ) -> ( ( A u. B ) ~~ A <-> A = B ) )
Theorem	idomsubgmo 37776*	The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Revised by NM, 17-Jun-2017.)
|- G = ( (mulGrp ` R ) ↾s (Unit ` R ) )   =>    |- ( ( R e. IDomn /\ N e. NN ) -> E* y e. (SubGrp ` G ) ( # ` y ) = N )
Theorem	proot1mul 37777	Any primitive N-th root of unity is a multiple of any other. (Contributed by Stefan O'Rear, 2-Nov-2015.)
|- G = ( (mulGrp ` R ) ↾s (Unit ` R ) )   &    |- O = ( od ` G )   &    |- K = (mrCls ` (SubGrp ` G ) )   =>    |- ( ( ( R e. IDomn /\ N e. NN ) /\ ( X e. ( `' O " { N } ) /\ Y e. ( `' O " { N } ) ) ) -> X e. ( K ` { Y } ) )
Theorem	proot1hash 37778	If an integral domain has a primitive N-th root of unity, it has exactly ( phi ` N ) of them. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- G = ( (mulGrp ` R ) ↾s (Unit ` R ) )   &    |- O = ( od ` G )   =>    |- ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( # ` ( `' O " { N } ) ) = ( phi ` N ) )
Theorem	proot1ex 37779	The complex field has primitive N-th roots of unity for all N. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- G = ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) )   &    |- O = ( od ` G )   =>    |- ( N e. NN -> ( -u 1 ^c ( 2 / N ) ) e. ( `' O " { N } ) )
20.25.49  Cyclotomic polynomials
Syntax	ccytp 37780	Syntax for the sequence of cyclotomic polynomials.
class CytP
Definition	df-cytp 37781*	The Nth cyclotomic polynomial is the polynomial which has as its zeros precisely the primitive Nth roots of unity. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- CytP = ( n e. NN |-> ( (mulGrp ` (Poly1 ` ℂfld ) ) gsumg ( r e. ( `' ( od ` ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) ) ) " { n } ) |-> ( (var1 ` ℂfld ) ( -g ` (Poly1 ` ℂfld ) ) ( (algSc ` (Poly1 ` ℂfld ) ) ` r ) ) ) ) )
Theorem	isdomn3 37782	Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- U = (mulGrp ` R )   =>    |- ( R e. Domn <-> ( R e. Ring /\ ( B \ { .0. } ) e. (SubMnd ` U ) ) )
Theorem	mon1pid 37783	Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- P = (Poly1 ` R )   &    |- .1. = ( 1r ` P )   &    |- M = (Monic1p ` R )   &    |- D = ( deg1 ` R )   =>    |- ( R e. NzRing -> ( .1. e. M /\ ( D ` .1. ) = 0 ) )
Theorem	mon1psubm 37784	Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- P = (Poly1 ` R )   &    |- M = (Monic1p ` R )   &    |- U = (mulGrp ` P )   =>    |- ( R e. NzRing -> M e. (SubMnd ` U ) )
Theorem	deg1mhm 37785	Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- D = ( deg1 ` R )   &    |- B = ( Base ` P )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- Y = ( (mulGrp ` P ) ↾s ( B \ { .0. } ) )   &    |- N = (ℂfld ↾s NN0 )   =>    |- ( R e. Domn -> ( D |` ( B \ { .0. } ) ) e. ( Y MndHom N ) )
Theorem	cytpfn 37786	Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- CytP Fn NN
Theorem	cytpval 37787*	Substitutions for the Nth cyclotomic polynomial. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- T = ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) )   &    |- O = ( od ` T )   &    |- P = (Poly1 ` ℂfld )   &    |- X = (var1 ` ℂfld )   &    |- Q = (mulGrp ` P )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   =>    |- ( N e. NN -> (CytP ` N ) = ( Q gsumg ( r e. ( `' O " { N } ) |-> ( X .- ( A ` r ) ) ) ) )
20.25.50  Miscellaneous topology
Theorem	fgraphopab 37788*	Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( F : A --> B -> F = { <. a , b >. | ( ( a e. A /\ b e. B ) /\ ( F ` a ) = b ) } )
Theorem	fgraphxp 37789*	Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( F : A --> B -> F = { x e. ( A X. B ) | ( F ` ( 1st ` x ) ) = ( 2nd ` x ) } )
Theorem	hausgraph 37790	The graph of a continuous function into a Hausdorff space is closed. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( ( K e. Haus /\ F e. ( J Cn K ) ) -> F e. ( Clsd ` ( J tX K ) ) )
Syntax	ctopsep 37791	The class of separable toplogies.
class TopSep
Syntax	ctoplnd 37792	The class of Lindelöf toplogies.
class TopLnd
Definition	df-topsep 37793*	A topology is separable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015.)
|- TopSep = { j e. Top | E. x e. ~P U. j ( x ~<_ om /\ ( ( cls ` j ) ` x ) = U. j ) }
Definition	df-toplnd 37794*	A topology is Lindelöf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.)
|- TopLnd = { x e. Top | A. y e. ~P x ( U. x = U. y -> E. z e. ~P x ( z ~<_ om /\ U. x = U. z ) ) }
20.26  Mathbox for Jon Pennant
Theorem	ioounsn 37795	The closure of the upper end of an open real interval. (Contributed by Jon Pennant, 8-Jun-2019.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
Theorem	iocunico 37796	Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,] B ) u. ( B [,) C ) ) = ( A (,) C ) )
Theorem	iocinico 37797	The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,] B ) i^i ( B [,) C ) ) = { B } )
Theorem	iocmbl 37798	An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.)
|- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) e. dom vol )
Theorem	cnioobibld 37799*	A bounded, continuous function on an open bounded interval is integrable. The function must be bounded. For a counterexample, consider F = ( x e. ( 0 (,) 1 ) |-> ( 1 / x ) ). See cniccibl 23607 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )   &    |- ( ph -> E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x )   =>    |- ( ph -> F e. L^1 )
Theorem	itgpowd 37800*	The integral of a monomial on a closed bounded interval of the real line. Co-authors TA and MC. (Contributed by Jon Pennant, 31-May-2019.) (Revised by Thierry Arnoux, 14-Jun-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )