P. 220 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21901-22000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mhpfval 21901*	Value of the "homogeneous polynomial" function. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ 𝐵 ∣ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑛}}))
Theorem	mhpval 21902*	Value of the "homogeneous polynomial" function. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐻‘𝑁) = {𝑓 ∈ 𝐵 ∣ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}})
Theorem	ismhp 21903*	Property of being a homogeneous polynomial. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐻‘𝑁) ↔ (𝑋 ∈ 𝐵 ∧ (𝑋 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁})))
Theorem	ismhp2 21904*	Deduce a homogeneous polynomial from its properties. (Contributed by SN, 25-May-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁})    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))
Theorem	ismhp3 21905*	A polynomial is homogeneous iff the degree of every nonzero term is the same. (Contributed by SN, 22-Jul-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐻‘𝑁) ↔ ∀𝑑 ∈ 𝐷 ((𝑋‘𝑑) ≠ 0 → ((ℂfld ↾s ℕ0) Σg 𝑑) = 𝑁)))
Theorem	mhpmpl 21906	A homogeneous polynomial is a polynomial. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	mhpdeg 21907*	All nonzero terms of a homogeneous polynomial have degree 𝑁. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑋 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁})
Theorem	mhp0cl 21908*	The zero polynomial is homogeneous. Under df-mhp 21895, it has any (nonnegative integer) degree which loosely corresponds to the value "undefined". The values -∞ and 0 are also used in Metamath (by df-mdeg 25805 and df-dgr 25940 respectively) and the literature: https://math.stackexchange.com/a/1796314/593843 25940. (Contributed by SN, 12-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐷 × { 0 }) ∈ (𝐻‘𝑁))
Theorem	mhpsclcl 21909	A scalar (or constant) polynomial has degree 0. Compare deg1scl 25866. In other contexts, there may be an exception for the zero polynomial, but under df-mhp 21895 the zero polynomial can be any degree (see mhp0cl 21908) so there is no exception. (Contributed by SN, 25-May-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝐴‘𝐶) ∈ (𝐻‘0))
Theorem	mhpvarcl 21910	A power series variable is a polynomial of degree 1. (Contributed by SN, 25-May-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑉‘𝑋) ∈ (𝐻‘1))
Theorem	mhpmulcl 21911	A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 25832 (which shows less-than-or-equal instead of equal). (Contributed by SN, 22-Jul-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑌 = (𝐼 mPoly 𝑅)    &   ⊢ · = (.r‘𝑌)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑃 ∈ (𝐻‘𝑀))    &   ⊢ (𝜑 → 𝑄 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑃 · 𝑄) ∈ (𝐻‘(𝑀 + 𝑁)))
Theorem	mhppwdeg 21912	Degree of a homogeneous polynomial raised to a power. General version of deg1pw 25873. (Contributed by SN, 26-Jul-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑀))    ⇒   ⊢ (𝜑 → (𝑁 ↑ 𝑋) ∈ (𝐻‘(𝑀 · 𝑁)))
Theorem	mhpaddcl 21913	Homogeneous polynomials are closed under addition. (Contributed by SN, 26-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ + = (+g‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐻‘𝑁))
Theorem	mhpinvcl 21914	Homogeneous polynomials are closed under taking the opposite. (Contributed by SN, 12-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑀 = (invg‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) ∈ (𝐻‘𝑁))
Theorem	mhpsubg 21915	Homogeneous polynomials form a subgroup of the polynomials. (Contributed by SN, 25-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐻‘𝑁) ∈ (SubGrp‘𝑃))
Theorem	mhpvscacl 21916	Homogeneous polynomials are closed under scalar multiplication. (Contributed by SN, 25-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑋 · 𝐹) ∈ (𝐻‘𝑁))
Theorem	mhplss 21917	Homogeneous polynomials form a linear subspace of the polynomials. (Contributed by SN, 25-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐻‘𝑁) ∈ (LSubSp‘𝑃))
11.3.4  Univariate polynomials 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 21947. 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 21947). 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 21918	Univariate power series.
class PwSer1
Syntax	cv1 21919	The base variable of a univariate power series.
class var1
Syntax	cpl1 21920	Univariate polynomials.
class Poly1
Syntax	cco1 21921	Coefficient function for a univariate polynomial.
class coe1
Syntax	ctp1 21922	Convert a univariate polynomial representation to multivariate.
class toPoly1
Definition	df-psr1 21923	Define the algebra of univariate power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ PwSer1 = (𝑟 ∈ V ↦ ((1o ordPwSer 𝑟)‘∅))
Definition	df-vr1 21924	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 21925	Define the algebra of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ Poly1 = (𝑟 ∈ V ↦ ((PwSer1‘𝑟) ↾s (Base‘(1o mPoly 𝑟))))
Definition	df-coe1 21926*	Define the coefficient function for a univariate polynomial. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ coe1 = (𝑓 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (𝑓‘(1o × {𝑛}))))
Definition	df-toply1 21927*	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 21928	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 21929	Value of the ring of univariate power series. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ 𝑆 = ((1o ordPwSer 𝑅)‘∅)
Theorem	psr1crng 21930	The ring of univariate power series is a commutative ring. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑆 ∈ CRing)
Theorem	psr1assa 21931	The ring of univariate power series is an associative algebra. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑆 ∈ AssAlg)
Theorem	psr1tos 21932	The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 2-Jun-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ (𝑅 ∈ Toset → 𝑆 ∈ Toset)
Theorem	psr1bas2 21933	The base set of the ring of univariate power series. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑂 = (1o mPwSer 𝑅)    ⇒   ⊢ 𝐵 = (Base‘𝑂)
Theorem	psr1bas 21934	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 21935	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 21936	The variable 𝑋 is a member of the power series algebra 𝑅[[𝑋]]. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑆 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵)
Theorem	ply1val 21937	The value of the set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ 𝑃 = (𝑆 ↾s (Base‘(1o mPoly 𝑅)))
Theorem	ply1bas 21938	The value of the base set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (PwSer1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    ⇒   ⊢ 𝑈 = (Base‘(1o mPoly 𝑅))
Theorem	ply1lss 21939	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 21940	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 21941	The ring of univariate polynomials is a commutative ring. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing)
Theorem	ply1assa 21942	The ring of univariate polynomials is an associative algebra. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑃 ∈ AssAlg)
Theorem	psr1bascl 21943	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 21944	Univariate power series base set elements are functions. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝑃 = (PwSer1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:(ℕ0 ↑m 1o)⟶𝐾)
Theorem	ply1basf 21945	Univariate polynomial base set elements are functions. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:(ℕ0 ↑m 1o)⟶𝐾)
Theorem	ply1bascl 21946	A univariate polynomial is a univariate power series. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ (Base‘(PwSer1‘𝑅)))
Theorem	ply1bascl2 21947	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 21948*	Value of the univariate polynomial coefficient function. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    ⇒   ⊢ (𝐹 ∈ 𝑉 → 𝐴 = (𝑛 ∈ ℕ0 ↦ (𝐹‘(1o × {𝑛}))))
Theorem	coe1fv 21949	Value of an evaluated coefficient in a polynomial coefficient vector. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    ⇒   ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝐴‘𝑁) = (𝐹‘(1o × {𝑁})))
Theorem	fvcoe1 21950	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 21951*	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 21952	Functionality of univariate power series coefficient vectors. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (PwSer1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐴:ℕ0⟶𝐾)
Theorem	coe1fval2 21953*	Univariate polynomial coefficient vectors expressed as a function composition. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (𝑦 ∈ ℕ0 ↦ (1o × {𝑦}))    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐴 = (𝐹 ∘ 𝐺))
Theorem	coe1f 21954	Functionality of univariate polynomial coefficient vectors. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐴 = (coe1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐴:ℕ0⟶𝐾)
Theorem	coe1fvalcl 21955	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 21956	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 21957*	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 21958*	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 21959*	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 21960	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 21961	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 21962	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 21963	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 21964	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 21965	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 21966	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 21967	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 21968	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 21969	Associative identity with scalar and ring multiplication for the polynomial ring. (Contributed by AV, 14-Aug-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ × = (.r‘𝑃)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)))
Theorem	ressply1bas2 21970	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 21971	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 21972	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 21973	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 21974	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 21975	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 21976	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 21977	Property deduction for power series base set. (Contributed by Stefan O'Rear, 27-Mar-2015.)
⊢ (𝜑 → (Base‘𝑅) = (Base‘𝑆))    ⇒   ⊢ (𝜑 → (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑆)))
Theorem	psrplusgpropd 21978*	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 21979*	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 21980	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 21981	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 21982	Lemma for ply1basfvi 21983 and deg1fvi 25838. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ ∅ = (Base‘(Poly1‘∅))
Theorem	ply1basfvi 21983	Protection compatibility of the univariate polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015.)
⊢ (Base‘(Poly1‘𝑅)) = (Base‘(Poly1‘( I ‘𝑅)))
Theorem	ply1plusgfvi 21984	Protection compatibility of the univariate polynomial addition. (Contributed by Stefan O'Rear, 27-Mar-2015.)
⊢ (+g‘(Poly1‘𝑅)) = (+g‘(Poly1‘( I ‘𝑅)))
Theorem	ply1baspropd 21985*	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 21986*	Property deduction for univariate polynomial addition. (Contributed by Stefan O'Rear, 27-Mar-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦))    ⇒   ⊢ (𝜑 → (+g‘(Poly1‘𝑅)) = (+g‘(Poly1‘𝑆)))
Theorem	opsrring 21987	Ordered power series form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → 𝑂 ∈ Ring)
Theorem	opsrlmod 21988	Ordered power series form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.)
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → 𝑂 ∈ LMod)
Theorem	psr1ring 21989	Univariate power series form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝑆 = (PwSer1‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑆 ∈ Ring)
Theorem	ply1ring 21990	Univariate polynomials form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
Theorem	psr1lmod 21991	Univariate power series form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.)
⊢ 𝑃 = (PwSer1‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
Theorem	psr1sca 21992	Scalars of a univariate power series ring. (Contributed by Stefan O'Rear, 4-Jul-2015.)
⊢ 𝑃 = (PwSer1‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘𝑃))
Theorem	psr1sca2 21993	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 21994	Univariate polynomials form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
Theorem	ply1sca 21995	Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘𝑃))
Theorem	ply1sca2 21996	Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ ( I ‘𝑅) = (Scalar‘𝑃)
Theorem	ply1mpl0 21997	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 21998	Zero times a univariate polynomial is the zero polynomial (lmod0vs 20649 analog.) (Contributed by AV, 2-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ ∗ = ( ·𝑠 ‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ( 0 ∗ 𝑀) = (0g‘𝑃))
Theorem	ply1mpl1 21999	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 22000	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 𝑅))