Home | Metamath
Proof Explorer Theorem List (p. 195 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | psrlmod 19401 | The ring of power series is a left module. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer | ||
Theorem | psr1cl 19402* | The identity element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer | ||
Theorem | psrlidm 19403* | The identity element of the ring of power series is a left identity. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by AV, 8-Jul-2019.) |
mPwSer | ||
Theorem | psrridm 19404* | The identity element of the ring of power series is a right identity. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by AV, 8-Jul-2019.) |
mPwSer | ||
Theorem | psrass1 19405* | Associative identity for the ring of power series. (Contributed by Mario Carneiro, 5-Jan-2015.) |
mPwSer | ||
Theorem | psrdi 19406* | Distributive law for the ring of power series (left-distributivity). (Contributed by Mario Carneiro, 7-Jan-2015.) |
mPwSer | ||
Theorem | psrdir 19407* | Distributive law for the ring of power series (right-distributivity). (Contributed by Mario Carneiro, 7-Jan-2015.) |
mPwSer | ||
Theorem | psrass23l 19408* | Associative identity for the ring of power series. Part of psrass23 19410 which does not require the scalar ring to be commutative. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 14-Aug-2019.) |
mPwSer | ||
Theorem | psrcom 19409* | Commutative law for the ring of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) |
mPwSer | ||
Theorem | psrass23 19410* | Associative identities for the ring of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) (Proof shortened by AV, 25-Nov-2019.) |
mPwSer | ||
Theorem | psrring 19411 | The ring of power series is a ring. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer | ||
Theorem | psr1 19412* | The identity element of the ring of power series. (Contributed by Mario Carneiro, 8-Jan-2015.) |
mPwSer | ||
Theorem | psrcrng 19413 | The ring of power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
mPwSer | ||
Theorem | psrassa 19414 | The ring of power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer AssAlg | ||
Theorem | resspsrbas 19415 | A restricted power series algebra has the same base set. (Contributed by Mario Carneiro, 3-Jul-2015.) |
mPwSer ↾s mPwSer ↾s SubRing | ||
Theorem | resspsradd 19416 | A restricted power series algebra has the same addition operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
mPwSer ↾s mPwSer ↾s SubRing | ||
Theorem | resspsrmul 19417 | A restricted power series algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
mPwSer ↾s mPwSer ↾s SubRing | ||
Theorem | resspsrvsca 19418 | A restricted power series algebra has the same scalar multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
mPwSer ↾s mPwSer ↾s SubRing | ||
Theorem | subrgpsr 19419 | A subring of the base ring induces a subring of power series. (Contributed by Mario Carneiro, 3-Jul-2015.) |
mPwSer ↾s mPwSer SubRing SubRing | ||
Theorem | mvrfval 19420* | Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015.) |
mVar | ||
Theorem | mvrval 19421* | Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015.) |
mVar | ||
Theorem | mvrval2 19422* | Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015.) |
mVar | ||
Theorem | mvrid 19423* | The -th coefficient of the term is . (Contributed by Mario Carneiro, 7-Jan-2015.) |
mVar | ||
Theorem | mvrf 19424 | The power series variable function is a function from the index set to elements of the power series structure representing for each . (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer mVar | ||
Theorem | mvrf1 19425 | The power series variable function is injective if the base ring is nonzero. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer mVar | ||
Theorem | mvrcl2 19426 | A power series variable is an element of the base set. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer mVar | ||
Theorem | reldmmpl 19427 | The multivariate polynomial constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.) |
mPoly | ||
Theorem | mplval 19428* | Value of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) |
mPoly mPwSer finSupp ↾s | ||
Theorem | mplbas 19429* | Base set of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) |
mPoly mPwSer finSupp | ||
Theorem | mplelbas 19430 | Property of being a polynomial. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) |
mPoly mPwSer finSupp | ||
Theorem | mplval2 19431 | Self-referential expression for the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
mPoly mPwSer ↾s | ||
Theorem | mplbasss 19432 | The set of polynomials is a subset of the set of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
mPoly mPwSer | ||
Theorem | mplelf 19433* | A polynomial is defined as a function on the coefficients. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
mPoly | ||
Theorem | mplsubglem 19434* | If is an ideal of sets (a nonempty collection closed under subset and binary union) of the set of finite bags (the primary applications being and for some ), then the set of all power series whose coefficient functions are supported on an element of is a subgroup of the set of all power series. (Contributed by Mario Carneiro, 12-Jan-2015.) (Revised by AV, 16-Jul-2019.) |
mPwSer supp SubGrp | ||
Theorem | mpllsslem 19435* | If is an ideal of subsets (a nonempty collection closed under subset and binary union) of the set of finite bags (the primary applications being and for some ), then the set of all power series whose coefficient functions are supported on an element of is a linear subspace of the set of all power series. (Contributed by Mario Carneiro, 12-Jan-2015.) (Revised by AV, 16-Jul-2019.) |
mPwSer supp | ||
Theorem | mplsubglem2 19436* | Lemma for mplsubg 19437 and mpllss 19438. (Contributed by AV, 16-Jul-2019.) |
mPwSer mPoly supp | ||
Theorem | mplsubg 19437 | The set of polynomials is closed under addition, i.e. it is a subgroup of the set of power series. (Contributed by Mario Carneiro, 8-Jan-2015.) (Proof shortened by AV, 16-Jul-2019.) |
mPwSer mPoly SubGrp | ||
Theorem | mpllss 19438 | The set of polynomials is closed under scalar multiplication, i.e. it is a linear subspace of the set of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) (Proof shortened by AV, 16-Jul-2019.) |
mPwSer mPoly | ||
Theorem | mplsubrglem 19439* | Lemma for mplsubrg 19440. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by AV, 18-Jul-2019.) |
mPwSer mPoly supp supp | ||
Theorem | mplsubrg 19440 | The set of polynomials is closed under multiplication, i.e. it is a subring of the set of power series. (Contributed by Mario Carneiro, 9-Jan-2015.) |
mPwSer mPoly SubRing | ||
Theorem | mpl0 19441* | The zero polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.) |
mPoly | ||
Theorem | mpladd 19442 | The addition operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
mPoly | ||
Theorem | mplmul 19443* | The multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
mPoly g | ||
Theorem | mpl1 19444* | The identity element of the ring of polynomials. (Contributed by Mario Carneiro, 10-Jan-2015.) |
mPoly | ||
Theorem | mplsca 19445 | The scalar field of a multivariate polynomial structure. (Contributed by Mario Carneiro, 9-Jan-2015.) |
mPoly Scalar | ||
Theorem | mplvsca2 19446 | The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
mPoly mPwSer | ||
Theorem | mplvsca 19447* | The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
mPoly | ||
Theorem | mplvscaval 19448* | The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
mPoly | ||
Theorem | mvrcl 19449 | A power series variable is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.) |
mPoly mVar | ||
Theorem | mplgrp 19450 | The polynomial ring is a group. (Contributed by Mario Carneiro, 9-Jan-2015.) |
mPoly | ||
Theorem | mpllmod 19451 | The polynomial ring is a left module. (Contributed by Mario Carneiro, 9-Jan-2015.) |
mPoly | ||
Theorem | mplring 19452 | The polynomial ring is a ring. (Contributed by Mario Carneiro, 9-Jan-2015.) |
mPoly | ||
Theorem | mplcrng 19453 | The polynomial ring is a commutative ring. (Contributed by Mario Carneiro, 9-Jan-2015.) |
mPoly | ||
Theorem | mplassa 19454 | The polynomial ring is an associative algebra. (Contributed by Mario Carneiro, 9-Jan-2015.) |
mPoly AssAlg | ||
Theorem | ressmplbas2 19455 | The base set of a restricted polynomial algebra consists of power series in the subring which are also polynomials (in the parent ring). (Contributed by Mario Carneiro, 3-Jul-2015.) |
mPoly ↾s mPoly SubRing mPwSer | ||
Theorem | ressmplbas 19456 | A restricted polynomial algebra has the same base set. (Contributed by Mario Carneiro, 3-Jul-2015.) |
mPoly ↾s mPoly SubRing ↾s | ||
Theorem | ressmpladd 19457 | A restricted polynomial algebra has the same addition operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
mPoly ↾s mPoly SubRing ↾s | ||
Theorem | ressmplmul 19458 | A restricted polynomial algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
mPoly ↾s mPoly SubRing ↾s | ||
Theorem | ressmplvsca 19459 | A restricted power series algebra has the same scalar multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
mPoly ↾s mPoly SubRing ↾s | ||
Theorem | subrgmpl 19460 | A subring of the base ring induces a subring of polynomials. (Contributed by Mario Carneiro, 3-Jul-2015.) |
mPoly ↾s mPoly SubRing SubRing | ||
Theorem | subrgmvr 19461 | The variables in a subring polynomial algebra are the same as the original ring. (Contributed by Mario Carneiro, 4-Jul-2015.) |
mVar SubRing ↾s mVar | ||
Theorem | subrgmvrf 19462 | The variables in a polynomial algebra are contained in every subring algebra. (Contributed by Mario Carneiro, 4-Jul-2015.) |
mVar SubRing ↾s mPoly | ||
Theorem | mplmon 19463* | A monomial is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.) |
mPoly | ||
Theorem | mplmonmul 19464* | The product of two monomials adds the exponent vectors together. For example, the product of with is , where the exponent vectors and are added to give . (Contributed by Mario Carneiro, 9-Jan-2015.) |
mPoly | ||
Theorem | mplcoe1 19465* | Decompose a polynomial into a finite sum of monomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
mPoly g | ||
Theorem | mplcoe3 19466* | Decompose a monomial in one variable into a power of a variable. (Contributed by Mario Carneiro, 7-Jan-2015.) (Proof shortened by AV, 18-Jul-2019.) |
mPoly mulGrp .g mVar | ||
Theorem | mplcoe5lem 19467* | Lemma for mplcoe4 19503. (Contributed by AV, 7-Oct-2019.) |
mPoly mulGrp .g mVar Cntz | ||
Theorem | mplcoe5 19468* | Decompose a monomial into a finite product of powers of variables. Instead of assuming that is a commutative ring (as in mplcoe2 19469), it is sufficient that is a ring and all the variables of the multivariate polynomial commute. (Contributed by AV, 7-Oct-2019.) |
mPoly mulGrp .g mVar g | ||
Theorem | mplcoe2 19469* | Decompose a monomial into a finite product of powers of variables. (The assumption that is a commutative ring is not strictly necessary, because the submonoid of monomials is in the center of the multiplicative monoid of polynomials, but it simplifies the proof.) (Contributed by Mario Carneiro, 10-Jan-2015.) (Proof shortened by AV, 18-Oct-2019.) |
mPoly mulGrp .g mVar g | ||
Theorem | mplbas2 19470 | An alternative expression for the set of polynomials, as the smallest subalgebra of the set of power series that contains all the variable generators. (Contributed by Mario Carneiro, 10-Jan-2015.) |
mPoly mPwSer mVar AlgSpan | ||
Theorem | ltbval 19471* | Value of the well-order on finite bags. (Contributed by Mario Carneiro, 8-Feb-2015.) |
bag | ||
Theorem | ltbwe 19472* | The finite bag order is a well-order, given a well-order of the index set. (Contributed by Mario Carneiro, 2-Jun-2015.) |
bag | ||
Theorem | reldmopsr 19473 | Lemma for ordered power series. (Contributed by Stefan O'Rear, 2-Oct-2015.) |
ordPwSer | ||
Theorem | opsrval 19474* | The value of the "ordered power series" function. This is the same as mPwSer psrval 19362, but with the addition of a well-order on we can turn a strict order on into a strict order on the power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) |
mPwSer ordPwSer bag sSet | ||
Theorem | opsrle 19475* | An alternative expression for the set of polynomials, as the smallest subalgebra of the set of power series that contains all the variable generators. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
mPwSer ordPwSer bag | ||
Theorem | opsrval2 19476 | Self-referential expression for the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) |
mPwSer ordPwSer sSet | ||
Theorem | opsrbaslem 19477 | Get a component of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 9-Sep-2021.) |
mPwSer ordPwSer Slot ; | ||
Theorem | opsrbaslemOLD 19478 | Obsolete version of opsrbaslem 19477 as of 9-Sep-2021. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
mPwSer ordPwSer Slot | ||
Theorem | opsrbas 19479 | The base set of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
mPwSer ordPwSer | ||
Theorem | opsrplusg 19480 | The addition operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
mPwSer ordPwSer | ||
Theorem | opsrmulr 19481 | The multiplication operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
mPwSer ordPwSer | ||
Theorem | opsrvsca 19482 | The scalar product operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
mPwSer ordPwSer | ||
Theorem | opsrsca 19483 | The scalar ring of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
mPwSer ordPwSer Scalar | ||
Theorem | opsrtoslem1 19484* | Lemma for opsrtos 19486. (Contributed by Mario Carneiro, 8-Feb-2015.) |
ordPwSer Toset mPwSer bag | ||
Theorem | opsrtoslem2 19485* | Lemma for opsrtos 19486. (Contributed by Mario Carneiro, 8-Feb-2015.) |
ordPwSer Toset mPwSer bag Toset | ||
Theorem | opsrtos 19486 | The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 10-Jan-2015.) |
ordPwSer Toset Toset | ||
Theorem | opsrso 19487 | The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 10-Jan-2015.) |
ordPwSer Toset | ||
Theorem | opsrcrng 19488 | The ring of ordered power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
ordPwSer | ||
Theorem | opsrassa 19489 | The ring of ordered power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
ordPwSer AssAlg | ||
Theorem | mplrcl 19490 | Reverse closure for the polynomial index set. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
mPoly | ||
Theorem | mplelsfi 19491 | A polynomial treated as a coefficient function has finitely many nonzero terms. (Contributed by Stefan O'Rear, 22-Mar-2015.) (Revised by AV, 25-Jun-2019.) |
mPoly finSupp | ||
Theorem | mvrf2 19492 | The power series/polynomial variable function maps indices to polynomials. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
mPoly mVar | ||
Theorem | mplmon2 19493* | Express a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
mPoly | ||
Theorem | psrbag0 19494* | The empty bag is a bag. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
Theorem | psrbagsn 19495* | A singleton bag is a bag. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
Theorem | mplascl 19496* | Value of the scalar injection into the polynomial algebra. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
mPoly algSc | ||
Theorem | mplasclf 19497 | The scalar injection is a function into the polynomial algebra. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
mPoly algSc | ||
Theorem | subrgascl 19498 | The scalar injection function in a subring algebra is the same up to a restriction to the subring. (Contributed by Mario Carneiro, 4-Jul-2015.) |
mPoly algSc ↾s mPoly SubRing algSc | ||
Theorem | subrgasclcl 19499 | The scalars in a polynomial algebra are in the subring algebra iff the scalar value is in the subring. (Contributed by Mario Carneiro, 4-Jul-2015.) |
mPoly algSc ↾s mPoly SubRing | ||
Theorem | mplmon2cl 19500* | A scaled monomial is a polynomial. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
mPoly |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |