P. 361 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36001-36100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pwfi2en 36001*	Finitely supported indicator functions are equinumerous to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Revised by AV, 14-Jun-2020.)
|- S = { y e. ( 2o ^m A ) | y finSupp (/) }   =>    |- ( A e. V -> S ~~ ( ~P A i^i Fin ) )
Theorem	frlmpwfi 36002	Formal linear combinations over Z/2Z are equivalent to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Proof shortened by AV, 14-Jun-2020.)
|- R = (ℤ/nℤ ` 2 )   &    |- Y = ( R freeLMod I )   &    |- B = ( Base ` Y )   =>    |- ( I e. V -> B ~~ ( ~P I i^i Fin ) )
Theorem	gicabl 36003	Being Abelian is a group invariant. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.)
|- ( G ~=g𝑔 H -> ( G e. Abel <-> H e. Abel ) )
Theorem	imasgim 36004	A relabeling of the elements of a group induces an isomorphism to the relabeled group. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) (Revised by Mario Carneiro, 11-Aug-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -1-1-onto-> B )   &    |- ( ph -> R e. Grp )   =>    |- ( ph -> F e. ( R GrpIso U ) )
Theorem	basfn 36005	Functionality of the base set extractor. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.)
|- Base Fn _V
Theorem	isnumbasgrplem1 36006	A set which is equipollent to the base set of a definable Abelian group is the base set of some (relabeled) Abelian group. (Contributed by Stefan O'Rear, 8-Jul-2015.)
|- B = ( Base ` R )   =>    |- ( ( R e. Abel /\ C ~~ B ) -> C e. ( Base " Abel ) )
Theorem	harn0 36007	The Hartogs number of a set is never zero. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.)
|- ( S e. V -> (har ` S ) =/= (/) )
Theorem	numinfctb 36008	A numerable infinite set contains a countable subset. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.)
|- ( ( S e. dom card /\ -. S e. Fin ) -> om ~<_ S )
Theorem	isnumbasgrplem2 36009	If the (to be thought of as disjoint, although the proof does not require this) union of a set and its Hartogs number supports a group structure (more generally, a cancellative magma), then the set must be numerable. (Contributed by Stefan O'Rear, 9-Jul-2015.)
|- ( ( S u. (har ` S ) ) e. ( Base " Grp ) -> S e. dom card )
Theorem	isnumbasgrplem3 36010	Every nonempty numerable set can be given the structure of an Abelian group, either a finite cyclic group or a vector space over Z/2Z. (Contributed by Stefan O'Rear, 10-Jul-2015.)
|- ( ( S e. dom card /\ S =/= (/) ) -> S e. ( Base " Abel ) )
Theorem	isnumbasabl 36011	A set is numerable iff it and its Hartogs number can be jointly given the structure of an Abelian group. (Contributed by Stefan O'Rear, 9-Jul-2015.)
|- ( S e. dom card <-> ( S u. (har ` S ) ) e. ( Base " Abel ) )
Theorem	isnumbasgrp 36012	A set is numerable iff it and its Hartogs number can be jointly given the structure of a group. (Contributed by Stefan O'Rear, 9-Jul-2015.)
|- ( S e. dom card <-> ( S u. (har ` S ) ) e. ( Base " Grp ) )
Theorem	dfacbasgrp 36013	A choice equivalent in abstract algebra: All nonempty sets admit a group structure. From http://mathoverflow.net/a/12988. (Contributed by Stefan O'Rear, 9-Jul-2015.)
|- (CHOICE <-> ( Base " Grp ) = ( _V \ { (/) } ) )
21.23.42  Noetherian rings and left modules II
Syntax	clnr 36014	Extend class notation with the class of left Noetherian rings.
class LNoeR
Definition	df-lnr 36015	A ring is left-Noetherian iff it is Noetherian as a left module over itself. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- LNoeR = { a e. Ring | (ringLMod ` a ) e. LNoeM }
Theorem	islnr 36016	Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( A e. LNoeR <-> ( A e. Ring /\ (ringLMod ` A ) e. LNoeM ) )
Theorem	lnrring 36017	Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( A e. LNoeR -> A e. Ring )
Theorem	lnrlnm 36018	Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( A e. LNoeR -> (ringLMod ` A ) e. LNoeM )
Theorem	islnr2 36019*	Property of being a left-Noetherian ring in terms of finite generation of ideals (the usual "pure ring theory" definition). (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- B = ( Base ` R )   &    |- U = (LIdeal ` R )   &    |- N = (RSpan ` R )   =>    |- ( R e. LNoeR <-> ( R e. Ring /\ A. i e. U E. g e. ( ~P B i^i Fin ) i = ( N ` g ) ) )
Theorem	islnr3 36020	Relate left-Noetherian rings to Noetherian-type closure property of the left ideal system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- B = ( Base ` R )   &    |- U = (LIdeal ` R )   =>    |- ( R e. LNoeR <-> ( R e. Ring /\ U e. (NoeACS ` B ) ) )
Theorem	lnr2i 36021*	Given an ideal in a left-Noetherian ring, there is a finite subset which generates it. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- U = (LIdeal ` R )   &    |- N = (RSpan ` R )   =>    |- ( ( R e. LNoeR /\ I e. U ) -> E. g e. ( ~P I i^i Fin ) I = ( N ` g ) )
Theorem	lpirlnr 36022	Left principal ideal rings are left Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( R e. LPIR -> R e. LNoeR )
Theorem	lnrfrlm 36023	Finite-dimensional free modules over a Noetherian ring are Noetherian. (Contributed by Stefan O'Rear, 3-Feb-2015.)
|- Y = ( R freeLMod I )   =>    |- ( ( R e. LNoeR /\ I e. Fin ) -> Y e. LNoeM )
Theorem	lnrfg 36024	Finitely-generated modules over a Noetherian ring, being homomorphic images of free modules, are Noetherian. (Contributed by Stefan O'Rear, 7-Feb-2015.)
|- S = (Scalar ` M )   =>    |- ( ( M e. LFinGen /\ S e. LNoeR ) -> M e. LNoeM )
Theorem	lnrfgtr 36025	A submodule of a finitely generated module over a Noetherian ring is finitely generated. Often taken as the definition of Noetherian ring. (Contributed by Stefan O'Rear, 7-Feb-2015.)
|- S = (Scalar ` M )   &    |- U = ( LSubSp ` M )   &    |- N = ( M ↾s P )   =>    |- ( ( M e. LFinGen /\ S e. LNoeR /\ P e. U ) -> N e. LFinGen )
21.23.43  Hilbert's Basis Theorem
Syntax	cldgis 36026	The leading ideal sequence used in the Hilbert Basis Theorem.
class ldgIdlSeq
Definition	df-ldgis 36027*	Define a function which carries polynomial ideals to the sequence of coefficient ideals of leading coefficients of degree- x elements in the polynomial ideal. The proof that this map is strictly monotone is the core of the Hilbert Basis Theorem hbt 36035. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ldgIdlSeq = ( r e. _V |-> ( i e. (LIdeal ` (Poly1 ` r ) ) |-> ( x e. NN0 |-> { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( (coe1 ` k ) ` x ) ) } ) ) )
Theorem	hbtlem1 36028*	Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- S = (ldgIdlSeq ` R )   &    |- D = ( deg1 ` R )   =>    |- ( ( R e. V /\ I e. U /\ X e. NN0 ) -> ( ( S ` I ) ` X ) = { j | E. k e. I ( ( D ` k ) <_ X /\ j = ( (coe1 ` k ) ` X ) ) } )
Theorem	hbtlem2 36029	Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- S = (ldgIdlSeq ` R )   &    |- T = (LIdeal ` R )   =>    |- ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( ( S ` I ) ` X ) e. T )
Theorem	hbtlem7 36030	Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- S = (ldgIdlSeq ` R )   &    |- T = (LIdeal ` R )   =>    |- ( ( R e. Ring /\ I e. U ) -> ( S ` I ) : NN0 --> T )
Theorem	hbtlem4 36031	The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- S = (ldgIdlSeq ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> I e. U )   &    |- ( ph -> X e. NN0 )   &    |- ( ph -> Y e. NN0 )   &    |- ( ph -> X <_ Y )   =>    |- ( ph -> ( ( S ` I ) ` X ) C_ ( ( S ` I ) ` Y ) )
Theorem	hbtlem3 36032	The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- S = (ldgIdlSeq ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> I e. U )   &    |- ( ph -> J e. U )   &    |- ( ph -> I C_ J )   &    |- ( ph -> X e. NN0 )   =>    |- ( ph -> ( ( S ` I ) ` X ) C_ ( ( S ` J ) ` X ) )
Theorem	hbtlem5 36033*	The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- S = (ldgIdlSeq ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> I e. U )   &    |- ( ph -> J e. U )   &    |- ( ph -> I C_ J )   &    |- ( ph -> A. x e. NN0 ( ( S ` J ) ` x ) C_ ( ( S ` I ) ` x ) )   =>    |- ( ph -> I = J )
Theorem	hbtlem6 36034*	There is a finite set of polynomials matching any single stage of the image. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- S = (ldgIdlSeq ` R )   &    |- N = (RSpan ` P )   &    |- ( ph -> R e. LNoeR )   &    |- ( ph -> I e. U )   &    |- ( ph -> X e. NN0 )   =>    |- ( ph -> E. k e. ( ~P I i^i Fin ) ( ( S ` I ) ` X ) C_ ( ( S ` ( N ` k ) ) ` X ) )
Theorem	hbt 36035	The Hilbert Basis Theorem - the ring of univariate polynomials over a Noetherian ring is a Noetherian ring. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. LNoeR -> P e. LNoeR )
21.23.44  Additional material on polynomials [DEPRECATED]
Syntax	cmnc 36036	Extend class notation with the class of monic polynomials.
class Monic
Syntax	cplylt 36037	Extend class notatin with the class of limited-degree polynomials.
class Poly<
Definition	df-mnc 36038*	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 36039*	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 36040	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 36041	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 36042	A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.)
|- ( P e. ( Monic ` S ) -> P e. (Poly ` S ) )
Theorem	mnccoe 36043	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 36044	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 36045	Extend class notation to include the degree function for algebraic numbers.
class degAA
Syntax	cdgraaold 36046	Extend class notation to include the degree function for algebraic numbers (old version).
class degAA
Syntax	cmpaa 36047	Extend class notation to include the minimal polynomial for an algebraic number.
class minPolyAA
Definition	df-dgraa 36048*	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-dgraaOLD 36049*	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.) Obsolete version of df-dgraa 36048 as of 29-Sep-2020. (New usage is discouraged.)
|- degAA = ( x e. AA |-> sup ( { d e. NN | E. p e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` p ) = d /\ ( p ` x ) = 0 ) } , RR , `' < ) )
Definition	df-mpaa 36050*	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 36051*	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	dgraavalOLD 36052*	Value of the degree function on an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) Obsolete version of dgraaval 36051 as of 29-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. AA -> (degAA ` A ) = sup ( { d e. NN | E. p e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` p ) = d /\ ( p ` A ) = 0 ) } , RR , `' < ) )
Theorem	dgraalem 36053*	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	dgraalemOLD 36054*	Properties of the degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) Obsolete version of dgraalem 36053 as of 29-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. AA -> ( (degAA ` A ) e. NN /\ E. p e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` p ) = (degAA ` A ) /\ ( p ` A ) = 0 ) ) )
Theorem	dgraacl 36055	Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( A e. AA -> (degAA ` A ) e. NN )
Theorem	dgraaclOLD 36056	Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.) Obsolete version of dgraacl 36055 as of 29-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. AA -> (degAA ` A ) e. NN )
Theorem	dgraaf 36057	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	dgraafOLD 36058	Degree function on algebraic numbers is a function. (Contributed by Stefan O'Rear, 25-Nov-2014.) Obsolete version of dgraaf 36057 as of 29-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- degAA : AA --> NN
Theorem	dgraaub 36059	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	dgraaubOLD 36060	Upper bound on degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) Obsolete version of dgraaub 36059 as of 29-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ( P e. (Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> (degAA ` A ) <_ (deg ` P ) )
Theorem	dgraa0p 36061	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 36062*	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 36063*	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 36064	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 36065	Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.)
|- ( A e. AA -> (minPolyAA ` A ) e. (Poly ` QQ ) )
Theorem	mpaadgr 36066	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 36067	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 36068	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 36069	Extend class notation with the integral-over predicate.
class IntgOver
Syntax	cza 36070	Extend class notation with the class of algebraic integers.
class ℤ
Definition	df-itgo 36071*	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 36074. 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 36072	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 36073*	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 36074	The standard algebraic numbers AA are generated by IntgOver. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- AA = (IntgOver ` QQ )
Theorem	itgoss 36075	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 36076	All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- (IntgOver ` S ) C_ CC
Theorem	cnsrexpcl 36077	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 36078*	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 36079	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 36080*	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 36081	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 36082	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 36083	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 36084	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 36085*	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 36086*	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 36087	Syntax for module endomorphism algebra.
class MEndo
Definition	df-mend 36088*	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 36089	Lemma to shorten proofs of algbase 36090 through algvsca 36094. (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 36090	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 36091	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 36092	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 36093	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 36094	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 36095*	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 36096	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 36097*	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 36098	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 36099*	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 36100	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 ) )