Home | Metamath
Proof Explorer Theorem List (p. 202 of 450) | < 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-28693) |
Hilbert Space Explorer
(28694-30216) |
Users' Mathboxes
(30217-44980) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | aspss 20101 | Span preserves subset ordering. (spanss 29123 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝐴 = (AlgSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆) → (𝐴‘𝑇) ⊆ (𝐴‘𝑆)) | ||
Theorem | aspssid 20102 | A set of vectors is a subset of its span. (spanss2 29120 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝐴 = (AlgSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ (𝐴‘𝑆)) | ||
Theorem | asclfval 20103* | Function value of the algebraic scalars function. (Contributed by Mario Carneiro, 8-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 1 = (1r‘𝑊) ⇒ ⊢ 𝐴 = (𝑥 ∈ 𝐾 ↦ (𝑥 · 1 )) | ||
Theorem | asclval 20104 | Value of a mapped algebra scalar. (Contributed by Mario Carneiro, 8-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 1 = (1r‘𝑊) ⇒ ⊢ (𝑋 ∈ 𝐾 → (𝐴‘𝑋) = (𝑋 · 1 )) | ||
Theorem | asclfn 20105 | Unconditional functionality of the algebra scalars function. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ 𝐴 Fn 𝐾 | ||
Theorem | asclf 20106 | The algebra scalars function is a function into the base set. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ Ring) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝜑 → 𝐴:𝐾⟶𝐵) | ||
Theorem | asclghm 20107 | The algebra scalars function is a group homomorphism. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ Ring) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐹 GrpHom 𝑊)) | ||
Theorem | ascl0 20108 | The scalar 0 embedded into a left module corresponds to the 0 of the left module if the left module is also a ring. (Contributed by AV, 31-Jul-2019.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑊 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐴‘(0g‘𝐹)) = (0g‘𝑊)) | ||
Theorem | asclmul1 20109 | Left multiplication by a lifted scalar is the same as the scalar operation. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ × = (.r‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → ((𝐴‘𝑅) × 𝑋) = (𝑅 · 𝑋)) | ||
Theorem | asclmul2 20110 | Right multiplication by a lifted scalar is the same as the scalar operation. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ × = (.r‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑋 × (𝐴‘𝑅)) = (𝑅 · 𝑋)) | ||
Theorem | ascldimul 20111 | The algebra scalars function distributes over multiplication. (Contributed by Mario Carneiro, 8-Mar-2015.) (Proof shortened by SN, 5-Nov-2023.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ × = (.r‘𝑊) & ⊢ · = (.r‘𝐹) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → (𝐴‘(𝑅 · 𝑆)) = ((𝐴‘𝑅) × (𝐴‘𝑆))) | ||
Theorem | ascldimulOLD 20112 | Obsolete version of ascldimul 20111 as of 5-Nov-2023. (Contributed by Mario Carneiro, 8-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ × = (.r‘𝑊) & ⊢ · = (.r‘𝐹) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑆 ∈ 𝐾) → (𝐴‘(𝑅 · 𝑆)) = ((𝐴‘𝑅) × (𝐴‘𝑆))) | ||
Theorem | asclinvg 20113 | The group inverse (negation) of a lifted scalar is the lifted negation of the scalar. (Contributed by AV, 2-Sep-2019.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ 𝐽 = (invg‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐶 ∈ 𝐵) → (𝐽‘(𝐴‘𝐶)) = (𝐴‘(𝐼‘𝐶))) | ||
Theorem | asclrhm 20114 | The scalar injection is a ring homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ AssAlg → 𝐴 ∈ (𝐹 RingHom 𝑊)) | ||
Theorem | rnascl 20115 | The set of injected scalars is also interpretable as the span of the identity. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 1 = (1r‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝑊 ∈ AssAlg → ran 𝐴 = (𝑁‘{ 1 })) | ||
Theorem | issubassa2 20116 | A subring of a unital algebra is a subspace and thus a subalgebra iff it contains all scalar multiples of the identity. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) → (𝑆 ∈ 𝐿 ↔ ran 𝐴 ⊆ 𝑆)) | ||
Theorem | rnasclsubrg 20117 | The scalar multiples of the unit vector form a subring of the vectors. (Contributed by SN, 5-Nov-2023.) |
⊢ 𝐶 = (algSc‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) ⇒ ⊢ (𝜑 → ran 𝐶 ∈ (SubRing‘𝑊)) | ||
Theorem | rnasclmulcl 20118 | (Vector) multiplication is closed for scalar multiples of the unit vector. (Contributed by SN, 5-Nov-2023.) |
⊢ 𝐶 = (algSc‘𝑊) & ⊢ × = (.r‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ ran 𝐶 ∧ 𝑌 ∈ ran 𝐶)) → (𝑋 × 𝑌) ∈ ran 𝐶) | ||
Theorem | rnasclassa 20119 | The scalar multiples of the unit vector form a subalgebra of the vectors. (Contributed by SN, 16-Nov-2023.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝑈 = (𝑊 ↾s ran 𝐴) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) ⇒ ⊢ (𝜑 → 𝑈 ∈ AssAlg) | ||
Theorem | ressascl 20120 | The injection of scalars is invariant between subalgebras and superalgebras. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝑋 = (𝑊 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 = (algSc‘𝑋)) | ||
Theorem | asclpropd 20121* | If two structures have the same components (properties), one is an associative algebra iff the other one is. The last hypotheses on 1r can be discharged either by letting 𝑊 = V (if strong equality is known on ·𝑠) or assuming 𝐾 is a ring. (Contributed by Mario Carneiro, 5-Jul-2015.) |
⊢ 𝐹 = (Scalar‘𝐾) & ⊢ 𝐺 = (Scalar‘𝐿) & ⊢ (𝜑 → 𝑃 = (Base‘𝐹)) & ⊢ (𝜑 → 𝑃 = (Base‘𝐺)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑊)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ (𝜑 → (1r‘𝐾) = (1r‘𝐿)) & ⊢ (𝜑 → (1r‘𝐾) ∈ 𝑊) ⇒ ⊢ (𝜑 → (algSc‘𝐾) = (algSc‘𝐿)) | ||
Theorem | aspval2 20122 | The algebraic closure is the ring closure when the generating set is expanded to include all scalars. EDITORIAL : In light of this, is AlgSpan independently needed? (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ 𝐴 = (AlgSpan‘𝑊) & ⊢ 𝐶 = (algSc‘𝑊) & ⊢ 𝑅 = (mrCls‘(SubRing‘𝑊)) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (𝐴‘𝑆) = (𝑅‘(ran 𝐶 ∪ 𝑆))) | ||
Theorem | assamulgscmlem1 20123 | Lemma 1 for assamulgscm 20125 (induction base). (Contributed by AV, 26-Aug-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐺 = (mulGrp‘𝐹) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝐻 = (mulGrp‘𝑊) & ⊢ 𝐸 = (.g‘𝐻) ⇒ ⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → (0𝐸(𝐴 · 𝑋)) = ((0 ↑ 𝐴) · (0𝐸𝑋))) | ||
Theorem | assamulgscmlem2 20124 | Lemma for assamulgscm 20125 (induction step). (Contributed by AV, 26-Aug-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐺 = (mulGrp‘𝐹) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝐻 = (mulGrp‘𝑊) & ⊢ 𝐸 = (.g‘𝐻) ⇒ ⊢ (𝑦 ∈ ℕ0 → (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → ((𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋)) → ((𝑦 + 1)𝐸(𝐴 · 𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))))) | ||
Theorem | assamulgscm 20125 | Exponentiation of a scalar multiplication in an associative algebra: (𝑎 · 𝑋)↑𝑁 = (𝑎↑𝑁) × (𝑋↑𝑁). (Contributed by AV, 26-Aug-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐺 = (mulGrp‘𝐹) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝐻 = (mulGrp‘𝑊) & ⊢ 𝐸 = (.g‘𝐻) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ (𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉)) → (𝑁𝐸(𝐴 · 𝑋)) = ((𝑁 ↑ 𝐴) · (𝑁𝐸𝑋))) | ||
Syntax | cmps 20126 | Multivariate power series. |
class mPwSer | ||
Syntax | cmvr 20127 | Multivariate power series variables. |
class mVar | ||
Syntax | cmpl 20128 | Multivariate polynomials. |
class mPoly | ||
Syntax | cltb 20129 | Ordering on terms of a multivariate polynomial. |
class <bag | ||
Syntax | copws 20130 | Ordered set of power series. |
class ordPwSer | ||
Definition | df-psr 20131* | Define the algebra of power series over the index set 𝑖 and with coefficients from the ring 𝑟. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ mPwSer = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑m 𝑑) / 𝑏⦌({〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))〉, 〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))〉} ∪ {〈(Scalar‘ndx), 𝑟〉, 〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))〉, 〈(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))〉})) | ||
Definition | df-mvr 20132* | Define the generating elements of the power series algebra. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ mVar = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟))))) | ||
Definition | df-mpl 20133* | Define the subalgebra of the power series algebra generated by the variables; this is the polynomial algebra (the set of power series with finite degree). (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) |
⊢ mPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)})) | ||
Definition | df-ltbag 20134* | Define a well-order on the set of all finite bags from the index set 𝑖 given a wellordering 𝑟 of 𝑖. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ <bag = (𝑟 ∈ V, 𝑖 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∧ ∃𝑧 ∈ 𝑖 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))}) | ||
Definition | df-opsr 20135* | Define a total order on the set of all power series in 𝑠 from the index set 𝑖 given a wellordering 𝑟 of 𝑖 and a totally ordered base ring 𝑠. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ ordPwSer = (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ ⦋(𝑖 mPwSer 𝑠) / 𝑝⦌(𝑝 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉))) | ||
Theorem | reldmpsr 20136 | The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ Rel dom mPwSer | ||
Theorem | psrval 20137* | Value of the multivariate power series structure. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑂 = (TopOpen‘𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐵 = (𝐾 ↑m 𝐷)) & ⊢ ✚ = ( ∘f + ↾ (𝐵 × 𝐵)) & ⊢ × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥))))))) & ⊢ ∙ = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓)) & ⊢ (𝜑 → 𝐽 = (∏t‘(𝐷 × {𝑂}))) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑆 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), ✚ 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑅〉, 〈( ·𝑠 ‘ndx), ∙ 〉, 〈(TopSet‘ndx), 𝐽〉})) | ||
Theorem | psrvalstr 20138 | The multivariate power series structure is a function. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑅〉, 〈( ·𝑠 ‘ndx), · 〉, 〈(TopSet‘ndx), 𝐽〉}) Struct 〈1, 9〉 | ||
Theorem | psrbag 20139* | Elementhood in the set of finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝐹 ∈ 𝐷 ↔ (𝐹:𝐼⟶ℕ0 ∧ (◡𝐹 “ ℕ) ∈ Fin))) | ||
Theorem | psrbagf 20140* | A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐼⟶ℕ0) | ||
Theorem | snifpsrbag 20141* | A bag containing one element is a finite bag. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 8-Jul-2019.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 𝑁, 0)) ∈ 𝐷) | ||
Theorem | fczpsrbag 20142* | The constant function equal to zero is a finite bag. (Contributed by AV, 8-Jul-2019.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷) | ||
Theorem | psrbaglesupp 20143* | The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → (◡𝐺 “ ℕ) ⊆ (◡𝐹 “ ℕ)) | ||
Theorem | psrbaglecl 20144* | The set of finite bags is downward-closed. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → 𝐺 ∈ 𝐷) | ||
Theorem | psrbagaddcl 20145* | The sum of two finite bags is a finite bag. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) → (𝐹 ∘f + 𝐺) ∈ 𝐷) | ||
Theorem | psrbagcon 20146* | The analogue of the statement "0 ≤ 𝐺 ≤ 𝐹 implies 0 ≤ 𝐹 − 𝐺 ≤ 𝐹 " for finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → ((𝐹 ∘f − 𝐺) ∈ 𝐷 ∧ (𝐹 ∘f − 𝐺) ∘r ≤ 𝐹)) | ||
Theorem | psrbaglefi 20147* | There are finitely many bags dominated by a given bag. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 25-Jan-2015.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ Fin) | ||
Theorem | psrbagconcl 20148* | The complement of a bag is a bag. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → (𝐹 ∘f − 𝑋) ∈ 𝑆) | ||
Theorem | psrbagconf1o 20149* | Bag complementation is a bijection on the set of bags dominated by a given bag 𝐹. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → (𝑥 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑥)):𝑆–1-1-onto→𝑆) | ||
Theorem | gsumbagdiaglem 20150* | Lemma for gsumbagdiag 20151. (Contributed by Mario Carneiro, 5-Jan-2015.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → (𝑌 ∈ 𝑆 ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑌)})) | ||
Theorem | gsumbagdiag 20151* | Two-dimensional commutation of a group sum over a "triangular" region. fsum0diag 15127 analogue for finite bags. (Contributed by Mario Carneiro, 5-Jan-2015.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝑆, 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)) = (𝐺 Σg (𝑘 ∈ 𝑆, 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑘)} ↦ 𝑋))) | ||
Theorem | psrass1lem 20152* | A group sum commutation used by psrass1 20180. (Contributed by Mario Carneiro, 5-Jan-2015.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑋 ∈ 𝐵) & ⊢ (𝑘 = (𝑛 ∘f − 𝑗) → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋))))) | ||
Theorem | psrbas 20153* | The base set of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 8-Jul-2019.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐵 = (𝐾 ↑m 𝐷)) | ||
Theorem | psrelbas 20154* | An element of the set of power series is a function on the coefficients. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋:𝐷⟶𝐾) | ||
Theorem | psrelbasfun 20155 | An element of the set of power series is a function. (Contributed by AV, 17-Jul-2019.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝑋 ∈ 𝐵 → Fun 𝑋) | ||
Theorem | psrplusg 20156 | The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ + = (+g‘𝑅) & ⊢ ✚ = (+g‘𝑆) ⇒ ⊢ ✚ = ( ∘f + ↾ (𝐵 × 𝐵)) | ||
Theorem | psradd 20157 | The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ + = (+g‘𝑅) & ⊢ ✚ = (+g‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ✚ 𝑌) = (𝑋 ∘f + 𝑌)) | ||
Theorem | psraddcl 20158 | Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵) | ||
Theorem | psrmulr 20159* | The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 2-Mar-2024.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ · = (.r‘𝑅) & ⊢ ∙ = (.r‘𝑆) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ⇒ ⊢ ∙ = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥))))))) | ||
Theorem | psrmulfval 20160* | The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ · = (.r‘𝑅) & ⊢ ∙ = (.r‘𝑆) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∙ 𝐺) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝐹‘𝑥) · (𝐺‘(𝑘 ∘f − 𝑥))))))) | ||
Theorem | psrmulval 20161* | The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ · = (.r‘𝑅) & ⊢ ∙ = (.r‘𝑆) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → ((𝐹 ∙ 𝐺)‘𝑋) = (𝑅 Σg (𝑘 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑋} ↦ ((𝐹‘𝑘) · (𝐺‘(𝑋 ∘f − 𝑘)))))) | ||
Theorem | psrmulcllem 20162* | Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵) | ||
Theorem | psrmulcl 20163 | Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵) | ||
Theorem | psrsca 20164 | The scalar field of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑅 = (Scalar‘𝑆)) | ||
Theorem | psrvscafval 20165* | The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ ∙ = ( ·𝑠 ‘𝑆) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ · = (.r‘𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ⇒ ⊢ ∙ = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓)) | ||
Theorem | psrvsca 20166* | 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 20167* | 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 20168 | Closure of the power series scalar multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 𝐹) ∈ 𝐵) | ||
Theorem | psr0cl 20169* | 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 20170* | 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 20171* | 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 20172* | 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 20173 | The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Grp) ⇒ ⊢ (𝜑 → 𝑆 ∈ Grp) | ||
Theorem | psr0 20174* | 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 20175* | 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 20176 | The ring of power series is a left module. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑆 ∈ LMod) | ||
Theorem | psr1cl 20177* | 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 20178* | 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 20179* | 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 20180* | Associative identity for the ring of power series. (Contributed by Mario Carneiro, 5-Jan-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ × = (.r‘𝑆) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 × 𝑌) × 𝑍) = (𝑋 × (𝑌 × 𝑍))) | ||
Theorem | psrdi 20181* | 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 20182* | 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 20183* | Associative identity for the ring of power series. Part of psrass23 20185 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 20184* | 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 20185* | 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 20186 | The ring of power series is a ring. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑆 ∈ Ring) | ||
Theorem | psr1 20187* | 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 20188 | The ring of power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝑆 ∈ CRing) | ||
Theorem | psrassa 20189 | The ring of power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝑆 ∈ AssAlg) | ||
Theorem | resspsrbas 20190 | 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 20191 | 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 20192 | 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 20193 | 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 20194 | 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 20195* | 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 20196* | 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 20197* | 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 20198* | 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 20199 | 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 20200 | 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→𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |