Home | Metamath
Proof Explorer Theorem List (p. 414 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cdgraa 41301 | Extend class notation to include the degree function for algebraic numbers. |
class degAA | ||
Syntax | cmpaa 41302 | Extend class notation to include the minimal polynomial for an algebraic number. |
class minPolyAA | ||
Definition | df-dgraa 41303* | 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 = (π₯ β πΈ β¦ inf({π β β β£ βπ β ((Polyββ) β {0π})((degβπ) = π β§ (πβπ₯) = 0)}, β, < )) | ||
Definition | df-mpaa 41304* | 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 = (π₯ β πΈ β¦ (β©π β (Polyββ)((degβπ) = (degAAβπ₯) β§ (πβπ₯) = 0 β§ ((coeffβπ)β(degAAβπ₯)) = 1))) | ||
Theorem | dgraaval 41305* | Value of the degree function on an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Revised by AV, 29-Sep-2020.) |
β’ (π΄ β πΈ β (degAAβπ΄) = inf({π β β β£ βπ β ((Polyββ) β {0π})((degβπ) = π β§ (πβπ΄) = 0)}, β, < )) | ||
Theorem | dgraalem 41306* | Properties of the degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.) |
β’ (π΄ β πΈ β ((degAAβπ΄) β β β§ βπ β ((Polyββ) β {0π})((degβπ) = (degAAβπ΄) β§ (πβπ΄) = 0))) | ||
Theorem | dgraacl 41307 | Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β (degAAβπ΄) β β) | ||
Theorem | dgraaf 41308 | Degree function on algebraic numbers is a function. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.) |
β’ degAA:πΈβΆβ | ||
Theorem | dgraaub 41309 | Upper bound on degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.) |
β’ (((π β (Polyββ) β§ π β 0π) β§ (π΄ β β β§ (πβπ΄) = 0)) β (degAAβπ΄) β€ (degβπ)) | ||
Theorem | dgraa0p 41310 | 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.) |
β’ ((π΄ β πΈ β§ π β (Polyββ) β§ (degβπ) < (degAAβπ΄)) β ((πβπ΄) = 0 β π = 0π)) | ||
Theorem | mpaaeu 41311* | An algebraic number has exactly one monic polynomial of the least degree. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β β!π β (Polyββ)((degβπ) = (degAAβπ΄) β§ (πβπ΄) = 0 β§ ((coeffβπ)β(degAAβπ΄)) = 1)) | ||
Theorem | mpaaval 41312* | Value of the minimal polynomial of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β (minPolyAAβπ΄) = (β©π β (Polyββ)((degβπ) = (degAAβπ΄) β§ (πβπ΄) = 0 β§ ((coeffβπ)β(degAAβπ΄)) = 1))) | ||
Theorem | mpaalem 41313 | Properties of the minimal polynomial of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β ((minPolyAAβπ΄) β (Polyββ) β§ ((degβ(minPolyAAβπ΄)) = (degAAβπ΄) β§ ((minPolyAAβπ΄)βπ΄) = 0 β§ ((coeffβ(minPolyAAβπ΄))β(degAAβπ΄)) = 1))) | ||
Theorem | mpaacl 41314 | Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β (minPolyAAβπ΄) β (Polyββ)) | ||
Theorem | mpaadgr 41315 | Minimal polynomial has degree the degree of the number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β (degβ(minPolyAAβπ΄)) = (degAAβπ΄)) | ||
Theorem | mpaaroot 41316 | The minimal polynomial of an algebraic number has the number as a root. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β ((minPolyAAβπ΄)βπ΄) = 0) | ||
Theorem | mpaamn 41317 | Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β ((coeffβ(minPolyAAβπ΄))β(degAAβπ΄)) = 1) | ||
Syntax | citgo 41318 | Extend class notation with the integral-over predicate. |
class IntgOver | ||
Syntax | cza 41319 | Extend class notation with the class of algebraic integers. |
class β€ | ||
Definition | df-itgo 41320* | 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 41323. 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 = (π β π« β β¦ {π₯ β β β£ βπ β (Polyβπ )((πβπ₯) = 0 β§ ((coeffβπ)β(degβπ)) = 1)}) | ||
Definition | df-za 41321 | 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ββ€) | ||
Theorem | itgoval 41322* | Value of the integral-over function. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ (π β β β (IntgOverβπ) = {π₯ β β β£ βπ β (Polyβπ)((πβπ₯) = 0 β§ ((coeffβπ)β(degβπ)) = 1)}) | ||
Theorem | aaitgo 41323 | The standard algebraic numbers πΈ are generated by IntgOver. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ πΈ = (IntgOverββ) | ||
Theorem | itgoss 41324 | An integral element is integral over a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ ((π β π β§ π β β) β (IntgOverβπ) β (IntgOverβπ)) | ||
Theorem | itgocn 41325 | All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ (IntgOverβπ) β β | ||
Theorem | cnsrexpcl 41326 | Exponentiation is closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β (SubRingββfld)) & β’ (π β π β π) & β’ (π β π β β0) β β’ (π β (πβπ) β π) | ||
Theorem | fsumcnsrcl 41327* | Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β (SubRingββfld)) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π) β β’ (π β Ξ£π β π΄ π΅ β π) | ||
Theorem | cnsrplycl 41328 | Polynomials are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β (SubRingββfld)) & β’ (π β π β (PolyβπΆ)) & β’ (π β π β π) & β’ (π β πΆ β π) β β’ (π β (πβπ) β π) | ||
Theorem | rgspnval 41329* | Value of the ring-span of a set of elements in a ring. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
β’ (π β π β Ring) & β’ (π β π΅ = (Baseβπ )) & β’ (π β π΄ β π΅) & β’ (π β π = (RingSpanβπ )) & β’ (π β π = (πβπ΄)) β β’ (π β π = β© {π‘ β (SubRingβπ ) β£ π΄ β π‘}) | ||
Theorem | rgspncl 41330 | The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
β’ (π β π β Ring) & β’ (π β π΅ = (Baseβπ )) & β’ (π β π΄ β π΅) & β’ (π β π = (RingSpanβπ )) & β’ (π β π = (πβπ΄)) β β’ (π β π β (SubRingβπ )) | ||
Theorem | rgspnssid 41331 | The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β Ring) & β’ (π β π΅ = (Baseβπ )) & β’ (π β π΄ β π΅) & β’ (π β π = (RingSpanβπ )) & β’ (π β π = (πβπ΄)) β β’ (π β π΄ β π) | ||
Theorem | rgspnmin 41332 | The ring-span is contained in all subspaces which contain all the generators. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β Ring) & β’ (π β π΅ = (Baseβπ )) & β’ (π β π΄ β π΅) & β’ (π β π = (RingSpanβπ )) & β’ (π β π = (πβπ΄)) & β’ (π β π β (SubRingβπ )) & β’ (π β π΄ β π) β β’ (π β π β π) | ||
Theorem | rgspnid 41333 | The span of a subring is itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β Ring) & β’ (π β π΄ β (SubRingβπ )) & β’ (π β π = ((RingSpanβπ )βπ΄)) β β’ (π β π = π΄) | ||
Theorem | rngunsnply 41334* | Adjoining one element to a ring results in a set of polynomial evaluations. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π΅ β (SubRingββfld)) & β’ (π β π β β) & β’ (π β π = ((RingSpanββfld)β(π΅ βͺ {π}))) β β’ (π β (π β π β βπ β (Polyβπ΅)π = (πβπ))) | ||
Theorem | flcidc 41335* | Finite linear combinations with an indicator function. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β πΉ = (π β π β¦ if(π = πΎ, 1, 0))) & β’ (π β π β Fin) & β’ (π β πΎ β π) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β Ξ£π β π ((πΉβπ) Β· π΅) = β¦πΎ / πβ¦π΅) | ||
Syntax | cmend 41336 | Syntax for module endomorphism algebra. |
class MEndo | ||
Definition | df-mend 41337* | Define the endomorphism algebra of a module. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
β’ MEndo = (π β V β¦ β¦(π LMHom π) / πβ¦({β¨(Baseβndx), πβ©, β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf (+gβπ)π¦))β©, β¨(.rβndx), (π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx), (Scalarβπ)β©, β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf ( Β·π βπ)π¦))β©})) | ||
Theorem | algstr 41338 | Lemma to shorten proofs of algbase 41339 through algvsca 41343. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ π΄ Struct β¨1, 6β© | ||
Theorem | algbase 41339 | The base set of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ (π΅ β π β π΅ = (Baseβπ΄)) | ||
Theorem | algaddg 41340 | The additive operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ ( + β π β + = (+gβπ΄)) | ||
Theorem | algmulr 41341 | The multiplicative operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ ( Γ β π β Γ = (.rβπ΄)) | ||
Theorem | algsca 41342 | The set of scalars of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ (π β π β π = (Scalarβπ΄)) | ||
Theorem | algvsca 41343 | The scalar product operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ ( Β· β π β Β· = ( Β·π βπ΄)) | ||
Theorem | mendval 41344* | Value of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
β’ π΅ = (π LMHom π) & β’ + = (π₯ β π΅, π¦ β π΅ β¦ (π₯ βf (+gβπ)π¦)) & β’ Γ = (π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦)) & β’ π = (Scalarβπ) & β’ Β· = (π₯ β (Baseβπ), π¦ β π΅ β¦ (((Baseβπ) Γ {π₯}) βf ( Β·π βπ)π¦)) β β’ (π β π β (MEndoβπ) = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©})) | ||
Theorem | mendbas 41345 | Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
β’ π΄ = (MEndoβπ) β β’ (π LMHom π) = (Baseβπ΄) | ||
Theorem | mendplusgfval 41346* | Addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π΄ = (MEndoβπ) & β’ π΅ = (Baseβπ΄) & β’ + = (+gβπ) β β’ (+gβπ΄) = (π₯ β π΅, π¦ β π΅ β¦ (π₯ βf + π¦)) | ||
Theorem | mendplusg 41347 | A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π΅ = (Baseβπ΄) & β’ + = (+gβπ) & β’ β = (+gβπ΄) β β’ ((π β π΅ β§ π β π΅) β (π β π) = (π βf + π)) | ||
Theorem | mendmulrfval 41348* | Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π΄ = (MEndoβπ) & β’ π΅ = (Baseβπ΄) β β’ (.rβπ΄) = (π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦)) | ||
Theorem | mendmulr 41349 | A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = (.rβπ΄) β β’ ((π β π΅ β§ π β π΅) β (π Β· π) = (π β π)) | ||
Theorem | mendsca 41350 | The module endomorphism algebra has the same scalars as the underlying module. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π΄ = (MEndoβπ) & β’ π = (Scalarβπ) β β’ π = (Scalarβπ΄) | ||
Theorem | mendvscafval 41351* | Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π΄ = (MEndoβπ) & β’ Β· = ( Β·π βπ) & β’ π΅ = (Baseβπ΄) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ πΈ = (Baseβπ) β β’ ( Β·π βπ΄) = (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦)) | ||
Theorem | mendvsca 41352 | A specific scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ Β· = ( Β·π βπ) & β’ π΅ = (Baseβπ΄) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ πΈ = (Baseβπ) & β’ β = ( Β·π βπ΄) β β’ ((π β πΎ β§ π β π΅) β (π β π) = ((πΈ Γ {π}) βf Β· π)) | ||
Theorem | mendring 41353 | The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΄ = (MEndoβπ) β β’ (π β LMod β π΄ β Ring) | ||
Theorem | mendlmod 41354 | The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π = (Scalarβπ) β β’ ((π β LMod β§ π β CRing) β π΄ β LMod) | ||
Theorem | mendassa 41355 | The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π = (Scalarβπ) β β’ ((π β LMod β§ π β CRing) β π΄ β AssAlg) | ||
Theorem | idomrootle 41356* | No element of an integral domain can have more than π π-th roots. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
β’ π΅ = (Baseβπ ) & β’ β = (.gβ(mulGrpβπ )) β β’ ((π β IDomn β§ π β π΅ β§ π β β) β (β―β{π¦ β π΅ β£ (π β π¦) = π}) β€ π) | ||
Theorem | idomodle 41357* | Limit on the number of π-th roots of unity in an integral domain. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ πΊ = ((mulGrpβπ ) βΎs (Unitβπ )) & β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) β β’ ((π β IDomn β§ π β β) β (β―β{π₯ β π΅ β£ (πβπ₯) β₯ π}) β€ π) | ||
Theorem | fiuneneq 41358 | 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.) |
β’ ((π΄ β π΅ β§ π΄ β Fin) β ((π΄ βͺ π΅) β π΄ β π΄ = π΅)) | ||
Theorem | idomsubgmo 41359* | 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.) |
β’ πΊ = ((mulGrpβπ ) βΎs (Unitβπ )) β β’ ((π β IDomn β§ π β β) β β*π¦ β (SubGrpβπΊ)(β―βπ¦) = π) | ||
Theorem | proot1mul 41360 | Any primitive π-th root of unity is a multiple of any other. (Contributed by Stefan O'Rear, 2-Nov-2015.) |
β’ πΊ = ((mulGrpβπ ) βΎs (Unitβπ )) & β’ π = (odβπΊ) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ (((π β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π β (πΎβ{π})) | ||
Theorem | proot1hash 41361 | If an integral domain has a primitive π-th root of unity, it has exactly (Οβπ) of them. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ πΊ = ((mulGrpβπ ) βΎs (Unitβπ )) & β’ π = (odβπΊ) β β’ ((π β IDomn β§ π β β β§ π β (β‘π β {π})) β (β―β(β‘π β {π})) = (Οβπ)) | ||
Theorem | proot1ex 41362 | The complex field has primitive π-th roots of unity for all π. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ πΊ = ((mulGrpββfld) βΎs (β β {0})) & β’ π = (odβπΊ) β β’ (π β β β (-1βπ(2 / π)) β (β‘π β {π})) | ||
Syntax | ccytp 41363 | Syntax for the sequence of cyclotomic polynomials. |
class CytP | ||
Definition | df-cytp 41364* | 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 = (π β β β¦ ((mulGrpβ(Poly1ββfld)) Ξ£g (π β (β‘(odβ((mulGrpββfld) βΎs (β β {0}))) β {π}) β¦ ((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ))))) | ||
Theorem | isdomn3 41365 | Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (mulGrpβπ ) β β’ (π β Domn β (π β Ring β§ (π΅ β { 0 }) β (SubMndβπ))) | ||
Theorem | mon1pid 41366 | Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π = (Poly1βπ ) & β’ 1 = (1rβπ) & β’ π = (Monic1pβπ ) & β’ π· = ( deg1 βπ ) β β’ (π β NzRing β ( 1 β π β§ (π·β 1 ) = 0)) | ||
Theorem | mon1psubm 41367 | Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π = (Poly1βπ ) & β’ π = (Monic1pβπ ) & β’ π = (mulGrpβπ) β β’ (π β NzRing β π β (SubMndβπ)) | ||
Theorem | deg1mhm 41368 | Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π· = ( deg1 βπ ) & β’ π΅ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π = ((mulGrpβπ) βΎs (π΅ β { 0 })) & β’ π = (βfld βΎs β0) β β’ (π β Domn β (π· βΎ (π΅ β { 0 })) β (π MndHom π)) | ||
Theorem | cytpfn 41369 | Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ CytP Fn β | ||
Theorem | cytpval 41370* | Substitutions for the Nth cyclotomic polynomial. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π = ((mulGrpββfld) βΎs (β β {0})) & β’ π = (odβπ) & β’ π = (Poly1ββfld) & β’ π = (var1ββfld) & β’ π = (mulGrpβπ) & β’ β = (-gβπ) & β’ π΄ = (algScβπ) β β’ (π β β β (CytPβπ) = (π Ξ£g (π β (β‘π β {π}) β¦ (π β (π΄βπ))))) | ||
Theorem | fgraphopab 41371* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (πΉ:π΄βΆπ΅ β πΉ = {β¨π, πβ© β£ ((π β π΄ β§ π β π΅) β§ (πΉβπ) = π)}) | ||
Theorem | fgraphxp 41372* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (πΉ:π΄βΆπ΅ β πΉ = {π₯ β (π΄ Γ π΅) β£ (πΉβ(1st βπ₯)) = (2nd βπ₯)}) | ||
Theorem | hausgraph 41373 | The graph of a continuous function into a Hausdorff space is closed. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β πΉ β (Clsdβ(π½ Γt πΎ))) | ||
Syntax | ctopsep 41374 | The class of separable topologies. |
class TopSep | ||
Syntax | ctoplnd 41375 | The class of LindelΓΆf topologies. |
class TopLnd | ||
Definition | df-topsep 41376* | A topology is separable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
β’ TopSep = {π β Top β£ βπ₯ β π« βͺ π(π₯ βΌ Ο β§ ((clsβπ)βπ₯) = βͺ π)} | ||
Definition | df-toplnd 41377* | A topology is LindelΓΆf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
β’ TopLnd = {π₯ β Top β£ βπ¦ β π« π₯(βͺ π₯ = βͺ π¦ β βπ§ β π« π₯(π§ βΌ Ο β§ βͺ π₯ = βͺ π§))} | ||
Theorem | r1sssucd 41378 | Deductive form of r1sssuc 9653. (Contributed by Noam Pasman, 19-Jan-2025.) |
β’ (π β π΄ β On) β β’ (π β (π 1βπ΄) β (π 1βsuc π΄)) | ||
Theorem | iocunico 41379 | Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ < π΅ β§ π΅ < πΆ)) β ((π΄(,]π΅) βͺ (π΅[,)πΆ)) = (π΄(,)πΆ)) | ||
Theorem | iocinico 41380 | The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ < π΅ β§ π΅ < πΆ)) β ((π΄(,]π΅) β© (π΅[,)πΆ)) = {π΅}) | ||
Theorem | iocmbl 41381 | An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.) |
β’ ((π΄ β β* β§ π΅ β β) β (π΄(,]π΅) β dom vol) | ||
Theorem | cnioobibld 41382* | A bounded, continuous function on an open bounded interval is integrable. The function must be bounded. For a counterexample, consider πΉ = (π₯ β (0(,)1) β¦ (1 / π₯)). See cniccibl 25127 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β βπ₯ β β βπ¦ β dom πΉ(absβ(πΉβπ¦)) β€ π₯) β β’ (π β πΉ β πΏ1) | ||
Theorem | arearect 41383 | The area of a rectangle whose sides are parallel to the coordinate axes in (β Γ β) is its width multiplied by its height. (Contributed by Jon Pennant, 19-Mar-2019.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β & β’ π΄ β€ π΅ & β’ πΆ β€ π· & β’ π = ((π΄[,]π΅) Γ (πΆ[,]π·)) β β’ (areaβπ) = ((π΅ β π΄) Β· (π· β πΆ)) | ||
Theorem | areaquad 41384* | The area of a quadrilateral with two sides which are parallel to the y-axis in (β Γ β) 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.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β & β’ πΈ β β & β’ πΉ β β & β’ π΄ < π΅ & β’ πΆ β€ πΈ & β’ π· β€ πΉ & β’ π = (πΆ + (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) & β’ π = (πΈ + (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) & β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄[,]π΅) β§ π¦ β (π[,]π))} β β’ (areaβπ) = ((((πΉ + πΈ) / 2) β ((π· + πΆ) / 2)) Β· (π΅ β π΄)) | ||
Theorem | omlimcl2 41385 | The product of a limit ordinal with any nonzero ordinal is a limit ordinal. (Contributed by RP, 8-Jan-2025.) |
β’ (((π΄ β On β§ (π΅ β πΆ β§ Lim π΅)) β§ β β π΄) β Lim (π΅ Β·o π΄)) | ||
Theorem | oawordex2 41386* | If πΆ is between π΄ (inclusive) and (π΄ +o π΅) (exclusive), there is an ordinal which equals πΆ when summed to π΄. This is a slightly different statement than oawordex 8472 or oawordeu 8470. (Contributed by RP, 7-Jan-2025.) |
β’ (((π΄ β On β§ π΅ β On) β§ (π΄ β πΆ β§ πΆ β (π΄ +o π΅))) β βπ₯ β π΅ (π΄ +o π₯) = πΆ) | ||
Theorem | nnawordexg 41387* | If an ordinal, π΅, is in a half-open interval between some π΄ and the next limit ordinal, π΅ is the sum of the π΄ and some natural number. This weakens the antecedent of nnawordex 8552. (Contributed by RP, 7-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π΅ β§ π΅ β (π΄ +o Ο)) β βπ₯ β Ο (π΄ +o π₯) = π΅) | ||
Theorem | succlg 41388 | Closure law for ordinal successor. (Contributed by RP, 8-Jan-2025.) |
β’ ((π΄ β π΅ β§ (π΅ = β β¨ (π΅ = (Ο Β·o πΆ) β§ πΆ β (On β 1o)))) β suc π΄ β π΅) | ||
Theorem | dflim5 41389* | A limit ordinal is either the proper class of ordinals or some nonzero product with omega. (Contributed by RP, 8-Jan-2025.) |
β’ (Lim π΄ β (π΄ = On β¨ βπ₯ β (On β 1o)π΄ = (Ο Β·o π₯))) | ||
Theorem | oacl2g 41390 | Closure law for ordinal addition. Here we show that ordinal addition is closed within the empty set or any ordinal power of omega. (Contributed by RP, 5-Jan-2025.) |
β’ (((π΄ β πΆ β§ π΅ β πΆ) β§ (πΆ = β β¨ (πΆ = (Ο βo π·) β§ π· β On))) β (π΄ +o π΅) β πΆ) | ||
Theorem | omabs2 41391 | Ordinal multiplication by a larger ordinal is absorbed when the larger ordinal is either 2 or Ο raised to some power of Ο. (Contributed by RP, 12-Jan-2025.) |
β’ (((π΄ β π΅ β§ β β π΄) β§ (π΅ = β β¨ π΅ = 2o β¨ (π΅ = (Ο βo (Ο βo πΆ)) β§ πΆ β On))) β (π΄ Β·o π΅) = π΅) | ||
Theorem | omcl2 41392 | Closure law for ordinal multiplication. (Contributed by RP, 12-Jan-2025.) |
β’ (((π΄ β πΆ β§ π΅ β πΆ) β§ (πΆ = β β¨ (πΆ = (Ο βo (Ο βo π·)) β§ π· β On))) β (π΄ Β·o π΅) β πΆ) | ||
Theorem | omcl3g 41393 | Closure law for ordinal multiplication. (Contributed by RP, 14-Jan-2025.) |
β’ (((π΄ β πΆ β§ π΅ β πΆ) β§ (πΆ β 3o β¨ (πΆ = (Ο βo (Ο βo π·)) β§ π· β On))) β (π΄ Β·o π΅) β πΆ) | ||
Theorem | ofoafg 41394* | Addition operator for functions from sets into ordinals results in a function from the intersection of sets into an ordinal. (Contributed by RP, 5-Jan-2025.) |
β’ (((π΄ β π β§ π΅ β π β§ πΆ = (π΄ β© π΅)) β§ (π· β On β§ πΈ β On β§ πΉ = βͺ π β π· (π +o πΈ))) β ( βf +o βΎ ((π· βm π΄) Γ (πΈ βm π΅))):((π· βm π΄) Γ (πΈ βm π΅))βΆ(πΉ βm πΆ)) | ||
Theorem | ofoaf 41395 | Addition operator for functions from sets into power of omega results in a function from the intersection of sets to that power of omega. (Contributed by RP, 5-Jan-2025.) |
β’ (((π΄ β π β§ π΅ β π β§ πΆ = (π΄ β© π΅)) β§ (π· β On β§ πΈ = (Ο βo π·))) β ( βf +o βΎ ((πΈ βm π΄) Γ (πΈ βm π΅))):((πΈ βm π΄) Γ (πΈ βm π΅))βΆ(πΈ βm πΆ)) | ||
Theorem | ofoafo 41396 | Addition operator for functions from a set into a power of omega is an onto binary operator. (Contributed by RP, 5-Jan-2025.) |
β’ ((π΄ β π β§ (π΅ β On β§ πΆ = (Ο βo π΅))) β ( βf +o βΎ ((πΆ βm π΄) Γ (πΆ βm π΄))):((πΆ βm π΄) Γ (πΆ βm π΄))βontoβ(πΆ βm π΄)) | ||
Theorem | ofoacl 41397 | Closure law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.) |
β’ (((π΄ β π β§ (π΅ β On β§ πΆ = (Ο βo π΅))) β§ (πΉ β (πΆ βm π΄) β§ πΊ β (πΆ βm π΄))) β (πΉ βf +o πΊ) β (πΆ βm π΄)) | ||
Theorem | ofoaid1 41398 | Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.) |
β’ (((π΄ β π β§ π΅ β On) β§ πΉ β (π΅ βm π΄)) β (πΉ βf +o (π΄ Γ {β })) = πΉ) | ||
Theorem | ofoaid2 41399 | Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.) |
β’ (((π΄ β π β§ π΅ β On) β§ πΉ β (π΅ βm π΄)) β ((π΄ Γ {β }) βf +o πΉ) = πΉ) | ||
Theorem | ofoaass 41400 | Component-wise addition of ordinal-yielding functions is associative. (Contributed by RP, 5-Jan-2025.) |
β’ (((π΄ β π β§ π΅ β On) β§ (πΉ β (π΅ βm π΄) β§ πΊ β (π΅ βm π΄) β§ π» β (π΅ βm π΄))) β ((πΉ βf +o πΊ) βf +o π») = (πΉ βf +o (πΊ βf +o π»))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |