P. 217 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21601-21700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	opsrle 21601*	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 21602	Self-referential expression for the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ ≤ = (le‘𝑂)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → 𝑂 = (𝑆 sSet ⟨(le‘ndx), ≤ ⟩))
Theorem	opsrbaslem 21603	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	opsrbaslemOLD 21604	Obsolete version of opsrbaslem 21603 as of 1-Nov-2024. 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.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑁 < ;10    ⇒   ⊢ (𝜑 → (𝐸‘𝑆) = (𝐸‘𝑂))
Theorem	opsrbas 21605	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	opsrbasOLD 21606	Obsolete version of opsrbaslem 21603 as of 1-Nov-2024. The base set of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → (Base‘𝑆) = (Base‘𝑂))
Theorem	opsrplusg 21607	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	opsrplusgOLD 21608	Obsolete version of opsrplusg 21607 as of 1-Nov-2024. The addition operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → (+g‘𝑆) = (+g‘𝑂))
Theorem	opsrmulr 21609	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	opsrmulrOLD 21610	Obsolete version of opsrmulr 21609 as of 1-Nov-2024. The multiplication operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → (.r‘𝑆) = (.r‘𝑂))
Theorem	opsrvsca 21611	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	opsrvscaOLD 21612	Obsolete version of opsrvsca 21611 as of 1-Nov-2024. The scalar product of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → ( ·𝑠 ‘𝑆) = ( ·𝑠 ‘𝑂))
Theorem	opsrsca 21613	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	opsrscaOLD 21614	Obsolete version of opsrsca 21613 as of 1-Nov-2024. The scalar ring of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝑅 = (Scalar‘𝑂))
Theorem	opsrtoslem1 21615*	Lemma for opsrtos 21617. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Toset)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    &   ⊢ (𝜑 → 𝑇 We 𝐼)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ < = (lt‘𝑅)    &   ⊢ 𝐶 = (𝑇 <bag 𝐼)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜓 ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))))    &   ⊢ ≤ = (le‘𝑂)    ⇒   ⊢ (𝜑 → ≤ = (({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)))
Theorem	opsrtoslem2 21616*	Lemma for opsrtos 21617. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Toset)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    &   ⊢ (𝜑 → 𝑇 We 𝐼)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ < = (lt‘𝑅)    &   ⊢ 𝐶 = (𝑇 <bag 𝐼)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜓 ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))))    &   ⊢ ≤ = (le‘𝑂)    ⇒   ⊢ (𝜑 → 𝑂 ∈ Toset)
Theorem	opsrtos 21617	The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Toset)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    &   ⊢ (𝜑 → 𝑇 We 𝐼)    ⇒   ⊢ (𝜑 → 𝑂 ∈ Toset)
Theorem	opsrso 21618	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 21619	The ring of ordered power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → 𝑂 ∈ CRing)
Theorem	opsrassa 21620	The ring of ordered power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼))    ⇒   ⊢ (𝜑 → 𝑂 ∈ AssAlg)
Theorem	mplmon2 21621*	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 21622*	The empty bag is a bag. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝐼 × {0}) ∈ 𝐷)
Theorem	psrbagsn 21623*	A singleton bag is a bag. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝐾, 1, 0)) ∈ 𝐷)
Theorem	mplascl 21624*	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 21625	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 21626	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 21627	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 21628*	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 21629*	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 21630*	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 21631*	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 21632	Evaluation of a multivariate polynomial in a subring.
class evalSub
Syntax	cevl 21633	Evaluation of a multivariate polynomial.
class eval
Definition	df-evls 21634*	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 21635*	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 21636*	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 21637*	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	psrbagev1OLD 21638*	Obsolete version of psrbagev1 21637 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) (Revised by AV, 11-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ · = (.g‘𝑇)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ CMnd)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝐵 ∘f · 𝐺):𝐼⟶𝐶 ∧ (𝐵 ∘f · 𝐺) finSupp 0 ))
Theorem	psrbagev2 21639*	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	psrbagev2OLD 21640*	Obsolete version of psrbagev2 21639 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 18-Jul-2019.) (Revised by AV, 11-Apr-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ · = (.g‘𝑇)    &   ⊢ (𝜑 → 𝑇 ∈ CMnd)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑇 Σg (𝐵 ∘f · 𝐺)) ∈ 𝐶)
Theorem	evlslem2 21641*	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 21642*	Lemma for evlseu 21645. 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 21643*	Lemma for evlseu 21645. 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 21644*	Lemma for evlseu 21645, 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 21645*	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 21646	Well-behaved binary operation property of evalSub. (Contributed by Stefan O'Rear, 19-Mar-2015.)
⊢ Rel dom evalSub
Theorem	mpfrcl 21647	Reverse closure for the set of polynomial functions. (Contributed by Stefan O'Rear, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝑄 → (𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)))
Theorem	evlsval 21648*	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 21649*	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 21650	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 21651	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 21652*	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 21653*	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 21654*	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 21655	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 21656	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 21657	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 21658	The simple evaluation map is a ring homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (𝑅 ↑s (𝐵 ↑m 𝐼))    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing) → 𝑄 ∈ (𝑊 RingHom 𝑇))
Theorem	evlsscasrng 21659	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 21660	Simple polynomial evaluation maps scalars to constant functions. (Contributed by AV, 12-Sep-2019.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = ((𝐵 ↑m 𝐼) × {𝑋}))
Theorem	evlsvarsrng 21661	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 21662*	Simple polynomial evaluation maps variables to projections. (Contributed by AV, 12-Sep-2019.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝑉 = (𝐼 mVar 𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑉‘𝑋)) = (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑋)))
Theorem	mpfconst 21663	Constants are multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    ⇒   ⊢ (𝜑 → ((𝐵 ↑m 𝐼) × {𝑋}) ∈ 𝑄)
Theorem	mpfproj 21664*	Projections are multivariate polynomial functions. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑓 ∈ (𝐵 ↑m 𝐼) ↦ (𝑓‘𝐽)) ∈ 𝑄)
Theorem	mpfsubrg 21665	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 21666	Polynomial functions are functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ 𝑄 → 𝐹:(𝐵 ↑m 𝐼)⟶𝐵)
Theorem	mpfaddcl 21667	The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f + 𝐺) ∈ 𝑄)
Theorem	mpfmulcl 21668	The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ · = (.r‘𝑆)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f · 𝐺) ∈ 𝑄)
Theorem	mpfind 21669*	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 21670	Select a subset of variables in a multivariate polynomial.
class selectVars
Syntax	cmhp 21671	Multivariate polynomials.
class mHomP
Syntax	cpsd 21672	Power series partial derivative function.
class mPSDer
Syntax	cai 21673	Algebraically independent.
class AlgInd
Definition	df-selv 21674*	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 𝑟)‘𝑥))))))))
Definition	df-mhp 21675*	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 𝑔) = 𝑛}}))
Definition	df-psd 21676*	Define the differentiation operation on multivariate polynomials. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ mPSDer = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))
Definition	df-algind 21677*	Define the predicate "the set 𝑣 is algebraically independent in the algebra 𝑤". A collection of vectors is algebraically independent if no nontrivial polynomial with elements from the subset evaluates to zero. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ AlgInd = (𝑤 ∈ V, 𝑘 ∈ 𝒫 (Base‘𝑤) ↦ {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))})
Theorem	selvffval 21678*	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 21679*	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 21680*	Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷 ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))
Theorem	mhpfval 21681*	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 21682*	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 21683*	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 21684*	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 21685*	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 21686	A homogeneous polynomial is a polynomial. (Contributed by Steven Nguyen, 25-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	mhpdeg 21687*	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 21688*	The zero polynomial is homogeneous. Under df-mhp 21675, 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 25569 and df-dgr 25704 respectively) and the literature: https://math.stackexchange.com/a/1796314/593843 25704. (Contributed by SN, 12-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐷 × { 0 }) ∈ (𝐻‘𝑁))
Theorem	mhpsclcl 21689	A scalar (or constant) polynomial has degree 0. Compare deg1scl 25630. In other contexts, there may be an exception for the zero polynomial, but under df-mhp 21675 the zero polynomial can be any degree (see mhp0cl 21688) so there is no exception. (Contributed by SN, 25-May-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝐴‘𝐶) ∈ (𝐻‘0))
Theorem	mhpvarcl 21690	A power series variable is a polynomial of degree 1. (Contributed by SN, 25-May-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑉‘𝑋) ∈ (𝐻‘1))
Theorem	mhpmulcl 21691	A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 25596 (which shows less-than-or-equal instead of equal). (Contributed by SN, 22-Jul-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑌 = (𝐼 mPoly 𝑅)    &   ⊢ · = (.r‘𝑌)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑃 ∈ (𝐻‘𝑀))    &   ⊢ (𝜑 → 𝑄 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑃 · 𝑄) ∈ (𝐻‘(𝑀 + 𝑁)))
Theorem	mhppwdeg 21692	Degree of a homogeneous polynomial raised to a power. General version of deg1pw 25637. (Contributed by SN, 26-Jul-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑀))    ⇒   ⊢ (𝜑 → (𝑁 ↑ 𝑋) ∈ (𝐻‘(𝑀 · 𝑁)))
Theorem	mhpaddcl 21693	Homogeneous polynomials are closed under addition. (Contributed by SN, 26-Aug-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ + = (+g‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐻‘𝑁))
Theorem	mhpinvcl 21694	Homogeneous polynomials are closed under taking the opposite. (Contributed by SN, 12-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑀 = (invg‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) ∈ (𝐻‘𝑁))
Theorem	mhpsubg 21695	Homogeneous polynomials form a subgroup of the polynomials. (Contributed by SN, 25-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐻‘𝑁) ∈ (SubGrp‘𝑃))
Theorem	mhpvscacl 21696	Homogeneous polynomials are closed under scalar multiplication. (Contributed by SN, 25-Sep-2023.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐻‘𝑁))    ⇒   ⊢ (𝜑 → (𝑋 · 𝐹) ∈ (𝐻‘𝑁))
Theorem	mhplss 21697	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 21727. 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 21727). 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 21698	Univariate power series.
class PwSer1
Syntax	cv1 21699	The base variable of a univariate power series.
class var1
Syntax	cpl1 21700	Univariate polynomials.
class Poly1