Home | Metamath
Proof Explorer Theorem List (p. 213 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | aspid 21201 | The algebraic span of a subalgebra is itself. (spanid 30075 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π΄ = (AlgSpanβπ) & β’ π = (Baseβπ) & β’ πΏ = (LSubSpβπ) β β’ ((π β AssAlg β§ π β (SubRingβπ) β§ π β πΏ) β (π΄βπ) = π) | ||
Theorem | aspsubrg 21202 | The algebraic span of a set of vectors is a subring of the algebra. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π΄ = (AlgSpanβπ) & β’ π = (Baseβπ) β β’ ((π β AssAlg β§ π β π) β (π΄βπ) β (SubRingβπ)) | ||
Theorem | aspss 21203 | Span preserves subset ordering. (spanss 30076 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π΄ = (AlgSpanβπ) & β’ π = (Baseβπ) β β’ ((π β AssAlg β§ π β π β§ π β π) β (π΄βπ) β (π΄βπ)) | ||
Theorem | aspssid 21204 | A set of vectors is a subset of its span. (spanss2 30073 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π΄ = (AlgSpanβπ) & β’ π = (Baseβπ) β β’ ((π β AssAlg β§ π β π) β π β (π΄βπ)) | ||
Theorem | asclfval 21205* | Function value of the algebraic scalars function. (Contributed by Mario Carneiro, 8-Mar-2015.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) β β’ π΄ = (π₯ β πΎ β¦ (π₯ Β· 1 )) | ||
Theorem | asclval 21206 | Value of a mapped algebra scalar. (Contributed by Mario Carneiro, 8-Mar-2015.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) β β’ (π β πΎ β (π΄βπ) = (π Β· 1 )) | ||
Theorem | asclfn 21207 | Unconditional functionality of the algebra scalars function. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ π΄ Fn πΎ | ||
Theorem | asclf 21208 | 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 21209 | The algebra scalars function is a group homomorphism. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β Ring) & β’ (π β π β LMod) β β’ (π β π΄ β (πΉ GrpHom π)) | ||
Theorem | ascl0 21210 | 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 | ascl1 21211 | The scalar 1 embedded into a left module corresponds to the 1 of the left module if the left module is also a ring. (Contributed by AV, 31-Jul-2019.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β LMod) & β’ (π β π β Ring) β β’ (π β (π΄β(1rβπΉ)) = (1rβπ)) | ||
Theorem | asclmul1 21212 | 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 21213 | 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 21214 | 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 | asclinvg 21215 | 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 21216 | The scalar injection is a ring homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) β β’ (π β AssAlg β π΄ β (πΉ RingHom π)) | ||
Theorem | rnascl 21217 | 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 21218 | 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 21219 | 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 21220 | (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 21221 | 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 21222 | The injection of scalars is invariant between subalgebras and superalgebras. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ π΄ = (algScβπ) & β’ π = (π βΎs π) β β’ (π β (SubRingβπ) β π΄ = (algScβπ)) | ||
Theorem | asclpropd 21223* | 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 21224 | 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 21225 | Lemma 1 for assamulgscm 21227 (induction base). (Contributed by AV, 26-Aug-2019.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ πΊ = (mulGrpβπΉ) & β’ β = (.gβπΊ) & β’ π» = (mulGrpβπ) & β’ πΈ = (.gβπ») β β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (0πΈ(π΄ Β· π)) = ((0 β π΄) Β· (0πΈπ))) | ||
Theorem | assamulgscmlem2 21226 | Lemma for assamulgscm 21227 (induction step). (Contributed by AV, 26-Aug-2019.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ πΊ = (mulGrpβπΉ) & β’ β = (.gβπΊ) & β’ π» = (mulGrpβπ) & β’ πΈ = (.gβπ») β β’ (π¦ β β0 β (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β ((π¦πΈ(π΄ Β· π)) = ((π¦ β π΄) Β· (π¦πΈπ)) β ((π¦ + 1)πΈ(π΄ Β· π)) = (((π¦ + 1) β π΄) Β· ((π¦ + 1)πΈπ))))) | ||
Theorem | assamulgscm 21227 | Exponentiation of a scalar multiplication in an associative algebra: (π Β· π)βπ = (πβπ) Γ (πβπ). (Contributed by AV, 26-Aug-2019.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ πΊ = (mulGrpβπΉ) & β’ β = (.gβπΊ) & β’ π» = (mulGrpβπ) & β’ πΈ = (.gβπ») β β’ ((π β AssAlg β§ (π β β0 β§ π΄ β π΅ β§ π β π)) β (ππΈ(π΄ Β· π)) = ((π β π΄) Β· (ππΈπ))) | ||
Theorem | zlmassa 21228 | The β€-module operation turns a ring into an associative algebra over β€. Also see zlmlmod 20850. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (β€ModβπΊ) β β’ (πΊ β Ring β π β AssAlg) | ||
Syntax | cmps 21229 | Multivariate power series. |
class mPwSer | ||
Syntax | cmvr 21230 | Multivariate power series variables. |
class mVar | ||
Syntax | cmpl 21231 | Multivariate polynomials. |
class mPoly | ||
Syntax | cltb 21232 | Ordering on terms of a multivariate polynomial. |
class <bag | ||
Syntax | copws 21233 | Ordered set of power series. |
class ordPwSer | ||
Definition | df-psr 21234* | 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 21235* | 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 21236* | 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 21237* | 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 21238* | 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 21239 | The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ Rel dom mPwSer | ||
Theorem | psrval 21240* | 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 21241 | 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 21242* | Elementhood in the set of finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ (πΌ β π β (πΉ β π· β (πΉ:πΌβΆβ0 β§ (β‘πΉ β β) β Fin))) | ||
Theorem | psrbagf 21243* | A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 30-Jul-2024.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ (πΉ β π· β πΉ:πΌβΆβ0) | ||
Theorem | psrbagfOLD 21244* | Obsolete version of psrbag 21242 as of 6-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ ((πΌ β π β§ πΉ β π·) β πΉ:πΌβΆβ0) | ||
Theorem | psrbagfsupp 21245* | Finite bags have finite support. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ (πΉ β π· β πΉ finSupp 0) | ||
Theorem | psrbagfsuppOLD 21246* | Obsolete version of psrbagfsupp 21245 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ ((π β π· β§ πΌ β π) β π finSupp 0) | ||
Theorem | snifpsrbag 21247* | 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 21248* | The constant function equal to zero is a finite bag. (Contributed by AV, 8-Jul-2019.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ (πΌ β π β (π₯ β πΌ β¦ 0) β π·) | ||
Theorem | psrbaglesupp 21249* | The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β (β‘πΊ β β) β (β‘πΉ β β)) | ||
Theorem | psrbaglesuppOLD 21250* | Obsolete version of psrbaglesupp 21249 as of 5-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (β‘πΊ β β) β (β‘πΉ β β)) | ||
Theorem | psrbaglecl 21251* | The set of finite bags is downward-closed. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β πΊ β π·) | ||
Theorem | psrbagleclOLD 21252* | Obsolete version of psrbaglecl 21251 as of 5-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β πΊ β π·) | ||
Theorem | psrbagaddcl 21253* | The sum of two finite bags is a finite bag. (Contributed by Mario Carneiro, 9-Jan-2015.) Shorten proof and remove a sethood antecedent. (Revised by SN, 7-Aug-2024.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ ((πΉ β π· β§ πΊ β π·) β (πΉ βf + πΊ) β π·) | ||
Theorem | psrbagaddclOLD 21254* | Obsolete version of psrbagaddcl 21253 as of 7-Aug-2024. (Contributed by Mario Carneiro, 9-Jan-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ ((πΌ β π β§ πΉ β π· β§ πΊ β π·) β (πΉ βf + πΊ) β π·) | ||
Theorem | psrbagcon 21255* | The analogue of the statement "0 β€ πΊ β€ πΉ implies 0 β€ πΉ β πΊ β€ πΉ " for finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β ((πΉ βf β πΊ) β π· β§ (πΉ βf β πΊ) βr β€ πΉ)) | ||
Theorem | psrbagconOLD 21256* | Obsolete version of psrbagcon 21255 as of 5-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β ((πΉ βf β πΊ) β π· β§ (πΉ βf β πΊ) βr β€ πΉ)) | ||
Theorem | psrbaglefi 21257* | There are finitely many bags dominated by a given bag. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 25-Jan-2015.) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ (πΉ β π· β {π¦ β π· β£ π¦ βr β€ πΉ} β Fin) | ||
Theorem | psrbaglefiOLD 21258* | Obsolete version of psrbaglefi 21257 as of 6-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 25-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ ((πΌ β π β§ πΉ β π·) β {π¦ β π· β£ π¦ βr β€ πΉ} β Fin) | ||
Theorem | psrbagconcl 21259* | The complement of a bag is a bag. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 6-Aug-2024.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π = {π¦ β π· β£ π¦ βr β€ πΉ} β β’ ((πΉ β π· β§ π β π) β (πΉ βf β π) β π) | ||
Theorem | psrbagconclOLD 21260* | Obsolete version of psrbagconcl 21259 as of 6-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π = {π¦ β π· β£ π¦ βr β€ πΉ} β β’ ((πΌ β π β§ πΉ β π· β§ π β π) β (πΉ βf β π) β π) | ||
Theorem | psrbagconf1o 21261* | Bag complementation is a bijection on the set of bags dominated by a given bag πΉ. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 6-Aug-2024.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π = {π¦ β π· β£ π¦ βr β€ πΉ} β β’ (πΉ β π· β (π₯ β π β¦ (πΉ βf β π₯)):πβ1-1-ontoβπ) | ||
Theorem | psrbagconf1oOLD 21262* | Obsolete version of psrbagconf1o 21261 as of 6-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π = {π¦ β π· β£ π¦ βr β€ πΉ} β β’ ((πΌ β π β§ πΉ β π·) β (π₯ β π β¦ (πΉ βf β π₯)):πβ1-1-ontoβπ) | ||
Theorem | gsumbagdiaglemOLD 21263* | Obsolete version of gsumbagdiaglem 21266 as of 6-Aug-2024. (Contributed by Mario Carneiro, 5-Jan-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π = {π¦ β π· β£ π¦ βr β€ πΉ} & β’ (π β πΌ β π) & β’ (π β πΉ β π·) β β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) | ||
Theorem | gsumbagdiagOLD 21264* | Obsolete version of gsumbagdiag 21267 as of 6-Aug-2024. (Contributed by Mario Carneiro, 5-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π = {π¦ β π· β£ π¦ βr β€ πΉ} & β’ (π β πΌ β π) & β’ (π β πΉ β π·) & β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π β π΅) β β’ (π β (πΊ Ξ£g (π β π, π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π)) = (πΊ Ξ£g (π β π, π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π))) | ||
Theorem | psrass1lemOLD 21265* | Obsolete version of psrass1lem 21268 as of 7-Aug-2024. (Contributed by Mario Carneiro, 5-Jan-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π = {π¦ β π· β£ π¦ βr β€ πΉ} & β’ (π β πΌ β π) & β’ (π β πΉ β π·) & β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π β π΅) & β’ (π = (π βf β π) β π = π) β β’ (π β (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π)))) = (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π))))) | ||
Theorem | gsumbagdiaglem 21266* | Lemma for gsumbagdiag 21267. (Contributed by Mario Carneiro, 5-Jan-2015.) Remove a sethood hypothesis. (Revised by SN, 6-Aug-2024.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π = {π¦ β π· β£ π¦ βr β€ πΉ} & β’ (π β πΉ β π·) β β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) | ||
Theorem | gsumbagdiag 21267* | Two-dimensional commutation of a group sum over a "triangular" region. fsum0diag 15597 analogue for finite bags. (Contributed by Mario Carneiro, 5-Jan-2015.) Remove a sethood hypothesis. (Revised by SN, 6-Aug-2024.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π = {π¦ β π· β£ π¦ βr β€ πΉ} & β’ (π β πΉ β π·) & β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π β π΅) β β’ (π β (πΊ Ξ£g (π β π, π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π)) = (πΊ Ξ£g (π β π, π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π))) | ||
Theorem | psrass1lem 21268* | A group sum commutation used by psrass1 21296. (Contributed by Mario Carneiro, 5-Jan-2015.) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π = {π¦ β π· β£ π¦ βr β€ πΉ} & β’ (π β πΉ β π·) & β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π β π΅) & β’ (π = (π βf β π) β π = π) β β’ (π β (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ π)))) = (πΊ Ξ£g (π β π β¦ (πΊ Ξ£g (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β¦ π))))) | ||
Theorem | psrbas 21269* | 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 21270* | 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 21271 | An element of the set of power series is a function. (Contributed by AV, 17-Jul-2019.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) β β’ (π β π΅ β Fun π) | ||
Theorem | psrplusg 21272 | 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 21273 | The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ ) & β’ β = (+gβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β π) = (π βf + π)) | ||
Theorem | psraddcl 21274 | Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β π β Grp) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π + π) β π΅) | ||
Theorem | psrmulr 21275* | 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 21276* | 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 21277* | 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 21278* | Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ (π β (π Β· π) β π΅) | ||
Theorem | psrmulcl 21279 | Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π Β· π) β π΅) | ||
Theorem | psrsca 21280 | The scalar field of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β π) β β’ (π β π = (Scalarβπ)) | ||
Theorem | psrvscafval 21281* | The scalar 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-Nov-2024.) |
β’ π = (πΌ mPwSer π ) & β’ β = ( Β·π βπ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} β β’ β = (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π)) | ||
Theorem | psrvsca 21282* | 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 21283* | 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 21284 | Closure of the power series scalar multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β Ring) & β’ (π β π β πΎ) & β’ (π β πΉ β π΅) β β’ (π β (π Β· πΉ) β π΅) | ||
Theorem | psr0cl 21285* | 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 21286* | 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 21287* | 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 21288* | 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 21289 | The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Grp) β β’ (π β π β Grp) | ||
Theorem | psr0 21290* | 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 21291* | 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 21292 | The ring of power series is a left module. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) β β’ (π β π β LMod) | ||
Theorem | psr1cl 21293* | 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 21294* | 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 21295* | 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 21296* | Associative identity for the ring of power series. (Contributed by Mario Carneiro, 5-Jan-2015.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ Γ = (.rβπ) & β’ π΅ = (Baseβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π Γ π) Γ π) = (π Γ (π Γ π))) | ||
Theorem | psrdi 21297* | 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 21298* | 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 21299* | Associative identity for the ring of power series. Part of psrass23 21301 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 21300* | Commutative law for the ring of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ Γ = (.rβπ) & β’ π΅ = (Baseβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β CRing) β β’ (π β (π Γ π) = (π Γ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |