![]() |
Metamath
Proof Explorer Theorem List (p. 221 of 481) | < 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: | ![]() (1-30604) |
![]() (30605-32127) |
![]() (32128-48014) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mhpmulcl 22001 | A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 25935 (which shows less-than-or-equal instead of equal). (Contributed by SN, 22-Jul-2024.) |
⊢ 𝐻 = (𝐼 mHomP 𝑅) & ⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ · = (.r‘𝑌) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑃 ∈ (𝐻‘𝑀)) & ⊢ (𝜑 → 𝑄 ∈ (𝐻‘𝑁)) ⇒ ⊢ (𝜑 → (𝑃 · 𝑄) ∈ (𝐻‘(𝑀 + 𝑁))) | ||
Theorem | mhppwdeg 22002 | Degree of a homogeneous polynomial raised to a power. General version of deg1pw 25976. (Contributed by SN, 26-Jul-2024.) |
⊢ 𝐻 = (𝐼 mHomP 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑇 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑀)) ⇒ ⊢ (𝜑 → (𝑁 ↑ 𝑋) ∈ (𝐻‘(𝑀 · 𝑁))) | ||
Theorem | mhpaddcl 22003 | Homogeneous polynomials are closed under addition. (Contributed by SN, 26-Aug-2023.) |
⊢ 𝐻 = (𝐼 mHomP 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ + = (+g‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) & ⊢ (𝜑 → 𝑌 ∈ (𝐻‘𝑁)) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐻‘𝑁)) | ||
Theorem | mhpinvcl 22004 | Homogeneous polynomials are closed under taking the opposite. (Contributed by SN, 12-Sep-2023.) |
⊢ 𝐻 = (𝐼 mHomP 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑀 = (invg‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) ⇒ ⊢ (𝜑 → (𝑀‘𝑋) ∈ (𝐻‘𝑁)) | ||
Theorem | mhpsubg 22005 | Homogeneous polynomials form a subgroup of the polynomials. (Contributed by SN, 25-Sep-2023.) |
⊢ 𝐻 = (𝐼 mHomP 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐻‘𝑁) ∈ (SubGrp‘𝑃)) | ||
Theorem | mhpvscacl 22006 | Homogeneous polynomials are closed under scalar multiplication. (Contributed by SN, 25-Sep-2023.) |
⊢ 𝐻 = (𝐼 mHomP 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐹 ∈ (𝐻‘𝑁)) ⇒ ⊢ (𝜑 → (𝑋 · 𝐹) ∈ (𝐻‘𝑁)) | ||
Theorem | mhplss 22007 | Homogeneous polynomials form a linear subspace of the polynomials. (Contributed by SN, 25-Sep-2023.) |
⊢ 𝐻 = (𝐼 mHomP 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐻‘𝑁) ∈ (LSubSp‘𝑃)) | ||
Definition | df-psd 22008* | Define the differentiation operation on multivariate polynomials. (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) is the partial derivative of the polynomial 𝐹 with respect to 𝑋. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ mPSDer = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))))))) | ||
Theorem | psdffval 22009* | Value of the power series differentiation operation. (Contributed by SN, 11-Apr-2025.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐼 mPSDer 𝑅) = (𝑥 ∈ 𝐼 ↦ (𝑓 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (((𝑘‘𝑥) + 1)(.g‘𝑅)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0))))))))) | ||
Theorem | psdfval 22010* | Give a map between power series and their partial derivatives with respect to a given variable 𝑋. (Contributed by SN, 11-Apr-2025.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → ((𝐼 mPSDer 𝑅)‘𝑋) = (𝑓 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))))) | ||
Theorem | psdval 22011* | Evaluate the partial derivative of a power series. (Contributed by SN, 11-Apr-2025.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) = (𝑘 ∈ 𝐷 ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) | ||
Theorem | psdcoef 22012* | Coefficient of a term of the derivative of a power series. (Contributed by SN, 12-Apr-2025.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ 𝐷) ⇒ ⊢ (𝜑 → ((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)‘𝐾) = (((𝐾‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝐾 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) | ||
Theorem | psdcl 22013 | The derivative of a power series is a power series. (Contributed by SN, 11-Apr-2025.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Mgm) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ 𝐵) | ||
Theorem | psdmplcl 22014 | The derivative of a polynomial is a polynomial. (Contributed by SN, 12-Apr-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ 𝐵) | ||
Theorem | psdadd 22015 | The derivative of a sum is the sum of the derivatives. (Contributed by SN, 12-Apr-2025.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐹 + 𝐺)) = ((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) + (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐺))) | ||
Theorem | psdvsca 22016 | The derivative of a scaled power series is the scaled derivative. (Contributed by SN, 12-Apr-2025.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) ⇒ ⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐶 · 𝐹)) = (𝐶 · (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹))) | ||
Definition | df-algind 22017* | Define the predicate "the set 𝑣 is algebraically independent in the algebra 𝑤". A collection of vectors is algebraically independent if no nontrivial polynomial with elements from the subset evaluates to zero. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ AlgInd = (𝑤 ∈ V, 𝑘 ∈ 𝒫 (Base‘𝑤) ↦ {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))}) | ||
According to Wikipedia ("Polynomial", 23-Dec-2019, https://en.wikipedia.org/wiki/Polynomial) "A polynomial in one indeterminate is called a univariate polynomial, a polynomial in more than one indeterminate is called a multivariate polynomial." In this sense univariate polynomials are defined as multivariate polynomials restricted to one indeterminate/polynomial variable in the following, see ply1bascl2 22047. According to the definition in Wikipedia "a polynomial can either be zero or can be written as the sum of a finite number of nonzero terms. Each term consists of the product of a number - called the coefficient of the term - and a finite number of indeterminates, raised to nonnegative integer powers.". By this, a term of a univariate polynomial (often also called "polynomial term") is the product of a coefficient (usually a member of the underlying ring) and the variable, raised to a nonnegative integer power. A (univariate) polynomial which has only one term is called (univariate) monomial - therefore, the notions "term" and "monomial" are often used synonymously, see also the definition in [Lang] p. 102. Sometimes, however, a monomial is defined as power product, "a product of powers of variables with nonnegative integer exponents", see Wikipedia ("Monomial", 23-Dec-2019, https://en.wikipedia.org/wiki/Mononomial 22047). In [Lang] p. 101, such terms are called "primitive monomials". To avoid any ambiguity, the notion "primitive monomial" is used for such power products ("x^i") in the following, whereas the synonym for "term" ("ai x^i") will be "scaled monomial". | ||
Syntax | cps1 22018 | Univariate power series. |
class PwSer1 | ||
Syntax | cv1 22019 | The base variable of a univariate power series. |
class var1 | ||
Syntax | cpl1 22020 | Univariate polynomials. |
class Poly1 | ||
Syntax | cco1 22021 | Coefficient function for a univariate polynomial. |
class coe1 | ||
Syntax | ctp1 22022 | Convert a univariate polynomial representation to multivariate. |
class toPoly1 | ||
Definition | df-psr1 22023 | Define the algebra of univariate power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ PwSer1 = (𝑟 ∈ V ↦ ((1o ordPwSer 𝑟)‘∅)) | ||
Definition | df-vr1 22024 | Define the base element of a univariate power series (the 𝑋 element of the set 𝑅[𝑋] of polynomials and also the 𝑋 in the set 𝑅[[𝑋]] of power series). (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ var1 = (𝑟 ∈ V ↦ ((1o mVar 𝑟)‘∅)) | ||
Definition | df-ply1 22025 | Define the algebra of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ Poly1 = (𝑟 ∈ V ↦ ((PwSer1‘𝑟) ↾s (Base‘(1o mPoly 𝑟)))) | ||
Definition | df-coe1 22026* | Define the coefficient function for a univariate polynomial. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ coe1 = (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1o × {𝑛})))) | ||
Definition | df-toply1 22027* | Define a function which maps a coefficient function for a univariate polynomial to the corresponding polynomial object. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ toPoly1 = (𝑓 ∈ V ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (𝑓‘(𝑛‘∅)))) | ||
Theorem | psr1baslem 22028 | The set of finite bags on 1o is just the set of all functions from 1o to ℕ0. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ (ℕ0 ↑m 1o) = {𝑓 ∈ (ℕ0 ↑m 1o) ∣ (◡𝑓 “ ℕ) ∈ Fin} | ||
Theorem | psr1val 22029 | Value of the ring of univariate power series. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑆 = (PwSer1‘𝑅) ⇒ ⊢ 𝑆 = ((1o ordPwSer 𝑅)‘∅) | ||
Theorem | psr1crng 22030 | The ring of univariate power series is a commutative ring. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑆 = (PwSer1‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝑆 ∈ CRing) | ||
Theorem | psr1assa 22031 | The ring of univariate power series is an associative algebra. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑆 = (PwSer1‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝑆 ∈ AssAlg) | ||
Theorem | psr1tos 22032 | The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 2-Jun-2015.) |
⊢ 𝑆 = (PwSer1‘𝑅) ⇒ ⊢ (𝑅 ∈ Toset → 𝑆 ∈ Toset) | ||
Theorem | psr1bas2 22033 | The base set of the ring of univariate power series. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (PwSer1‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑂 = (1o mPwSer 𝑅) ⇒ ⊢ 𝐵 = (Base‘𝑂) | ||
Theorem | psr1bas 22034 | The base set of the ring of univariate power series. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑆 = (PwSer1‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ 𝐵 = (𝐾 ↑m (ℕ0 ↑m 1o)) | ||
Theorem | vr1val 22035 | The value of the generator of the power series algebra (the 𝑋 in 𝑅[[𝑋]]). Since all univariate polynomial rings over a fixed base ring 𝑅 are isomorphic, we don't bother to pass this in as a parameter; internally we are actually using the empty set as this generator and 1o = {∅} is the index set (but for most purposes this choice should not be visible anyway). (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑋 = (var1‘𝑅) ⇒ ⊢ 𝑋 = ((1o mVar 𝑅)‘∅) | ||
Theorem | vr1cl2 22036 | The variable 𝑋 is a member of the power series algebra 𝑅[[𝑋]]. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑆 = (PwSer1‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵) | ||
Theorem | ply1val 22037 | The value of the set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (PwSer1‘𝑅) ⇒ ⊢ 𝑃 = (𝑆 ↾s (Base‘(1o mPoly 𝑅))) | ||
Theorem | ply1bas 22038 | The value of the base set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (PwSer1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) ⇒ ⊢ 𝑈 = (Base‘(1o mPoly 𝑅)) | ||
Theorem | ply1lss 22039 | Univariate polynomials form a linear subspace of the set of univariate power series. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (PwSer1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → 𝑈 ∈ (LSubSp‘𝑆)) | ||
Theorem | ply1subrg 22040 | Univariate polynomials form a subring of the set of univariate power series. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (PwSer1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → 𝑈 ∈ (SubRing‘𝑆)) | ||
Theorem | ply1crng 22041 | The ring of univariate polynomials is a commutative ring. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) | ||
Theorem | ply1assa 22042 | The ring of univariate polynomials is an associative algebra. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝑃 ∈ AssAlg) | ||
Theorem | psr1bascl 22043 | A univariate power series is a multivariate power series on one index. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝑃 = (PwSer1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ (Base‘(1o mPwSer 𝑅))) | ||
Theorem | psr1basf 22044 | Univariate power series base set elements are functions. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝑃 = (PwSer1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐹:(ℕ0 ↑m 1o)⟶𝐾) | ||
Theorem | ply1basf 22045 | Univariate polynomial base set elements are functions. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐹:(ℕ0 ↑m 1o)⟶𝐾) | ||
Theorem | ply1bascl 22046 | A univariate polynomial is a univariate power series. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ (Base‘(PwSer1‘𝑅))) | ||
Theorem | ply1bascl2 22047 | A univariate polynomial is a multivariate polynomial on one index. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ (Base‘(1o mPoly 𝑅))) | ||
Theorem | coe1fval 22048* | Value of the univariate polynomial coefficient function. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ (𝐹 ∈ 𝑉 → 𝐴 = (𝑛 ∈ ℕ0 ↦ (𝐹‘(1o × {𝑛})))) | ||
Theorem | coe1fv 22049 | Value of an evaluated coefficient in a polynomial coefficient vector. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝐴‘𝑁) = (𝐹‘(1o × {𝑁}))) | ||
Theorem | fvcoe1 22050 | Value of a multivariate coefficient in terms of the coefficient vector. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ (ℕ0 ↑m 1o)) → (𝐹‘𝑋) = (𝐴‘(𝑋‘∅))) | ||
Theorem | coe1fval3 22051* | Univariate power series coefficient vectors expressed as a function composition. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (PwSer1‘𝑅) & ⊢ 𝐺 = (𝑦 ∈ ℕ0 ↦ (1o × {𝑦})) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐴 = (𝐹 ∘ 𝐺)) | ||
Theorem | coe1f2 22052 | Functionality of univariate power series coefficient vectors. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (PwSer1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐴:ℕ0⟶𝐾) | ||
Theorem | coe1fval2 22053* | Univariate polynomial coefficient vectors expressed as a function composition. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (𝑦 ∈ ℕ0 ↦ (1o × {𝑦})) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐴 = (𝐹 ∘ 𝐺)) | ||
Theorem | coe1f 22054 | Functionality of univariate polynomial coefficient vectors. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐴:ℕ0⟶𝐾) | ||
Theorem | coe1fvalcl 22055 | A coefficient of a univariate polynomial over a class/ring is an element of this class/ring. (Contributed by AV, 9-Oct-2019.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0) → (𝐴‘𝑁) ∈ 𝐾) | ||
Theorem | coe1sfi 22056 | Finite support of univariate polynomial coefficient vectors. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 19-Jul-2019.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐴 finSupp 0 ) | ||
Theorem | coe1fsupp 22057* | The coefficient vector of a univariate polynomial is a finitely supported mapping from the nonnegative integers to the elements of the coefficient class/ring for the polynomial. (Contributed by AV, 3-Oct-2019.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐴 ∈ {𝑔 ∈ (𝐾 ↑m ℕ0) ∣ 𝑔 finSupp 0 }) | ||
Theorem | mptcoe1fsupp 22058* | A mapping involving coefficients of polynomials is finitely supported. (Contributed by AV, 12-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((coe1‘𝑀)‘𝑘)) finSupp 0 ) | ||
Theorem | coe1ae0 22059* | The coefficient vector of a univariate polynomial is 0 almost everywhere. (Contributed by AV, 19-Oct-2019.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐵 → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝐴‘𝑛) = 0 )) | ||
Theorem | vr1cl 22060 | The generator of a univariate polynomial algebra is contained in the base set. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵) | ||
Theorem | opsr0 22061 | Zero in the ordered power series ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → (0g‘𝑆) = (0g‘𝑂)) | ||
Theorem | opsr1 22062 | One in the ordered power series ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → (1r‘𝑆) = (1r‘𝑂)) | ||
Theorem | psr1plusg 22063 | Value of addition in a univariate power series ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑌 = (PwSer1‘𝑅) & ⊢ 𝑆 = (1o mPwSer 𝑅) & ⊢ + = (+g‘𝑌) ⇒ ⊢ + = (+g‘𝑆) | ||
Theorem | psr1vsca 22064 | Value of scalar multiplication in a univariate power series ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑌 = (PwSer1‘𝑅) & ⊢ 𝑆 = (1o mPwSer 𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) ⇒ ⊢ · = ( ·𝑠 ‘𝑆) | ||
Theorem | psr1mulr 22065 | Value of multiplication in a univariate power series ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑌 = (PwSer1‘𝑅) & ⊢ 𝑆 = (1o mPwSer 𝑅) & ⊢ · = (.r‘𝑌) ⇒ ⊢ · = (.r‘𝑆) | ||
Theorem | ply1plusg 22066 | Value of addition in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝑆 = (1o mPoly 𝑅) & ⊢ + = (+g‘𝑌) ⇒ ⊢ + = (+g‘𝑆) | ||
Theorem | ply1vsca 22067 | Value of scalar multiplication in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝑆 = (1o mPoly 𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) ⇒ ⊢ · = ( ·𝑠 ‘𝑆) | ||
Theorem | ply1mulr 22068 | Value of multiplication in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝑆 = (1o mPoly 𝑅) & ⊢ · = (.r‘𝑌) ⇒ ⊢ · = (.r‘𝑆) | ||
Theorem | ply1ass23l 22069 | Associative identity with scalar and ring multiplication for the polynomial ring. (Contributed by AV, 14-Aug-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌))) | ||
Theorem | ressply1bas2 22070 | 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.) |
⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑊 = (PwSer1‘𝐻) & ⊢ 𝐶 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 ∩ 𝐾)) | ||
Theorem | ressply1bas 22071 | A restricted polynomial algebra has the same base set. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑃 = (𝑆 ↾s 𝐵) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝑃)) | ||
Theorem | ressply1add 22072 | A restricted polynomial algebra has the same addition operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑃 = (𝑆 ↾s 𝐵) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑈)𝑌) = (𝑋(+g‘𝑃)𝑌)) | ||
Theorem | ressply1mul 22073 | A restricted polynomial algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑃 = (𝑆 ↾s 𝐵) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(.r‘𝑈)𝑌) = (𝑋(.r‘𝑃)𝑌)) | ||
Theorem | ressply1vsca 22074 | A restricted power series algebra has the same scalar multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑃 = (𝑆 ↾s 𝐵) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵)) → (𝑋( ·𝑠 ‘𝑈)𝑌) = (𝑋( ·𝑠 ‘𝑃)𝑌)) | ||
Theorem | subrgply1 22075 | A subring of the base ring induces a subring of polynomials. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) ⇒ ⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝐵 ∈ (SubRing‘𝑆)) | ||
Theorem | gsumply1subr 22076 | Evaluate a group sum in a polynomial ring over a subring. (Contributed by AV, 22-Sep-2019.) (Proof shortened by AV, 31-Jan-2020.) |
⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝑆 Σg 𝐹) = (𝑈 Σg 𝐹)) | ||
Theorem | psrbaspropd 22077 | Property deduction for power series base set. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ (𝜑 → (Base‘𝑅) = (Base‘𝑆)) ⇒ ⊢ (𝜑 → (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑆))) | ||
Theorem | psrplusgpropd 22078* | Property deduction for power series addition. (Contributed by Stefan O'Rear, 27-Mar-2015.) (Revised by Mario Carneiro, 3-Oct-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → (+g‘(𝐼 mPwSer 𝑅)) = (+g‘(𝐼 mPwSer 𝑆))) | ||
Theorem | mplbaspropd 22079* | Property deduction for polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 19-Jul-2019.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → (Base‘(𝐼 mPoly 𝑅)) = (Base‘(𝐼 mPoly 𝑆))) | ||
Theorem | psropprmul 22080 | Reversing multiplication in a ring reverses multiplication in the power series ring. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ 𝑌 = (𝐼 mPwSer 𝑅) & ⊢ 𝑆 = (oppr‘𝑅) & ⊢ 𝑍 = (𝐼 mPwSer 𝑆) & ⊢ · = (.r‘𝑌) & ⊢ ∙ = (.r‘𝑍) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 ∙ 𝐺) = (𝐺 · 𝐹)) | ||
Theorem | ply1opprmul 22081 | Reversing multiplication in a ring reverses multiplication in the univariate polynomial ring. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝑆 = (oppr‘𝑅) & ⊢ 𝑍 = (Poly1‘𝑆) & ⊢ · = (.r‘𝑌) & ⊢ ∙ = (.r‘𝑍) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 ∙ 𝐺) = (𝐺 · 𝐹)) | ||
Theorem | 00ply1bas 22082 | Lemma for ply1basfvi 22083 and deg1fvi 25941. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ ∅ = (Base‘(Poly1‘∅)) | ||
Theorem | ply1basfvi 22083 | Protection compatibility of the univariate polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ (Base‘(Poly1‘𝑅)) = (Base‘(Poly1‘( I ‘𝑅))) | ||
Theorem | ply1plusgfvi 22084 | Protection compatibility of the univariate polynomial addition. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ (+g‘(Poly1‘𝑅)) = (+g‘(Poly1‘( I ‘𝑅))) | ||
Theorem | ply1baspropd 22085* | Property deduction for univariate polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → (Base‘(Poly1‘𝑅)) = (Base‘(Poly1‘𝑆))) | ||
Theorem | ply1plusgpropd 22086* | Property deduction for univariate polynomial addition. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → (+g‘(Poly1‘𝑅)) = (+g‘(Poly1‘𝑆))) | ||
Theorem | opsrring 22087 | Ordered power series form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → 𝑂 ∈ Ring) | ||
Theorem | opsrlmod 22088 | Ordered power series form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → 𝑂 ∈ LMod) | ||
Theorem | psr1ring 22089 | Univariate power series form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝑆 = (PwSer1‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑆 ∈ Ring) | ||
Theorem | ply1ring 22090 | Univariate polynomials form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) | ||
Theorem | psr1lmod 22091 | Univariate power series form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑃 = (PwSer1‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) | ||
Theorem | psr1sca 22092 | Scalars of a univariate power series ring. (Contributed by Stefan O'Rear, 4-Jul-2015.) |
⊢ 𝑃 = (PwSer1‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘𝑃)) | ||
Theorem | psr1sca2 22093 | Scalars of a univariate power series ring. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑃 = (PwSer1‘𝑅) ⇒ ⊢ ( I ‘𝑅) = (Scalar‘𝑃) | ||
Theorem | ply1lmod 22094 | Univariate polynomials form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) | ||
Theorem | ply1sca 22095 | Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘𝑃)) | ||
Theorem | ply1sca2 22096 | Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ ( I ‘𝑅) = (Scalar‘𝑃) | ||
Theorem | ply1mpl0 22097 | The univariate polynomial ring has the same zero as the corresponding multivariate polynomial ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝑀 = (1o mPoly 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) ⇒ ⊢ 0 = (0g‘𝑀) | ||
Theorem | ply10s0 22098 | Zero times a univariate polynomial is the zero polynomial (lmod0vs 20737 analog.) (Contributed by AV, 2-Dec-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ ∗ = ( ·𝑠 ‘𝑃) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ( 0 ∗ 𝑀) = (0g‘𝑃)) | ||
Theorem | ply1mpl1 22099 | The univariate polynomial ring has the same one as the corresponding multivariate polynomial ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝑀 = (1o mPoly 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 1 = (1r‘𝑃) ⇒ ⊢ 1 = (1r‘𝑀) | ||
Theorem | ply1ascl 22100 | The univariate polynomial ring inherits the multivariate ring's scalar function. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by Fan Zheng, 26-Jun-2016.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ 𝐴 = (algSc‘(1o mPoly 𝑅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |