Home | Metamath
Proof Explorer Theorem List (p. 202 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | psrvsca 20101* | The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ ∙ = ( ·𝑠 ‘𝑆) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ · = (.r‘𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∙ 𝐹) = ((𝐷 × {𝑋}) ∘f · 𝐹)) | ||
Theorem | psrvscaval 20102* | The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ ∙ = ( ·𝑠 ‘𝑆) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ · = (.r‘𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → ((𝑋 ∙ 𝐹)‘𝑌) = (𝑋 · (𝐹‘𝑌))) | ||
Theorem | psrvscacl 20103 | Closure of the power series scalar multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 𝐹) ∈ 𝐵) | ||
Theorem | psr0cl 20104* | The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝐵) | ||
Theorem | psr0lid 20105* | The zero element of the ring of power series is a left identity. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐷 × { 0 }) + 𝑋) = 𝑋) | ||
Theorem | psrnegcl 20106* | The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑁 ∘ 𝑋) ∈ 𝐵) | ||
Theorem | psrlinv 20107* | The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 0 = (0g‘𝑅) & ⊢ + = (+g‘𝑆) ⇒ ⊢ (𝜑 → ((𝑁 ∘ 𝑋) + 𝑋) = (𝐷 × { 0 })) | ||
Theorem | psrgrp 20108 | The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Grp) ⇒ ⊢ (𝜑 → 𝑆 ∈ Grp) | ||
Theorem | psr0 20109* | The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑂 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑆) ⇒ ⊢ (𝜑 → 0 = (𝐷 × {𝑂})) | ||
Theorem | psrneg 20110* | The negative function of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑀 = (invg‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑀‘𝑋) = (𝑁 ∘ 𝑋)) | ||
Theorem | psrlmod 20111 | The ring of power series is a left module. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑆 ∈ LMod) | ||
Theorem | psr1cl 20112* | The identity element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 )) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝐵) | ||
Theorem | psrlidm 20113* | The identity element of the ring of power series is a left identity. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by AV, 8-Jul-2019.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 )) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑈 · 𝑋) = 𝑋) | ||
Theorem | psrridm 20114* | The identity element of the ring of power series is a right identity. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by AV, 8-Jul-2019.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 )) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 𝑈) = 𝑋) | ||
Theorem | psrass1 20115* | Associative identity for the ring of power series. (Contributed by Mario Carneiro, 5-Jan-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ × = (.r‘𝑆) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 × 𝑌) × 𝑍) = (𝑋 × (𝑌 × 𝑍))) | ||
Theorem | psrdi 20116* | 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 20117* | 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 20118* | Associative identity for the ring of power series. Part of psrass23 20120 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 20119* | 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 20120* | 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 20121 | The ring of power series is a ring. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑆 ∈ Ring) | ||
Theorem | psr1 20122* | 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 20123 | The ring of power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝑆 ∈ CRing) | ||
Theorem | psrassa 20124 | The ring of power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝑆 ∈ AssAlg) | ||
Theorem | resspsrbas 20125 | 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 20126 | 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 20127 | 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 20128 | 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 20129 | A subring of the base ring induces a subring of power series. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (𝐼 mPwSer 𝐻) & ⊢ 𝐵 = (Base‘𝑈) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝐵 ∈ (SubRing‘𝑆)) | ||
Theorem | mvrfval 20130* | 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 20131* | 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 20132* | 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 20133* | 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 20134 | 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 20135 | 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 20136 | A power series variable is an element of the base set. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑉‘𝑋) ∈ 𝐵) | ||
Theorem | reldmmpl 20137 | The multivariate polynomial constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ Rel dom mPoly | ||
Theorem | mplval 20138* | 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 20139* | 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 20140 | Property of being a polynomial. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) ⇒ ⊢ (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 finSupp 0 )) | ||
Theorem | mplval2 20141 | 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 20142 | 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 20143* | 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 20144* | 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 20145* | 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 20146* | Lemma for mplsubg 20147 and mpllss 20148. (Contributed by AV, 16-Jul-2019.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑈 = {𝑔 ∈ (Base‘𝑆) ∣ (𝑔 supp (0g‘𝑅)) ∈ Fin}) | ||
Theorem | mplsubg 20147 | 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 20148 | 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 20149* | Lemma for mplsubrg 20150. (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 20150 | 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 20151* | The zero polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑂 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Grp) ⇒ ⊢ (𝜑 → 0 = (𝐷 × {𝑂})) | ||
Theorem | mpladd 20152 | 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 | mplmul 20153* | 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 20154* | 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 20155 | The scalar field of a multivariate polynomial structure. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) | ||
Theorem | mplvsca2 20156 | The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) ⇒ ⊢ · = ( ·𝑠 ‘𝑆) | ||
Theorem | mplvsca 20157* | 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 20158* | The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ ∙ = ( ·𝑠 ‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → ((𝑋 ∙ 𝐹)‘𝑌) = (𝑋 · (𝐹‘𝑌))) | ||
Theorem | mvrcl 20159 | A power series variable is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑉‘𝑋) ∈ 𝐵) | ||
Theorem | mplgrp 20160 | The polynomial ring is a group. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp) → 𝑃 ∈ Grp) | ||
Theorem | mpllmod 20161 | The polynomial ring is a left module. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ LMod) | ||
Theorem | mplring 20162 | The polynomial ring is a ring. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring) | ||
Theorem | mpllvec 20163 | The polynomial ring is a vector space. (Contributed by SN, 29-Feb-2024.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ DivRing) → 𝑃 ∈ LVec) | ||
Theorem | mplcrng 20164 | The polynomial ring is a commutative ring. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ CRing) | ||
Theorem | mplassa 20165 | The polynomial ring is an associative algebra. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg) | ||
Theorem | ressmplbas2 20166 | 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 20167 | 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 20168 | 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 20169 | 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 20170 | 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 20171 | 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 20172 | 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 20173 | 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 20174* | 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 20175* | 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 20176* | 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 20177* | 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 20178* | Lemma for mplcoe4 20213. (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 20179* | Decompose a monomial into a finite product of powers of variables. Instead of assuming that 𝑅 is a commutative ring (as in mplcoe2 20180), 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 20180* | 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 20181 | 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 20182* | Value of the well-order on finite bags. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐶 = (𝑇 <bag 𝐼) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐶 = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐷 ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))}) | ||
Theorem | ltbwe 20183* | 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 20184 | Lemma for ordered power series. (Contributed by Stefan O'Rear, 2-Oct-2015.) |
⊢ Rel dom ordPwSer | ||
Theorem | opsrval 20185* | The value of the "ordered power series" function. This is the same as mPwSer psrval 20072, 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 20186* | 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 20187 | Self-referential expression for the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ ≤ = (le‘𝑂) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → 𝑂 = (𝑆 sSet 〈(le‘ndx), ≤ 〉)) | ||
Theorem | opsrbaslem 20188 | 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.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 < ;10 ⇒ ⊢ (𝜑 → (𝐸‘𝑆) = (𝐸‘𝑂)) | ||
Theorem | opsrbas 20189 | The base set of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → (Base‘𝑆) = (Base‘𝑂)) | ||
Theorem | opsrplusg 20190 | The addition operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → (+g‘𝑆) = (+g‘𝑂)) | ||
Theorem | opsrmulr 20191 | The multiplication operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → (.r‘𝑆) = (.r‘𝑂)) | ||
Theorem | opsrvsca 20192 | The scalar product operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → ( ·𝑠 ‘𝑆) = ( ·𝑠 ‘𝑂)) | ||
Theorem | opsrsca 20193 | The scalar ring of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑅 = (Scalar‘𝑂)) | ||
Theorem | opsrtoslem1 20194* | Lemma for opsrtos 20196. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Toset) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) & ⊢ (𝜑 → 𝑇 We 𝐼) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ < = (lt‘𝑅) & ⊢ 𝐶 = (𝑇 <bag 𝐼) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜓 ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ (𝜑 → ≤ = (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵))) | ||
Theorem | opsrtoslem2 20195* | Lemma for opsrtos 20196. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Toset) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) & ⊢ (𝜑 → 𝑇 We 𝐼) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ < = (lt‘𝑅) & ⊢ 𝐶 = (𝑇 <bag 𝐼) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜓 ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ (𝜑 → 𝑂 ∈ Toset) | ||
Theorem | opsrtos 20196 | The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Toset) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) & ⊢ (𝜑 → 𝑇 We 𝐼) ⇒ ⊢ (𝜑 → 𝑂 ∈ Toset) | ||
Theorem | opsrso 20197 | 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 20198 | The ring of ordered power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → 𝑂 ∈ CRing) | ||
Theorem | opsrassa 20199 | The ring of ordered power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → 𝑂 ∈ AssAlg) | ||
Theorem | mplrcl 20200 | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |