P. 221 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22001-22100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ressmpladd 22001	A restricted polynomial algebra has the same addition operation. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (𝐼 mPoly 𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝑃 = (𝑆 ↾s 𝐵)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑈)𝑌) = (𝑋(+g‘𝑃)𝑌))
Theorem	ressmplmul 22002	A restricted polynomial algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (𝐼 mPoly 𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝑃 = (𝑆 ↾s 𝐵)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(.r‘𝑈)𝑌) = (𝑋(.r‘𝑃)𝑌))
Theorem	ressmplvsca 22003	A restricted power series algebra has the same scalar multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (𝐼 mPoly 𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝑃 = (𝑆 ↾s 𝐵)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵)) → (𝑋( ·𝑠 ‘𝑈)𝑌) = (𝑋( ·𝑠 ‘𝑃)𝑌))
Theorem	subrgmpl 22004	A subring of the base ring induces a subring of polynomials. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ 𝑆 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (𝐼 mPoly 𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝐵 ∈ (SubRing‘𝑆))
Theorem	subrgmvr 22005	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 22006	The variables in a polynomial algebra are contained in every subring algebra. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅))    &   ⊢ 𝐻 = (𝑅 ↾s 𝑇)    &   ⊢ 𝑈 = (𝐼 mPoly 𝐻)    &   ⊢ 𝐵 = (Base‘𝑈)    ⇒   ⊢ (𝜑 → 𝑉:𝐼⟶𝐵)
Theorem	mplmon 22007*	A monomial is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )) ∈ 𝐵)
Theorem	mplmonmul 22008*	The product of two monomials adds the exponent vectors together. For example, the product of (𝑥↑2)(𝑦↑2) with (𝑦↑1)(𝑧↑3) is (𝑥↑2)(𝑦↑3)(𝑧↑3), where the exponent vectors ⟨2, 2, 0⟩ and ⟨0, 1, 3⟩ are added to give ⟨2, 3, 3⟩. (Contributed by Mario Carneiro, 9-Jan-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ · = (.r‘𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑋 ∘f + 𝑌), 1 , 0 )))
Theorem	mplcoe1 22009*	Decompose a polynomial into a finite sum of monomials. (Contributed by Mario Carneiro, 9-Jan-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = (𝑃 Σg (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
Theorem	mplcoe3 22010*	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 𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑘 ∈ 𝐼 ↦ if(𝑘 = 𝑋, 𝑁, 0)), 1 , 0 )) = (𝑁 ↑ (𝑉‘𝑋)))
Theorem	mplcoe5lem 22011*	Lemma for mplcoe4 22043. (Contributed by AV, 7-Oct-2019.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐼 ((𝑉‘𝑦)(+g‘𝐺)(𝑉‘𝑥)) = ((𝑉‘𝑥)(+g‘𝐺)(𝑉‘𝑦)))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → ran (𝑘 ∈ 𝑆 ↦ ((𝑌‘𝑘) ↑ (𝑉‘𝑘))) ⊆ ((Cntz‘𝐺)‘ran (𝑘 ∈ 𝑆 ↦ ((𝑌‘𝑘) ↑ (𝑉‘𝑘)))))
Theorem	mplcoe5 22012*	Decompose a monomial into a finite product of powers of variables. Instead of assuming that 𝑅 is a commutative ring (as in mplcoe2 22013), it is sufficient that 𝑅 is a ring and all the variables of the multivariate polynomial commute. (Contributed by AV, 7-Oct-2019.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐼 ((𝑉‘𝑦)(+g‘𝐺)(𝑉‘𝑥)) = ((𝑉‘𝑥)(+g‘𝐺)(𝑉‘𝑦)))    ⇒   ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 )) = (𝐺 Σg (𝑘 ∈ 𝐼 ↦ ((𝑌‘𝑘) ↑ (𝑉‘𝑘)))))
Theorem	mplcoe2 22013*	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 𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 )) = (𝐺 Σg (𝑘 ∈ 𝐼 ↦ ((𝑌‘𝑘) ↑ (𝑉‘𝑘)))))
Theorem	mplbas2 22014	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‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → (𝐴‘ran 𝑉) = (Base‘𝑃))
Theorem	ltbval 22015*	Value of the well-order on finite bags. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐶 = (𝑇 <bag 𝐼)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐶 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐷 ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))})
Theorem	ltbwe 22016*	The finite bag order is a well-order, given a well-order of the index set. (Contributed by Mario Carneiro, 2-Jun-2015.)
⊢ 𝐶 = (𝑇 <bag 𝐼)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑇 We 𝐼)    ⇒   ⊢ (𝜑 → 𝐶 We 𝐷)
Theorem	reldmopsr 22017	Lemma for ordered power series. (Contributed by Stefan O'Rear, 2-Oct-2015.)
⊢ Rel dom ordPwSer
Theorem	opsrval 22018*	The value of the "ordered power series" function. This is the same as mPwSer psrval 21889, 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 𝑅)‘𝑇)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ < = (lt‘𝑅)    &   ⊢ 𝐶 = (𝑇 <bag 𝐼)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ ≤ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → 𝑂 = (𝑆 sSet ⟨(le‘ndx), ≤ ⟩))
Theorem	opsrle 22019*	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 𝑅)‘𝑇)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ < = (lt‘𝑅)    &   ⊢ 𝐶 = (𝑇 <bag 𝐼)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ ≤ = (le‘𝑂)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))})
Theorem	opsrval2 22020	Self-referential expression for the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ ≤ = (le‘𝑂)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → 𝑂 = (𝑆 sSet ⟨(le‘ndx), ≤ ⟩))
Theorem	opsrbaslem 22021	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.) (Revised by AV, 1-Nov-2024.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (le‘ndx)    ⇒   ⊢ (𝜑 → (𝐸‘𝑆) = (𝐸‘𝑂))
Theorem	opsrbas 22022	The base set of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) (Revised by AV, 1-Nov-2024.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → (Base‘𝑆) = (Base‘𝑂))
Theorem	opsrplusg 22023	The addition operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) (Revised by AV, 1-Nov-2024.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → (+g‘𝑆) = (+g‘𝑂))
Theorem	opsrmulr 22024	The multiplication operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) (Revised by AV, 1-Nov-2024.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → (.r‘𝑆) = (.r‘𝑂))
Theorem	opsrvsca 22025	The scalar product operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) (Revised by AV, 1-Nov-2024.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → ( ·𝑠 ‘𝑆) = ( ·𝑠 ‘𝑂))
Theorem	opsrsca 22026	The scalar ring of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) (Revised by AV, 1-Nov-2024.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝑅 = (Scalar‘𝑂))
Theorem	opsrtoslem1 22027*	Lemma for opsrtos 22029. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Toset)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    &   ⊢ (𝜑 → 𝑇 We 𝐼)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ < = (lt‘𝑅)    &   ⊢ 𝐶 = (𝑇 <bag 𝐼)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜓 ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))))    &   ⊢ ≤ = (le‘𝑂)    ⇒   ⊢ (𝜑 → ≤ = (({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)))
Theorem	opsrtoslem2 22028*	Lemma for opsrtos 22029. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Toset)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    &   ⊢ (𝜑 → 𝑇 We 𝐼)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ < = (lt‘𝑅)    &   ⊢ 𝐶 = (𝑇 <bag 𝐼)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜓 ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))))    &   ⊢ ≤ = (le‘𝑂)    ⇒   ⊢ (𝜑 → 𝑂 ∈ Toset)
Theorem	opsrtos 22029	The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Toset)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    &   ⊢ (𝜑 → 𝑇 We 𝐼)    ⇒   ⊢ (𝜑 → 𝑂 ∈ Toset)
Theorem	opsrso 22030	The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Toset)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    &   ⊢ (𝜑 → 𝑇 We 𝐼)    &   ⊢ ≤ = (lt‘𝑂)    &   ⊢ 𝐵 = (Base‘𝑂)    ⇒   ⊢ (𝜑 → ≤ Or 𝐵)
Theorem	opsrcrng 22031	The ring of ordered power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → 𝑂 ∈ CRing)
Theorem	opsrassa 22032	The ring of ordered power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → 𝑂 ∈ AssAlg)
Theorem	mplmon2 22033*	Express a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝐾, 1 , 0 ))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝐾, 𝑋, 0 )))
Theorem	psrbag0 22034*	The empty bag is a bag. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝐼 × {0}) ∈ 𝐷)
Theorem	psrbagsn 22035*	A singleton bag is a bag. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝐾, 1, 0)) ∈ 𝐷)
Theorem	mplascl 22036*	Value of the scalar injection into the polynomial algebra. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴‘𝑋) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑋, 0 )))
Theorem	mplasclf 22037	The scalar injection is a function into the polynomial algebra. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝐴:𝐾⟶𝐵)
Theorem	subrgascl 22038	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 22039	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‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑈)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝐵 ↔ 𝑋 ∈ 𝑇))
Theorem	mplmon2cl 22040*	A scaled monomial is a polynomial. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝐾, 𝑋, 0 )) ∈ 𝐵)
Theorem	mplmon2mul 22041*	Product of scaled monomials. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 𝐹, 0 )) ∙ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 𝐺, 0 ))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑋 ∘f + 𝑌), (𝐹 · 𝐺), 0 )))
Theorem	mplind 22042*	Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. The commutativity condition is stronger than strictly needed. (Contributed by Stefan O'Rear, 11-Mar-2015.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝑌 = (𝐼 mPoly 𝑅)    &   ⊢ + = (+g‘𝑌)    &   ⊢ · = (.r‘𝑌)    &   ⊢ 𝐶 = (algSc‘𝑌)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 + 𝑦) ∈ 𝐻)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 · 𝑦) ∈ 𝐻)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐶‘𝑥) ∈ 𝐻)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) ∈ 𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐻)
Theorem	mplcoe4 22043*	Decompose a polynomial into a finite sum of scaled monomials. (Contributed by Stefan O'Rear, 8-Mar-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = (𝑃 Σg (𝑘 ∈ 𝐷 ↦ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, (𝑋‘𝑘), 0 )))))
11.3.2  Polynomial evaluation
Syntax	ces 22044	Evaluation of a multivariate polynomial in a subring.
class evalSub
Syntax	cevl 22045	Evaluation of a multivariate polynomial.
class eval
Definition	df-evls 22046*	Define the evaluation map for the polynomial algebra. The function ((𝐼 evalSub 𝑆)‘𝑅):𝑉⟶(𝑆 ↑m (𝑆 ↑m 𝐼)) makes sense when 𝐼 is an index set, 𝑆 is a ring, 𝑅 is a subring of 𝑆, and where 𝑉 is the set of polynomials in (𝐼 mPoly 𝑅). This function maps an element of the formal polynomial algebra (with coefficients in 𝑅) to a function from assignments 𝐼⟶𝑆 of the variables to elements of 𝑆 formed by evaluating the polynomial with the given assignments. (Contributed by Stefan O'Rear, 11-Mar-2015.)
⊢ evalSub = (𝑖 ∈ V, 𝑠 ∈ CRing ↦ ⦋(Base‘𝑠) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))))))
Definition	df-evl 22047*	A simplification of evalSub when the evaluation ring is the same as the coefficient ring. (Contributed by Stefan O'Rear, 19-Mar-2015.)
⊢ eval = (𝑖 ∈ V, 𝑟 ∈ V ↦ ((𝑖 evalSub 𝑟)‘(Base‘𝑟)))
Theorem	evlslem4 22048*	The support of a tensor product of ring element families is contained in the product of the supports. (Contributed by Stefan O'Rear, 8-Mar-2015.) (Revised by AV, 18-Jul-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑋 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)) supp 0 ) ⊆ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))
Theorem	psrbagev1 22049*	A bag of multipliers provides the conditions for a valid sum. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) (Revised by AV, 11-Apr-2024.) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ · = (.g‘𝑇)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ CMnd)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    ⇒   ⊢ (𝜑 → ((𝐵 ∘f · 𝐺):𝐼⟶𝐶 ∧ (𝐵 ∘f · 𝐺) finSupp 0 ))
Theorem	psrbagev2 22050*	Closure of a sum using a bag of multipliers. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 18-Jul-2019.) (Revised by AV, 11-Apr-2024.) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ · = (.g‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ CMnd)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    ⇒   ⊢ (𝜑 → (𝑇 Σg (𝐵 ∘f · 𝐺)) ∈ 𝐶)
Theorem	evlslem2 22051*	A linear function on the polynomial ring which is multiplicative on scaled monomials is generally multiplicative. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 11-Apr-2024.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐸 ∈ (𝑃 GrpHom 𝑆))    &   ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑗 ∈ 𝐷 ∧ 𝑖 ∈ 𝐷))) → (𝐸‘(𝑘 ∈ 𝐷 ↦ if(𝑘 = (𝑗 ∘f + 𝑖), ((𝑥‘𝑗)(.r‘𝑅)(𝑦‘𝑖)), 0 ))) = ((𝐸‘(𝑘 ∈ 𝐷 ↦ if(𝑘 = 𝑗, (𝑥‘𝑗), 0 ))) · (𝐸‘(𝑘 ∈ 𝐷 ↦ if(𝑘 = 𝑖, (𝑦‘𝑖), 0 )))))    ⇒   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(.r‘𝑃)𝑦)) = ((𝐸‘𝑥) · (𝐸‘𝑦)))
Theorem	evlslem3 22052*	Lemma for evlseu 22055. Polynomial evaluation of a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015.) (Revised by AV, 11-Apr-2024.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑇)    &   ⊢ · = (.r‘𝑆)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘f ↑ 𝐺))))
Theorem	evlslem6 22053*	Lemma for evlseu 22055. Finiteness and consistency of the top-level sum. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 26-Jul-2019.) (Revised by AV, 11-Apr-2024.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑇)    &   ⊢ · = (.r‘𝑆)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆)))
Theorem	evlslem1 22054*	Lemma for evlseu 22055, give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 26-Jul-2019.) (Revised by AV, 11-Apr-2024.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑇)    &   ⊢ · = (.r‘𝑆)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸 ∘ 𝐴) = 𝐹 ∧ (𝐸 ∘ 𝑉) = 𝐺))
Theorem	evlseu 22055*	For a given interpretation of the variables 𝐺 and of the scalars 𝐹, this extends to a homomorphic interpretation of the polynomial ring in exactly one way. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 11-Apr-2024.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    ⇒   ⊢ (𝜑 → ∃!𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺))
Theorem	reldmevls 22056	Well-behaved binary operation property of evalSub. (Contributed by Stefan O'Rear, 19-Mar-2015.)
⊢ Rel dom evalSub
Theorem	mpfrcl 22057	Reverse closure for the set of polynomial functions. (Contributed by Stefan O'Rear, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝑄 → (𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)))
Theorem	evlsval 22058*	Value of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 11-Mar-2015.) (Revised by AV, 18-Sep-2021.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑉 = (𝐼 mVar 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑇 = (𝑆 ↑s (𝐵 ↑m 𝐼))    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑m 𝐼) × {𝑥}))    &   ⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥)))    ⇒   ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))
Theorem	evlsval2 22059*	Characterizing properties of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 12-Mar-2015.) (Revised by AV, 18-Sep-2021.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑉 = (𝐼 mVar 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑇 = (𝑆 ↑s (𝐵 ↑m 𝐼))    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑m 𝐼) × {𝑥}))    &   ⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥)))    ⇒   ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → (𝑄 ∈ (𝑊 RingHom 𝑇) ∧ ((𝑄 ∘ 𝐴) = 𝑋 ∧ (𝑄 ∘ 𝑉) = 𝑌)))
Theorem	evlsrhm 22060	Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Stefan O'Rear, 12-Mar-2015.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑇 = (𝑆 ↑s (𝐵 ↑m 𝐼))    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ (𝑊 RingHom 𝑇))
Theorem	evlssca 22061	Polynomial evaluation maps scalars to constant functions. (Contributed by Stefan O'Rear, 13-Mar-2015.) (Proof shortened by AV, 18-Sep-2021.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    ⇒   ⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = ((𝐵 ↑m 𝐼) × {𝑋}))
Theorem	evlsvar 22062*	Polynomial evaluation maps variables to projections. (Contributed by Stefan O'Rear, 12-Mar-2015.) (Proof shortened by AV, 18-Sep-2021.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑉 = (𝐼 mVar 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑉‘𝑋)) = (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑋)))
Theorem	evlsgsumadd 22063*	Polynomial evaluation maps (additive) group sums to group sums. (Contributed by SN, 13-Feb-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑃 = (𝑆 ↑s (𝐾 ↑m 𝐼))    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ⊆ ℕ0)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝑃 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))))
Theorem	evlsgsummul 22064*	Polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by SN, 13-Feb-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ 1 = (1r‘𝑊)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑃 = (𝑆 ↑s (𝐾 ↑m 𝐼))    &   ⊢ 𝐻 = (mulGrp‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ⊆ ℕ0)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 1 )    ⇒   ⊢ (𝜑 → (𝑄‘(𝐺 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝐻 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))))
Theorem	evlspw 22065	Polynomial evaluation for subrings maps the exponentiation of a polynomial to the exponentiation of the evaluated polynomial. (Contributed by SN, 29-Feb-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑃 = (𝑆 ↑s (𝐾 ↑m 𝐼))    &   ⊢ 𝐻 = (mulGrp‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑁 ↑ 𝑋)) = (𝑁(.g‘𝐻)(𝑄‘𝑋)))
Theorem	evlsvarpw 22066	Polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by SN, 21-Feb-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝑋 = ((𝐼 mVar 𝑈)‘𝑌)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑃 = (𝑆 ↑s (𝐵 ↑m 𝐼))    &   ⊢ 𝐻 = (mulGrp‘𝑃)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑁 ↑ 𝑋)) = (𝑁(.g‘𝐻)(𝑄‘𝑋)))
Theorem	evlval 22067	Value of the simple/same ring evaluation map. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ 𝑄 = ((𝐼 evalSub 𝑅)‘𝐵)
Theorem	evlrhm 22068	The simple evaluation map is a ring homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (𝑅 ↑s (𝐵 ↑m 𝐼))    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing) → 𝑄 ∈ (𝑊 RingHom 𝑇))
Theorem	evlsscasrng 22069	The evaluation of a scalar of a subring yields the same result as evaluated as a scalar over the ring itself. (Contributed by AV, 12-Sep-2019.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑂 = (𝐼 eval 𝑆)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐶 = (algSc‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    ⇒   ⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = (𝑂‘(𝐶‘𝑋)))
Theorem	evlsca 22070	Simple polynomial evaluation maps scalars to constant functions. (Contributed by AV, 12-Sep-2019.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = ((𝐵 ↑m 𝐼) × {𝑋}))
Theorem	evlsvarsrng 22071	The evaluation of the variable of polynomials over subring yields the same result as evaluated as variable of the polynomials over the ring itself. (Contributed by AV, 12-Sep-2019.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑂 = (𝐼 eval 𝑆)    &   ⊢ 𝑉 = (𝐼 mVar 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑉‘𝑋)) = (𝑂‘(𝑉‘𝑋)))
Theorem	evlvar 22072*	Simple polynomial evaluation maps variables to projections. (Contributed by AV, 12-Sep-2019.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝑉 = (𝐼 mVar 𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑉‘𝑋)) = (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑋)))
Theorem	mpfconst 22073	Constants are multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    ⇒   ⊢ (𝜑 → ((𝐵 ↑m 𝐼) × {𝑋}) ∈ 𝑄)
Theorem	mpfproj 22074*	Projections are multivariate polynomial functions. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑓 ∈ (𝐵 ↑m 𝐼) ↦ (𝑓‘𝐽)) ∈ 𝑄)
Theorem	mpfsubrg 22075	Polynomial functions are a subring. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) (Revised by AV, 19-Sep-2021.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ (SubRing‘(𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))))
Theorem	mpff 22076	Polynomial functions are functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ 𝑄 → 𝐹:(𝐵 ↑m 𝐼)⟶𝐵)
Theorem	mpfaddcl 22077	The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f + 𝐺) ∈ 𝑄)
Theorem	mpfmulcl 22078	The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ · = (.r‘𝑆)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f · 𝐺) ∈ 𝑄)
Theorem	mpfind 22079*	Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ · = (.r‘𝑆)    &   ⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜁)    &   ⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜎)    &   ⊢ (𝑥 = ((𝐵 ↑m 𝐼) × {𝑓}) → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑓)) → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑓 → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝑔 → (𝜓 ↔ 𝜂))    &   ⊢ (𝑥 = (𝑓 ∘f + 𝑔) → (𝜓 ↔ 𝜁))    &   ⊢ (𝑥 = (𝑓 ∘f · 𝑔) → (𝜓 ↔ 𝜎))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜌))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑅) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐼) → 𝜃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑄)    ⇒   ⊢ (𝜑 → 𝜌)
11.3.3  Additional definitions for (multivariate) polynomials
Syntax	cslv 22080	Select a subset of variables in a multivariate polynomial.
class selectVars
Syntax	cmhp 22081	Multivariate polynomials.
class mHomP
Syntax	cpsd 22082	Power series partial derivative function.
class mPSDer
Syntax	cai 22083	Algebraically independent.
class AlgInd
Definition	df-selv 22084*	Define the "variable selection" function. The function ((𝐼 selectVars 𝑅)‘𝐽) maps elements of (𝐼 mPoly 𝑅) bijectively onto (𝐽 mPoly ((𝐼 ∖ 𝐽) mPoly 𝑅)) in the natural way, for example if 𝐼 = {𝑥, 𝑦} and 𝐽 = {𝑦} it would map 1 + 𝑥 + 𝑦 + 𝑥𝑦 ∈ ({𝑥, 𝑦} mPoly ℤ) to (1 + 𝑥) + (1 + 𝑥)𝑦 ∈ ({𝑦} mPoly ({𝑥} mPoly ℤ)). This, for example, allows one to treat a multivariate polynomial as a univariate polynomial with coefficients in a polynomial ring with one less variable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ selectVars = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑢⦌⦋(𝑗 mPoly 𝑢) / 𝑡⦌⦋(algSc‘𝑡) / 𝑐⦌⦋(𝑐 ∘ (algSc‘𝑢)) / 𝑑⦌((((𝑖 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))))))))
Theorem	selvffval 22085*	Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐼 selectVars 𝑅) = (𝑗 ∈ 𝒫 𝐼 ↦ (𝑓 ∈ (Base‘(𝐼 mPoly 𝑅)) ↦ ⦋((𝐼 ∖ 𝑗) mPoly 𝑅) / 𝑢⦌⦋(𝑗 mPoly 𝑢) / 𝑡⦌⦋(algSc‘𝑡) / 𝑐⦌⦋(𝑐 ∘ (algSc‘𝑢)) / 𝑑⦌((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼 ∖ 𝑗) mVar 𝑅)‘𝑥))))))))
Theorem	selvfval 22086*	Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐼 selectVars 𝑅)‘𝐽) = (𝑓 ∈ (Base‘(𝐼 mPoly 𝑅)) ↦ ⦋((𝐼 ∖ 𝐽) mPoly 𝑅) / 𝑢⦌⦋(𝐽 mPoly 𝑢) / 𝑡⦌⦋(algSc‘𝑡) / 𝑐⦌⦋(𝑐 ∘ (algSc‘𝑢)) / 𝑑⦌((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑 ∘ 𝑓))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))))
Theorem	selvval 22087*	Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷 ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))
Definition	df-mhp 22088*	Define the subspaces of order- 𝑛 homogeneous polynomials. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ mHomP = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑛}}))
Theorem	reldmmhp 22089	The domain of the homogeneous polynomial operator is a relation. (Contributed by SN, 18-May-2025.)
⊢ Rel dom mHomP
Theorem	mhpfval 22090*	Value of the "homogeneous polynomial" operator. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ 𝐵 ∣ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑛}}))
Theorem	mhpval 22091*	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 22092*	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 22093*	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 22094*	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	mhprcl 22095	Reverse closure for homogeneous polynomials, use elfvov1 7455 and elfvov2 7456 with reldmmhp 22089 for the reverse closure of 𝐼 and 𝑅. (Contributed by SN, 4-Aug-2025.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ0)
Theorem	mhpmpl 22096	A homogeneous polynomial is a polynomial. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	mhpdeg 22097*	All nonzero terms of a homogeneous polynomial have degree 𝑁. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑋 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁})
Theorem	mhp0cl 22098*	The zero polynomial is homogeneous. Under df-mhp 22088, 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 26030 and df-dgr 26166 respectively) and the literature: https://math.stackexchange.com/a/1796314/593843 26166. (Contributed by SN, 12-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐷 × { 0 }) ∈ (𝐻‘𝑁))
Theorem	mhpsclcl 22099	A scalar (or constant) polynomial has degree 0. Compare deg1scl 26088. In other contexts, there may be an exception for the zero polynomial, but under df-mhp 22088 the zero polynomial can be any degree (see mhp0cl 22098) so there is no exception. (Contributed by SN, 25-May-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝐴‘𝐶) ∈ (𝐻‘0))
Theorem	mhpvarcl 22100	A power series variable is a polynomial of degree 1. (Contributed by SN, 25-May-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑉‘𝑋) ∈ (𝐻‘1))