P. 358 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35701-35800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mncply 35701	A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.)
|- ( P e. ( Monic ` S ) -> P e. (Poly ` S ) )
Theorem	mnccoe 35702	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 35703	A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014.)
|- ( P e. ( Monic ` S ) -> P =/= 0p )
21.23.45  Degree and minimal polynomial of algebraic numbers
Syntax	cdgraa 35704	Extend class notation to include the degree function for algebraic numbers.
class degAA
Syntax	cmpaa 35705	Extend class notation to include the minimal polynomial for an algebraic number.
class minPolyAA
Definition	df-dgraa 35706*	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.)
|- degAA = ( x e. AA |-> sup ( { d e. NN | E. p e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` p ) = d /\ ( p ` x ) = 0 ) } , RR , `' < ) )
Definition	df-mpaa 35707*	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 35708*	Value of the degree function on an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( A e. AA -> (degAA ` A ) = sup ( { d e. NN | E. p e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` p ) = d /\ ( p ` A ) = 0 ) } , RR , `' < ) )
Theorem	dgraalem 35709*	Properties of the degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( A e. AA -> ( (degAA ` A ) e. NN /\ E. p e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` p ) = (degAA ` A ) /\ ( p ` A ) = 0 ) ) )
Theorem	dgraacl 35710	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 35711	Degree function on algebraic numbers is a function. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- degAA : AA --> NN
Theorem	dgraaub 35712	Upper bound on degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( ( ( P e. (Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> (degAA ` A ) <_ (deg ` P ) )
Theorem	dgraa0p 35713	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 35714*	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 35715*	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 35716	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 35717	Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( A e. AA -> (minPolyAA ` A ) e. (Poly ` QQ ) )
Theorem	mpaadgr 35718	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 35719	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 35720	Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( A e. AA -> ( (coeff ` (minPolyAA ` A ) ) ` (degAA ` A ) ) = 1 )
21.23.46  Algebraic integers I
Syntax	citgo 35721	Extend class notation with the integral-over predicate.
class IntgOver
Syntax	cza 35722	Extend class notation with the class of algebraic integers.
class ℤ
Definition	df-itgo 35723*	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 35726. 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 35724	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 35725*	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 35726	The standard algebraic numbers AA are generated by IntgOver. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- AA = (IntgOver ` QQ )
Theorem	itgoss 35727	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 35728	All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- (IntgOver ` S ) C_ CC
Theorem	cnsrexpcl 35729	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 35730*	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 35731	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 35732*	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 35733	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 35734	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 35735	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 35736	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 35737*	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 35738*	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 )
21.23.47  Endomorphism algebra
Syntax	cmend 35739	Syntax for module endomorphism algebra.
class MEndo
Definition	df-mend 35740*	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 35741	Lemma to shorten proofs of algbase 35742 through algvsca 35746. (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 35742	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 35743	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 35744	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 35745	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 35746	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 35747*	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 35748	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 35749*	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 35750	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 35751*	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 35752	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 35753	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 35754*	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 35755	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 35756	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 35757	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 35758	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 )
21.23.48  Subfields
Syntax	csdrg 35759	Syntax for subfields (sub-division-rings).
class SubDRing
Definition	df-sdrg 35760*	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 35761	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 35762*	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 35763*	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 35764	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 35765	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 35766	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 ) )
21.23.49  Cyclic groups and order
Theorem	idomrootle 35767*	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 35768*	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 35769	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 35770*	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 35771	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	hashgcdlem 35772*	A correspondence between elements of specific GCD and relative primes in a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- A = { y e. ( 0..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 }   &    |- B = { z e. ( 0..^ M ) | ( z gcd M ) = N }   &    |- F = ( x e. A |-> ( x x. N ) )   =>    |- ( ( M e. NN /\ N e. NN /\ N || M ) -> F : A -1-1-onto-> B )
Theorem	hashgcdeq 35773*	Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- ( ( M e. NN /\ N e. NN ) -> ( # ` { x e. ( 0..^ M ) | ( x gcd M ) = N } ) = if ( N || M , ( phi ` ( M / N ) ) , 0 ) )
Theorem	phisum 35774*	The divisor sum identity of the totient function. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- ( N e. NN -> sum_ d e. { x e. NN | x || N } ( phi ` d ) = N )
Theorem	proot1hash 35775	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 35776	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 } ) )
21.23.50  Cyclotomic polynomials
Syntax	ccytp 35777	Syntax for the sequence of cyclotomic polynomials.
class CytP
Definition	df-cytp 35778*	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 35779	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 35780	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 35781	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 35782	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 35783	Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- CytP Fn NN
Theorem	cytpval 35784*	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 ) ) ) ) )
21.23.51  Miscellaneous topology
Theorem	fgraphopab 35785*	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 35786*	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 35787	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 35788	The class of separable toplogies.
class TopSep
Syntax	ctoplnd 35789	The class of Lindelöf toplogies.
class TopLnd
Definition	df-topsep 35790*	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 35791*	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 ) ) }
21.24  Mathbox for Jon Pennant
Theorem	ioounsn 35792	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 35793	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 35794	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 35795	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 35796*	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 22675 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 35797*	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 ) ) )
Theorem	arearect 35798	The area of a rectangle whose sides are parallel to the coordinate axes in ( RR X. RR ) is its width multiplied by its height. (Contributed by Jon Pennant, 19-Mar-2019.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- D e. RR   &    |- A <_ B   &    |- C <_ D   &    |- S = ( ( A [,] B ) X. ( C [,] D ) )   =>    |- (area ` S ) = ( ( B - A ) x. ( D - C ) )
Theorem	areaquad 35799*	The area of a quadrilateral with two sides which are parallel to the y-axis in ( RR X. RR ) is its width multiplied by the average height of its higher edge minus the average height of its lower edge. Co-author TA. (Contributed by Jon Pennant, 31-May-2019.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- D e. RR   &    |- E e. RR   &    |- F e. RR   &    |- A < B   &    |- C <_ E   &    |- D <_ F   &    |- U = ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )   &    |- V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )   &    |- S = { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) }   =>    |- (area ` S ) = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
21.25  Mathbox for Richard Penner
21.25.1  Short Studies
21.25.1.1  Additional work on conditional logical operator
Theorem	ifpan123g 35800	Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
|- ( (if- ( ph , ch , ta ) /\ if- ( ps , th , et ) ) <-> ( ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) /\ ( ( -. ps \/ th ) /\ ( ps \/ et ) ) ) )