![]() |
Metamath
Proof Explorer Theorem List (p. 221 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | psrass1 22001* | Associative identity for the ring of power series. (Contributed by Mario Carneiro, 5-Jan-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ × = (.r‘𝑆) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 × 𝑌) × 𝑍) = (𝑋 × (𝑌 × 𝑍))) | ||
Theorem | psrdi 22002* | Distributive law for the ring of power series (left-distributivity). (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ × = (.r‘𝑆) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ + = (+g‘𝑆) ⇒ ⊢ (𝜑 → (𝑋 × (𝑌 + 𝑍)) = ((𝑋 × 𝑌) + (𝑋 × 𝑍))) | ||
Theorem | psrdir 22003* | Distributive law for the ring of power series (right-distributivity). (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ × = (.r‘𝑆) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ + = (+g‘𝑆) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) × 𝑍) = ((𝑋 × 𝑍) + (𝑌 × 𝑍))) | ||
Theorem | psrass23l 22004* | Associative identity for the ring of power series. Part of psrass23 22006 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 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ × = (.r‘𝑆) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌))) | ||
Theorem | psrcom 22005* | Commutative law for the ring of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ × = (.r‘𝑆) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → (𝑋 × 𝑌) = (𝑌 × 𝑋)) | ||
Theorem | psrass23 22006* | 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 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ × = (.r‘𝑆) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) ⇒ ⊢ (𝜑 → (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌)))) | ||
Theorem | psrring 22007 | The ring of power series is a ring. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑆 ∈ Ring) | ||
Theorem | psr1 22008* | The identity element of the ring of power series. (Contributed by Mario Carneiro, 8-Jan-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑈 = (1r‘𝑆) ⇒ ⊢ (𝜑 → 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 ))) | ||
Theorem | psrcrng 22009 | The ring of power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝑆 ∈ CRing) | ||
Theorem | psrassa 22010 | The ring of power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝑆 ∈ AssAlg) | ||
Theorem | resspsrbas 22011 | 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 22012 | 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 22013 | 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 22014 | 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 22015 | 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 | psrascl 22016* | Value of the scalar injection into the power series algebra. (Contributed by SN, 18-May-2025.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑋, 0 ))) | ||
Theorem | psrasclcl 22017 | A scalar is lifted into a member of the power series. (Contributed by SN, 25-Apr-2025.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝐴‘𝐶) ∈ 𝐵) | ||
Theorem | mvrfval 22018* | Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ 𝑌) ⇒ ⊢ (𝜑 → 𝑉 = (𝑥 ∈ 𝐼 ↦ (𝑓 ∈ 𝐷 ↦ if(𝑓 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0)), 1 , 0 )))) | ||
Theorem | mvrval 22019* | Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑉‘𝑋) = (𝑓 ∈ 𝐷 ↦ if(𝑓 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)), 1 , 0 ))) | ||
Theorem | mvrval2 22020* | Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) ⇒ ⊢ (𝜑 → ((𝑉‘𝑋)‘𝐹) = if(𝐹 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)), 1 , 0 )) | ||
Theorem | mvrid 22021* | The 𝑋𝑖-th coefficient of the term 𝑋𝑖 is 1. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → ((𝑉‘𝑋)‘(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) = 1 ) | ||
Theorem | mvrf 22022 | 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 22023 | 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 22024 | A power series variable is an element of the base set. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑉‘𝑋) ∈ 𝐵) | ||
Theorem | reldmmpl 22025 | The multivariate polynomial constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ Rel dom mPoly | ||
Theorem | mplval 22026* | 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 22027* | 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 22028 | 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 | mvrcl 22029 | A power series variable is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑉‘𝑋) ∈ 𝐵) | ||
Theorem | mvrf2 22030 | The power series/polynomial variable function maps indices to polynomials. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑉:𝐼⟶𝐵) | ||
Theorem | mplrcl 22031 | Reverse closure for the polynomial index set. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝑋 ∈ 𝐵 → 𝐼 ∈ V) | ||
Theorem | mplelsfi 22032 | A polynomial treated as a coefficient function has finitely many nonzero terms. (Contributed by Stefan O'Rear, 22-Mar-2015.) (Revised by AV, 25-Jun-2019.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐹 finSupp 0 ) | ||
Theorem | mplval2 22033 | 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 22034 | 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 22035* | 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 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋:𝐷⟶𝐾) | ||
Theorem | mplsubglem 22036* | 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 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → ∅ ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∪ 𝑦) ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ∈ 𝐴) & ⊢ (𝜑 → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}) & ⊢ (𝜑 → 𝑅 ∈ Grp) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑆)) | ||
Theorem | mpllsslem 22037* | 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 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → ∅ ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∪ 𝑦) ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ∈ 𝐴) & ⊢ (𝜑 → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑆)) | ||
Theorem | mplsubglem2 22038* | Lemma for mplsubg 22039 and mpllss 22040. (Contributed by AV, 16-Jul-2019.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑈 = {𝑔 ∈ (Base‘𝑆) ∣ (𝑔 supp (0g‘𝑅)) ∈ Fin}) | ||
Theorem | mplsubg 22039 | 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 22040 | 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 22041* | Lemma for mplsubrg 22042. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by AV, 18-Jul-2019.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = ( ∘f + “ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌) ∈ 𝑈) | ||
Theorem | mplsubrg 22042 | 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 22043* | The zero polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑂 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Grp) ⇒ ⊢ (𝜑 → 0 = (𝐷 × {𝑂})) | ||
Theorem | mplplusg 22044 | Value of addition in a polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ + = (+g‘𝑌) ⇒ ⊢ + = (+g‘𝑆) | ||
Theorem | mplmulr 22045 | Value of multiplication in a polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ · = (.r‘𝑌) ⇒ ⊢ · = (.r‘𝑆) | ||
Theorem | mpladd 22046 | The addition operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ + = (+g‘𝑅) & ⊢ ✚ = (+g‘𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ✚ 𝑌) = (𝑋 ∘f + 𝑌)) | ||
Theorem | mplneg 22047 | The negative function on multivariate polynomials. (Contributed by SN, 25-May-2024.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝑀 = (invg‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑀‘𝑋) = (𝑁 ∘ 𝑋)) | ||
Theorem | mplmul 22048* | The multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑅) & ⊢ ∙ = (.r‘𝑃) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∙ 𝐺) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝐹‘𝑥) · (𝐺‘(𝑘 ∘f − 𝑥))))))) | ||
Theorem | mpl1 22049* | The identity element of the ring of polynomials. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑈 = (1r‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 ))) | ||
Theorem | mplsca 22050 | The scalar field of a multivariate polynomial structure. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) | ||
Theorem | mplvsca2 22051 | The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) ⇒ ⊢ · = ( ·𝑠 ‘𝑆) | ||
Theorem | mplvsca 22052* | 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 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∙ 𝐹) = ((𝐷 × {𝑋}) ∘f · 𝐹)) | ||
Theorem | mplvscaval 22053* | The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ ∙ = ( ·𝑠 ‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → ((𝑋 ∙ 𝐹)‘𝑌) = (𝑋 · (𝐹‘𝑌))) | ||
Theorem | mplgrp 22054 | The polynomial ring is a group. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp) → 𝑃 ∈ Grp) | ||
Theorem | mpllmod 22055 | The polynomial ring is a left module. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ LMod) | ||
Theorem | mplring 22056 | The polynomial ring is a ring. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring) | ||
Theorem | mpllvec 22057 | The polynomial ring is a vector space. (Contributed by SN, 29-Feb-2024.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ DivRing) → 𝑃 ∈ LVec) | ||
Theorem | mplcrng 22058 | The polynomial ring is a commutative ring. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ CRing) | ||
Theorem | mplassa 22059 | The polynomial ring is an associative algebra. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg) | ||
Theorem | mplringd 22060 | The polynomial ring is a ring. (Contributed by SN, 7-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑃 ∈ Ring) | ||
Theorem | mpllmodd 22061 | The polynomial ring is a left module. (Contributed by SN, 12-Mar-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑃 ∈ LMod) | ||
Theorem | ressmplbas2 22062 | The base set of a restricted polynomial algebra consists of power series in the subring which are also polynomials (in the parent ring). (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (𝐼 mPoly 𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (𝐼 mPoly 𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑊 = (𝐼 mPwSer 𝐻) & ⊢ 𝐶 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 ∩ 𝐾)) | ||
Theorem | ressmplbas 22063 | A restricted polynomial algebra has the same base set. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (𝐼 mPoly 𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (𝐼 mPoly 𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑃 = (𝑆 ↾s 𝐵) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝑃)) | ||
Theorem | ressmpladd 22064 | 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 22065 | 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 22066 | 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 22067 | 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 22068 | 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 22069 | 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 22070* | 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 22071* | 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 22072* | 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 22073* | 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 22074* | Lemma for mplcoe4 22112. (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 22075* | Decompose a monomial into a finite product of powers of variables. Instead of assuming that 𝑅 is a commutative ring (as in mplcoe2 22076), 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 22076* | 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 22077 | 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 22078* | Value of the well-order on finite bags. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐶 = (𝑇 <bag 𝐼) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐶 = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐷 ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))}) | ||
Theorem | ltbwe 22079* | 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 22080 | Lemma for ordered power series. (Contributed by Stefan O'Rear, 2-Oct-2015.) |
⊢ Rel dom ordPwSer | ||
Theorem | opsrval 22081* | The value of the "ordered power series" function. This is the same as mPwSer psrval 21952, 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 22082* | 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 22083 | Self-referential expression for the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ ≤ = (le‘𝑂) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → 𝑂 = (𝑆 sSet 〈(le‘ndx), ≤ 〉)) | ||
Theorem | opsrbaslem 22084 | 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 22085 | Obsolete version of opsrbaslem 22084 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 22086 | 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 22087 | Obsolete version of opsrbaslem 22084 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 22088 | 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 22089 | Obsolete version of opsrplusg 22088 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 22090 | 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 22091 | Obsolete version of opsrmulr 22090 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 22092 | 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 22093 | Obsolete version of opsrvsca 22092 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 22094 | 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 22095 | Obsolete version of opsrsca 22094 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 22096* | Lemma for opsrtos 22098. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Toset) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) & ⊢ (𝜑 → 𝑇 We 𝐼) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ < = (lt‘𝑅) & ⊢ 𝐶 = (𝑇 <bag 𝐼) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜓 ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ (𝜑 → ≤ = (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵))) | ||
Theorem | opsrtoslem2 22097* | Lemma for opsrtos 22098. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Toset) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) & ⊢ (𝜑 → 𝑇 We 𝐼) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ < = (lt‘𝑅) & ⊢ 𝐶 = (𝑇 <bag 𝐼) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜓 ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ (𝜑 → 𝑂 ∈ Toset) | ||
Theorem | opsrtos 22098 | The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Toset) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) & ⊢ (𝜑 → 𝑇 We 𝐼) ⇒ ⊢ (𝜑 → 𝑂 ∈ Toset) | ||
Theorem | opsrso 22099 | 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 22100 | The ring of ordered power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → 𝑂 ∈ CRing) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |