P. 195 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19401-19500   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cmpl 19401	Multivariate polynomials.
class mPoly
Syntax	cltb 19402	Ordering on terms of a multivariate polynomial.
class <bag
Syntax	copws 19403	Ordered set of power series.
class ordPwSer
Definition	df-psr 19404*	Define the algebra of power series over the index set 𝑖 and with coefficients from the ring 𝑟. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ mPwSer = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋{ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}))
Definition	df-mvr 19405*	Define the generating elements of the power series algebra. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ mVar = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟)))))
Definition	df-mpl 19406*	Define the subalgebra of the power series algebra generated by the variables; this is the polynomial algebra (the set of power series with finite degree). (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.)
⊢ mPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)}))
Definition	df-ltbag 19407*	Define a well-order on the set of all finite bags from the index set 𝑖 given a wellordering 𝑟 of 𝑖. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ <bag = (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∧ ∃𝑧 ∈ 𝑖 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))})
Definition	df-opsr 19408*	Define a total order on the set of all power series in 𝑠 from the index set 𝑖 given a wellordering 𝑟 of 𝑖 and a totally ordered base ring 𝑠. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ ordPwSer = (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ ⦋(𝑖 mPwSer 𝑠) / 𝑝⦌(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
Theorem	reldmpsr 19409	The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ Rel dom mPwSer
Theorem	psrval 19410*	Value of the multivariate power series structure. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑂 = (TopOpen‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐵 = (𝐾 ↑𝑚 𝐷))    &   ⊢ ✚ = ( ∘𝑓 + ↾ (𝐵 × 𝐵))    &   ⊢ × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))    &   ⊢ ∙ = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))    &   ⊢ (𝜑 → 𝐽 = (∏t‘(𝐷 × {𝑂})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝑆 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}))
Theorem	psrvalstr 19411	The multivariate power series structure is a function. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(TopSet‘ndx), 𝐽⟩}) Struct ⟨1, 9⟩
Theorem	psrbag 19412*	Elementhood in the set of finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝐹 ∈ 𝐷 ↔ (𝐹:𝐼⟶ℕ0 ∧ (◡𝐹 “ ℕ) ∈ Fin)))
Theorem	psrbagf 19413*	A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐼⟶ℕ0)
Theorem	snifpsrbag 19414*	A bag containing one element is a finite bag. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 8-Jul-2019.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 𝑁, 0)) ∈ 𝐷)
Theorem	fczpsrbag 19415*	The constant function equal to zero is a finite bag. (Contributed by AV, 8-Jul-2019.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷)
Theorem	psrbaglesupp 19416*	The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟 ≤ 𝐹)) → (◡𝐺 “ ℕ) ⊆ (◡𝐹 “ ℕ))
Theorem	psrbaglecl 19417*	The set of finite bags is downward-closed. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟 ≤ 𝐹)) → 𝐺 ∈ 𝐷)
Theorem	psrbagaddcl 19418*	The sum of two finite bags is a finite bag. (Contributed by Mario Carneiro, 9-Jan-2015.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) → (𝐹 ∘𝑓 + 𝐺) ∈ 𝐷)
Theorem	psrbagcon 19419*	The analogue of the statement "0 ≤ 𝐺 ≤ 𝐹 implies 0 ≤ 𝐹 − 𝐺 ≤ 𝐹 " for finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟 ≤ 𝐹)) → ((𝐹 ∘𝑓 − 𝐺) ∈ 𝐷 ∧ (𝐹 ∘𝑓 − 𝐺) ∘𝑟 ≤ 𝐹))
Theorem	psrbaglefi 19420*	There are finitely many bags dominated by a given bag. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 25-Jan-2015.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} ∈ Fin)
Theorem	psrbagconcl 19421*	The complement of a bag is a bag. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → (𝐹 ∘𝑓 − 𝑋) ∈ 𝑆)
Theorem	psrbagconf1o 19422*	Bag complementation is a bijection on the set of bags dominated by a given bag 𝐹. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → (𝑥 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑥)):𝑆–1-1-onto→𝑆)
Theorem	gsumbagdiaglem 19423*	Lemma for gsumbagdiag 19424. (Contributed by Mario Carneiro, 5-Jan-2015.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑋)})) → (𝑌 ∈ 𝑆 ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑌)}))
Theorem	gsumbagdiag 19424*	Two-dimensional commutation of a group sum over a "triangular" region. fsum0diag 14553 analogue for finite bags. (Contributed by Mario Carneiro, 5-Jan-2015.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑗)})) → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝑆, 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑗)} ↦ 𝑋)) = (𝐺 Σg (𝑘 ∈ 𝑆, 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑘)} ↦ 𝑋)))
Theorem	psrass1lem 19425*	A group sum commutation used by psrass1 19453. (Contributed by Mario Carneiro, 5-Jan-2015.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑗)})) → 𝑋 ∈ 𝐵)    &   ⊢ (𝑘 = (𝑛 ∘𝑓 − 𝑗) → 𝑋 = 𝑌)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑗)} ↦ 𝑋)))))
Theorem	psrbas 19426*	The base set of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 8-Jul-2019.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐵 = (𝐾 ↑𝑚 𝐷))
Theorem	psrelbas 19427*	An element of the set of power series is a function on the coefficients. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋:𝐷⟶𝐾)
Theorem	psrelbasfun 19428	An element of the set of power series is a function. (Contributed by AV, 17-Jul-2019.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝑋 ∈ 𝐵 → Fun 𝑋)
Theorem	psrplusg 19429	The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = (+g‘𝑆)    ⇒   ⊢ ✚ = ( ∘𝑓 + ↾ (𝐵 × 𝐵))
Theorem	psradd 19430	The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = (+g‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ✚ 𝑌) = (𝑋 ∘𝑓 + 𝑌))
Theorem	psraddcl 19431	Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	psrmulr 19432*	The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑆)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    ⇒   ⊢ ∙ = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))
Theorem	psrmulfval 19433*	The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑆)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∙ 𝐺) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝐹‘𝑥) · (𝐺‘(𝑘 ∘𝑓 − 𝑥)))))))
Theorem	psrmulval 19434*	The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑆)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((𝐹 ∙ 𝐺)‘𝑋) = (𝑅 Σg (𝑘 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑋} ↦ ((𝐹‘𝑘) · (𝐺‘(𝑋 ∘𝑓 − 𝑘))))))
Theorem	psrmulcllem 19435*	Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)
Theorem	psrmulcl 19436	Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)
Theorem	psrsca 19437	The scalar field of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝑅 = (Scalar‘𝑆))
Theorem	psrvscafval 19438*	The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ ∙ = ( ·𝑠 ‘𝑆)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    ⇒   ⊢ ∙ = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))
Theorem	psrvsca 19439*	The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ ∙ = ( ·𝑠 ‘𝑆)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∙ 𝐹) = ((𝐷 × {𝑋}) ∘𝑓 · 𝐹))
Theorem	psrvscaval 19440*	The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ ∙ = ( ·𝑠 ‘𝑆)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((𝑋 ∙ 𝐹)‘𝑌) = (𝑋 · (𝐹‘𝑌)))
Theorem	psrvscacl 19441	Closure of the power series scalar multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑆)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 𝐹) ∈ 𝐵)
Theorem	psr0cl 19442*	The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝐵)
Theorem	psr0lid 19443*	The zero element of the ring of power series is a left identity. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐷 × { 0 }) + 𝑋) = 𝑋)
Theorem	psrnegcl 19444*	The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁 ∘ 𝑋) ∈ 𝐵)
Theorem	psrlinv 19445*	The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ (𝜑 → ((𝑁 ∘ 𝑋) + 𝑋) = (𝐷 × { 0 }))
Theorem	psrgrp 19446	The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝑆 ∈ Grp)
Theorem	psr0 19447*	The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑂 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑆)    ⇒   ⊢ (𝜑 → 0 = (𝐷 × {𝑂}))
Theorem	psrneg 19448*	The negative function of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑀 = (invg‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) = (𝑁 ∘ 𝑋))
Theorem	psrlmod 19449	The ring of power series is a left module. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑆 ∈ LMod)
Theorem	psr1cl 19450*	The identity element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 ))    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝐵)
Theorem	psrlidm 19451*	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 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 ))    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑈 · 𝑋) = 𝑋)
Theorem	psrridm 19452*	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 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 ))    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑈) = 𝑋)
Theorem	psrass1 19453*	Associative identity for the ring of power series. (Contributed by Mario Carneiro, 5-Jan-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ × = (.r‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 × 𝑌) × 𝑍) = (𝑋 × (𝑌 × 𝑍)))
Theorem	psrdi 19454*	Distributive law for the ring of power series (left-distributivity). (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ × = (.r‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ (𝜑 → (𝑋 × (𝑌 + 𝑍)) = ((𝑋 × 𝑌) + (𝑋 × 𝑍)))
Theorem	psrdir 19455*	Distributive law for the ring of power series (right-distributivity). (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ × = (.r‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) × 𝑍) = ((𝑋 × 𝑍) + (𝑌 × 𝑍)))
Theorem	psrass23l 19456*	Associative identity for the ring of power series. Part of psrass23 19458 which does not require the scalar ring to be commutative. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 14-Aug-2019.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ × = (.r‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)))
Theorem	psrcom 19457*	Commutative law for the ring of power series. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ × = (.r‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → (𝑋 × 𝑌) = (𝑌 × 𝑋))
Theorem	psrass23 19458*	Associative identities for the ring of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) (Proof shortened by AV, 25-Nov-2019.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ × = (.r‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌))))
Theorem	psrring 19459	The ring of power series is a ring. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑆 ∈ Ring)
Theorem	psr1 19460*	The identity element of the ring of power series. (Contributed by Mario Carneiro, 8-Jan-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑈 = (1r‘𝑆)    ⇒   ⊢ (𝜑 → 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 )))
Theorem	psrcrng 19461	The ring of power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝑆 ∈ CRing)
Theorem	psrassa 19462	The ring of power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝑆 ∈ AssAlg)
Theorem	resspsrbas 19463	A restricted power series algebra has the same base set. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (𝐼 mPwSer 𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ 𝑃 = (𝑆 ↾s 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝑃))
Theorem	resspsradd 19464	A restricted power series algebra has the same addition operation. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (𝐼 mPwSer 𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ 𝑃 = (𝑆 ↾s 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑈)𝑌) = (𝑋(+g‘𝑃)𝑌))
Theorem	resspsrmul 19465	A restricted power series algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (𝐼 mPwSer 𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ 𝑃 = (𝑆 ↾s 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(.r‘𝑈)𝑌) = (𝑋(.r‘𝑃)𝑌))
Theorem	resspsrvsca 19466	A restricted power series algebra has the same scalar multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (𝐼 mPwSer 𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ 𝑃 = (𝑆 ↾s 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵)) → (𝑋( ·𝑠 ‘𝑈)𝑌) = (𝑋( ·𝑠 ‘𝑃)𝑌))
Theorem	subrgpsr 19467	A subring of the base ring induces a subring of power series. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (𝐼 mPwSer 𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝐵 ∈ (SubRing‘𝑆))
Theorem	mvrfval 19468*	Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑌)    ⇒   ⊢ (𝜑 → 𝑉 = (𝑥 ∈ 𝐼 ↦ (𝑓 ∈ 𝐷 ↦ if(𝑓 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0)), 1 , 0 ))))
Theorem	mvrval 19469*	Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑉‘𝑋) = (𝑓 ∈ 𝐷 ↦ if(𝑓 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)), 1 , 0 )))
Theorem	mvrval2 19470*	Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((𝑉‘𝑋)‘𝐹) = if(𝐹 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)), 1 , 0 ))
Theorem	mvrid 19471*	The 𝑋𝑖-th coefficient of the term 𝑋𝑖 is 1. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((𝑉‘𝑋)‘(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) = 1 )
Theorem	mvrf 19472	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 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑉:𝐼⟶𝐵)
Theorem	mvrf1 19473	The power series variable function is injective if the base ring is nonzero. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 1 ≠ 0 )    ⇒   ⊢ (𝜑 → 𝑉:𝐼–1-1→𝐵)
Theorem	mvrcl2 19474	A power series variable is an element of the base set. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑉‘𝑋) ∈ 𝐵)
Theorem	reldmmpl 19475	The multivariate polynomial constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ Rel dom mPoly
Theorem	mplval 19476*	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 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = {𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 }    ⇒   ⊢ 𝑃 = (𝑆 ↾s 𝑈)
Theorem	mplbas 19477*	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 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    ⇒   ⊢ 𝑈 = {𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 }
Theorem	mplelbas 19478	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 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    ⇒   ⊢ (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 finSupp 0 ))
Theorem	mplval2 19479	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 𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    ⇒   ⊢ 𝑃 = (𝑆 ↾s 𝑈)
Theorem	mplbasss 19480	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 𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ 𝑈 ⊆ 𝐵
Theorem	mplelf 19481*	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 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋:𝐷⟶𝐾)
Theorem	mplsubglem 19482*	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 𝐴 = Fin 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 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → ∅ ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∪ 𝑦) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑆))
Theorem	mpllsslem 19483*	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 𝐴 = Fin 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 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → ∅ ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∪ 𝑦) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑆))
Theorem	mplsubglem2 19484*	Lemma for mplsubg 19485 and mpllss 19486. (Contributed by AV, 16-Jul-2019.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝑈 = {𝑔 ∈ (Base‘𝑆) ∣ (𝑔 supp (0g‘𝑅)) ∈ Fin})
Theorem	mplsubg 19485	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 𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑆))
Theorem	mpllss 19486	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 𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑆))
Theorem	mplsubrglem 19487*	Lemma for mplsubrg 19488. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by AV, 18-Jul-2019.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = ( ∘𝑓 + “ ((𝑋 supp 0 ) × (𝑌 supp 0 )))    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌) ∈ 𝑈)
Theorem	mplsubrg 19488	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 𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑆))
Theorem	mpl0 19489*	The zero polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑂 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    ⇒   ⊢ (𝜑 → 0 = (𝐷 × {𝑂}))
Theorem	mpladd 19490	The addition operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = (+g‘𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ✚ 𝑌) = (𝑋 ∘𝑓 + 𝑌))
Theorem	mplmul 19491*	The multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∙ 𝐺) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝐹‘𝑥) · (𝐺‘(𝑘 ∘𝑓 − 𝑥)))))))
Theorem	mpl1 19492*	The identity element of the ring of polynomials. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑈 = (1r‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 )))
Theorem	mplsca 19493	The scalar field of a multivariate polynomial structure. (Contributed by Mario Carneiro, 9-Jan-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝑅 = (Scalar‘𝑃))
Theorem	mplvsca2 19494	The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    ⇒   ⊢ · = ( ·𝑠 ‘𝑆)
Theorem	mplvsca 19495*	The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ ∙ = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∙ 𝐹) = ((𝐷 × {𝑋}) ∘𝑓 · 𝐹))
Theorem	mplvscaval 19496*	The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ ∙ = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((𝑋 ∙ 𝐹)‘𝑌) = (𝑋 · (𝐹‘𝑌)))
Theorem	mvrcl 19497	A power series variable is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑉‘𝑋) ∈ 𝐵)
Theorem	mplgrp 19498	The polynomial ring is a group. (Contributed by Mario Carneiro, 9-Jan-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp) → 𝑃 ∈ Grp)
Theorem	mpllmod 19499	The polynomial ring is a left module. (Contributed by Mario Carneiro, 9-Jan-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ LMod)
Theorem	mplring 19500	The polynomial ring is a ring. (Contributed by Mario Carneiro, 9-Jan-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring)