HomeTheorem List (p. 215 of 479)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 215 of 479) | < 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-30166) |
Hilbert Space Explorer
(30167-31689) |
Users' Mathboxes
(31690-47842) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | uvcendim 21401 | In a nonzero ring, the number of unit vectors of a free module corresponds to the dimension of the free module. (Contributed by AV, 10-Mar-2019.) |
| β’ π = (π unitVec πΌ) β β’ ((π β NzRing β§ πΌ β π) β πΌ β ran π) | ||
| Theorem | frlmisfrlm 21402 | A free module is isomorphic to a free module over the same (nonzero) ring, with the same cardinality. (Contributed by AV, 10-Mar-2019.) |
| β’ ((π β NzRing β§ πΌ β π β§ πΌ β π½) β (π freeLMod πΌ) βπ (π freeLMod π½)) | ||
| Theorem | frlmiscvec 21403 | Every free module is isomorphic to the free module of "column vectors" of the same dimension over the same (nonzero) ring. (Contributed by AV, 10-Mar-2019.) |
| β’ ((π β NzRing β§ πΌ β π) β (π freeLMod πΌ) βπ (π freeLMod (πΌ Γ {β }))) | ||
| Syntax | casa 21404 | Associative algebra. |
| class AssAlg | ||
| Syntax | casp 21405 | Algebraic span function. |
| class AlgSpan | ||
| Syntax | cascl 21406 | Class of algebra scalar injection function. |
| class algSc | ||
| Definition | df-assa 21407* | Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a ring, coupled with a multiplicative internal operation on the vectors of the module that is associative and distributive for the additive structure of the left-module (so giving the vectors a ring structure) and that is also bilinear under the scalar product. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by SN, 2-Mar-2025.) |
| β’ AssAlg = {π€ β (LMod β© Ring) β£ [(Scalarβπ€) / π]βπ β (Baseβπ)βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ€)[( Β·π βπ€) / π ][(.rβπ€) / π‘](((ππ π₯)π‘π¦) = (ππ (π₯π‘π¦)) β§ (π₯π‘(ππ π¦)) = (ππ (π₯π‘π¦)))} | ||
| Definition | df-asp 21408* | Define the algebraic span of a set of vectors in an algebra. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| β’ AlgSpan = (π€ β AssAlg β¦ (π β π« (Baseβπ€) β¦ β© {π‘ β ((SubRingβπ€) β© (LSubSpβπ€)) β£ π β π‘})) | ||
| Definition | df-ascl 21409* | Every unital algebra contains a canonical homomorphic image of its ring of scalars as scalar multiples of the unity element. This names the homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015.) |
| β’ algSc = (π€ β V β¦ (π₯ β (Baseβ(Scalarβπ€)) β¦ (π₯( Β·π βπ€)(1rβπ€)))) | ||
| Theorem | isassa 21410* | The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by SN, 2-Mar-2025.) |
| β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) β β’ (π β AssAlg β ((π β LMod β§ π β Ring) β§ βπ β π΅ βπ₯ β π βπ¦ β π (((π Β· π₯) Γ π¦) = (π Β· (π₯ Γ π¦)) β§ (π₯ Γ (π Β· π¦)) = (π Β· (π₯ Γ π¦))))) | ||
| Theorem | assalem 21411 | The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
| β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) β β’ ((π β AssAlg β§ (π΄ β π΅ β§ π β π β§ π β π)) β (((π΄ Β· π) Γ π) = (π΄ Β· (π Γ π)) β§ (π Γ (π΄ Β· π)) = (π΄ Β· (π Γ π)))) | ||
| Theorem | assaass 21412 | Left-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
| β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) β β’ ((π β AssAlg β§ (π΄ β π΅ β§ π β π β§ π β π)) β ((π΄ Β· π) Γ π) = (π΄ Β· (π Γ π))) | ||
| Theorem | assaassr 21413 | Right-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
| β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) β β’ ((π β AssAlg β§ (π΄ β π΅ β§ π β π β§ π β π)) β (π Γ (π΄ Β· π)) = (π΄ Β· (π Γ π))) | ||
| Theorem | assalmod 21414 | An associative algebra is a left module. (Contributed by Mario Carneiro, 5-Dec-2014.) |
| β’ (π β AssAlg β π β LMod) | ||
| Theorem | assaring 21415 | An associative algebra is a ring. (Contributed by Mario Carneiro, 5-Dec-2014.) |
| β’ (π β AssAlg β π β Ring) | ||
| Theorem | assasca 21416 | The scalars of an associative algebra form a ring. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by SN, 2-Mar-2025.) |
| β’ πΉ = (Scalarβπ) β β’ (π β AssAlg β πΉ β Ring) | ||
| Theorem | assa2ass 21417 | Left- and right-associative property of an associative algebra. Notice that the scalars are commuted! (Contributed by AV, 14-Aug-2019.) |
| β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ β = (.rβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) β β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β ((π΄ Β· π) Γ (πΆ Β· π)) = ((πΆ β π΄) Β· (π Γ π))) | ||
| Theorem | isassad 21418* | Sufficient condition for being an associative algebra. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by SN, 2-Mar-2025.) |
| β’ (π β π = (Baseβπ)) & β’ (π β πΉ = (Scalarβπ)) & β’ (π β π΅ = (BaseβπΉ)) & β’ (π β Β· = ( Β·π βπ)) & β’ (π β Γ = (.rβπ)) & β’ (π β π β LMod) & β’ (π β π β Ring) & β’ ((π β§ (π β π΅ β§ π₯ β π β§ π¦ β π)) β ((π Β· π₯) Γ π¦) = (π Β· (π₯ Γ π¦))) & β’ ((π β§ (π β π΅ β§ π₯ β π β§ π¦ β π)) β (π₯ Γ (π Β· π¦)) = (π Β· (π₯ Γ π¦))) β β’ (π β π β AssAlg) | ||
| Theorem | issubassa3 21419 | A subring that is also a subspace is a subalgebra. The key theorem is islss3 20569. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| β’ π = (π βΎs π΄) & β’ πΏ = (LSubSpβπ) β β’ ((π β AssAlg β§ (π΄ β (SubRingβπ) β§ π΄ β πΏ)) β π β AssAlg) | ||
| Theorem | issubassa 21420 | The subalgebras of an associative algebra are exactly the subrings (under the ring multiplication) that are simultaneously subspaces (under the scalar multiplication from the vector space). (Contributed by Mario Carneiro, 7-Jan-2015.) |
| β’ π = (π βΎs π΄) & β’ πΏ = (LSubSpβπ) & β’ π = (Baseβπ) & β’ 1 = (1rβπ) β β’ ((π β AssAlg β§ 1 β π΄ β§ π΄ β π) β (π β AssAlg β (π΄ β (SubRingβπ) β§ π΄ β πΏ))) | ||
| Theorem | sraassab 21421 | A subring algebra is an associative algebra if and only if the subring is included in the ring's center. (Contributed by SN, 21-Mar-2025.) |
| β’ π΄ = ((subringAlg βπ)βπ) & β’ π = (Cntrβ(mulGrpβπ)) & β’ (π β π β Ring) & β’ (π β π β (SubRingβπ)) β β’ (π β (π΄ β AssAlg β π β π)) | ||
| Theorem | sraassa 21422 | The subring algebra over a commutative ring is an associative algebra. (Contributed by Mario Carneiro, 6-Oct-2015.) (Proof shortened by SN, 21-Mar-2025.) |
| β’ π΄ = ((subringAlg βπ)βπ) β β’ ((π β CRing β§ π β (SubRingβπ)) β π΄ β AssAlg) | ||
| Theorem | sraassaOLD 21423 | Obsolete version of sraassa 21422 as of 21-Mar-2025. (Contributed by Mario Carneiro, 6-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| β’ π΄ = ((subringAlg βπ)βπ) β β’ ((π β CRing β§ π β (SubRingβπ)) β π΄ β AssAlg) | ||
| Theorem | rlmassa 21424 | The ring module over a commutative ring is an associative algebra. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| β’ (π β CRing β (ringLModβπ ) β AssAlg) | ||
| Theorem | assapropd 21425* | If two structures have the same components (properties), one is an associative algebra iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.) |
| β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) & β’ (π β πΉ = (ScalarβπΎ)) & β’ (π β πΉ = (ScalarβπΏ)) & β’ π = (BaseβπΉ) & β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π βπΎ)π¦) = (π₯( Β·π βπΏ)π¦)) β β’ (π β (πΎ β AssAlg β πΏ β AssAlg)) | ||
| Theorem | aspval 21426* | Value of the algebraic closure operation inside an associative algebra. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| β’ π΄ = (AlgSpanβπ) & β’ π = (Baseβπ) & β’ πΏ = (LSubSpβπ) β β’ ((π β AssAlg β§ π β π) β (π΄βπ) = β© {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘}) | ||
| Theorem | asplss 21427 | The algebraic span of a set of vectors is a vector subspace. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| β’ π΄ = (AlgSpanβπ) & β’ π = (Baseβπ) & β’ πΏ = (LSubSpβπ) β β’ ((π β AssAlg β§ π β π) β (π΄βπ) β πΏ) | ||
| Theorem | aspid 21428 | The algebraic span of a subalgebra is itself. (spanid 30595 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
| β’ π΄ = (AlgSpanβπ) & β’ π = (Baseβπ) & β’ πΏ = (LSubSpβπ) β β’ ((π β AssAlg β§ π β (SubRingβπ) β§ π β πΏ) β (π΄βπ) = π) | ||
| Theorem | aspsubrg 21429 | 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 21430 | Span preserves subset ordering. (spanss 30596 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
| β’ π΄ = (AlgSpanβπ) & β’ π = (Baseβπ) β β’ ((π β AssAlg β§ π β π β§ π β π) β (π΄βπ) β (π΄βπ)) | ||
| Theorem | aspssid 21431 | A set of vectors is a subset of its span. (spanss2 30593 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
| β’ π΄ = (AlgSpanβπ) & β’ π = (Baseβπ) β β’ ((π β AssAlg β§ π β π) β π β (π΄βπ)) | ||
| Theorem | asclfval 21432* | Function value of the algebraic scalars function. (Contributed by Mario Carneiro, 8-Mar-2015.) |
| β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) β β’ π΄ = (π₯ β πΎ β¦ (π₯ Β· 1 )) | ||
| Theorem | asclval 21433 | Value of a mapped algebra scalar. (Contributed by Mario Carneiro, 8-Mar-2015.) |
| β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) β β’ (π β πΎ β (π΄βπ) = (π Β· 1 )) | ||
| Theorem | asclfn 21434 | Unconditional functionality of the algebra scalars function. (Contributed by Mario Carneiro, 9-Mar-2015.) |
| β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ π΄ Fn πΎ | ||
| Theorem | asclf 21435 | 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 21436 | The algebra scalars function is a group homomorphism. (Contributed by Mario Carneiro, 4-Jul-2015.) |
| β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β Ring) & β’ (π β π β LMod) β β’ (π β π΄ β (πΉ GrpHom π)) | ||
| Theorem | ascl0 21437 | 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 21438 | 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 21439 | 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 21440 | 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 21441 | 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 21442 | 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 21443 | The scalar injection is a ring homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015.) |
| β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) β β’ (π β AssAlg β π΄ β (πΉ RingHom π)) | ||
| Theorem | rnascl 21444 | 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 21445 | 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 21446 | 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 21447 | (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 21448 | 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 21449 | The injection of scalars is invariant between subalgebras and superalgebras. (Contributed by Mario Carneiro, 9-Mar-2015.) |
| β’ π΄ = (algScβπ) & β’ π = (π βΎs π) β β’ (π β (SubRingβπ) β π΄ = (algScβπ)) | ||
| Theorem | asclpropd 21450* | 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 21451 | 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 21452 | Lemma 1 for assamulgscm 21454 (induction base). (Contributed by AV, 26-Aug-2019.) |
| β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ πΊ = (mulGrpβπΉ) & β’ β = (.gβπΊ) & β’ π» = (mulGrpβπ) & β’ πΈ = (.gβπ») β β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (0πΈ(π΄ Β· π)) = ((0 β π΄) Β· (0πΈπ))) | ||
| Theorem | assamulgscmlem2 21453 | Lemma for assamulgscm 21454 (induction step). (Contributed by AV, 26-Aug-2019.) |
| β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ πΊ = (mulGrpβπΉ) & β’ β = (.gβπΊ) & β’ π» = (mulGrpβπ) & β’ πΈ = (.gβπ») β β’ (π¦ β β0 β (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β ((π¦πΈ(π΄ Β· π)) = ((π¦ β π΄) Β· (π¦πΈπ)) β ((π¦ + 1)πΈ(π΄ Β· π)) = (((π¦ + 1) β π΄) Β· ((π¦ + 1)πΈπ))))) | ||
| Theorem | assamulgscm 21454 | 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 21455 | The β€-module operation turns a ring into an associative algebra over β€. Also see zlmlmod 21075. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (β€ModβπΊ) β β’ (πΊ β Ring β π β AssAlg) | ||
| Syntax | cmps 21456 | Multivariate power series. |
| class mPwSer | ||
| Syntax | cmvr 21457 | Multivariate power series variables. |
| class mVar | ||
| Syntax | cmpl 21458 | Multivariate polynomials. |
| class mPoly | ||
| Syntax | cltb 21459 | Ordering on terms of a multivariate polynomial. |
| class <bag | ||
| Syntax | copws 21460 | Ordered set of power series. |
| class ordPwSer | ||
| Definition | df-psr 21461* | 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 21462* | 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 21463* | 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 21464* | 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 21465* | 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 21466 | The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| β’ Rel dom mPwSer | ||
| Theorem | psrval 21467* | 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 21468 | 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 21469* | Elementhood in the set of finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.) |
| β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ (πΌ β π β (πΉ β π· β (πΉ:πΌβΆβ0 β§ (β‘πΉ β β) β Fin))) | ||
| Theorem | psrbagf 21470* | 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 21471* | Obsolete version of psrbag 21469 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 21472* | 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 21473* | Obsolete version of psrbagfsupp 21472 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 21474* | 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 21475* | The constant function equal to zero is a finite bag. (Contributed by AV, 8-Jul-2019.) |
| β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ (πΌ β π β (π₯ β πΌ β¦ 0) β π·) | ||
| Theorem | psrbaglesupp 21476* | 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 21477* | Obsolete version of psrbaglesupp 21476 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 21478* | 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 21479* | Obsolete version of psrbaglecl 21478 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 21480* | 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 21481* | Obsolete version of psrbagaddcl 21480 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 21482* | 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 21483* | Obsolete version of psrbagcon 21482 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 21484* | 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 21485* | Obsolete version of psrbaglefi 21484 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 21486* | 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 21487* | Obsolete version of psrbagconcl 21486 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 21488* | 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 21489* | Obsolete version of psrbagconf1o 21488 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 21490* | Obsolete version of gsumbagdiaglem 21493 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 21491* | Obsolete version of gsumbagdiag 21494 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 21492* | Obsolete version of psrass1lem 21495 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 21493* | Lemma for gsumbagdiag 21494. (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 21494* | Two-dimensional commutation of a group sum over a "triangular" region. fsum0diag 15722 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 21495* | A group sum commutation used by psrass1 21524. (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 21496* | 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 21497* | 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 21498 | An element of the set of power series is a function. (Contributed by AV, 17-Jul-2019.) |
| β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) β β’ (π β π΅ β Fun π) | ||
| Theorem | psrplusg 21499 | 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 21500 | The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
| β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ ) & β’ β = (+gβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β π) = (π βf + π)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |