![]() |
Metamath
Proof Explorer Theorem List (p. 219 of 485) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30800) |
![]() (30801-32323) |
![]() (32324-48421) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | casa 21801 | Associative algebra. |
class AssAlg | ||
Syntax | casp 21802 | Algebraic span function. |
class AlgSpan | ||
Syntax | cascl 21803 | Class of algebra scalar injection function. |
class algSc | ||
Definition | df-assa 21804* | 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 21805* | 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 21806* | 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 21807* | 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 21808 | The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌)))) | ||
Theorem | assaass 21809 | Left-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌))) | ||
Theorem | assaassr 21810 | Right-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌))) | ||
Theorem | assalmod 21811 | An associative algebra is a left module. (Contributed by Mario Carneiro, 5-Dec-2014.) |
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) | ||
Theorem | assaring 21812 | An associative algebra is a ring. (Contributed by Mario Carneiro, 5-Dec-2014.) |
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) | ||
Theorem | assasca 21813 | 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 21814 | 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 21815* | 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 21816 | A subring that is also a subspace is a subalgebra. The key theorem is islss3 20855. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝑆 = (𝑊 ↾s 𝐴) & ⊢ 𝐿 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝑆 ∈ AssAlg) | ||
Theorem | issubassa 21817 | 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 21818 | 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 21819 | 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 21820 | Obsolete version of sraassa 21819 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 21821 | The ring module over a commutative ring is an associative algebra. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ (𝑅 ∈ CRing → (ringLMod‘𝑅) ∈ AssAlg) | ||
Theorem | assapropd 21822* | 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 21823* | Value of the algebraic closure operation inside an associative algebra. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝐴 = (AlgSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (𝐴‘𝑆) = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) | ||
Theorem | asplss 21824 | 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 21825 | The algebraic span of a subalgebra is itself. (spanid 31229 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝐴 = (AlgSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊) ∧ 𝑆 ∈ 𝐿) → (𝐴‘𝑆) = 𝑆) | ||
Theorem | aspsubrg 21826 | 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 21827 | Span preserves subset ordering. (spanss 31230 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝐴 = (AlgSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆) → (𝐴‘𝑇) ⊆ (𝐴‘𝑆)) | ||
Theorem | aspssid 21828 | A set of vectors is a subset of its span. (spanss2 31227 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝐴 = (AlgSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ (𝐴‘𝑆)) | ||
Theorem | asclfval 21829* | Function value of the algebraic scalars function. (Contributed by Mario Carneiro, 8-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 1 = (1r‘𝑊) ⇒ ⊢ 𝐴 = (𝑥 ∈ 𝐾 ↦ (𝑥 · 1 )) | ||
Theorem | asclval 21830 | Value of a mapped algebra scalar. (Contributed by Mario Carneiro, 8-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 1 = (1r‘𝑊) ⇒ ⊢ (𝑋 ∈ 𝐾 → (𝐴‘𝑋) = (𝑋 · 1 )) | ||
Theorem | asclfn 21831 | Unconditional functionality of the algebra scalars function. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ 𝐴 Fn 𝐾 | ||
Theorem | asclf 21832 | 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 21833 | The algebra scalars function is a group homomorphism. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ Ring) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐹 GrpHom 𝑊)) | ||
Theorem | ascl0 21834 | 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 21835 | 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 21836 | 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 21837 | 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 21838 | 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 21839 | 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 21840 | The scalar injection is a ring homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ AssAlg → 𝐴 ∈ (𝐹 RingHom 𝑊)) | ||
Theorem | rnascl 21841 | 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 21842 | 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 21843 | 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 21844 | (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 21845 | 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 21846 | The injection of scalars is invariant between subalgebras and superalgebras. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝑋 = (𝑊 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 = (algSc‘𝑋)) | ||
Theorem | asclpropd 21847* | 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 21848 | 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 21849 | Lemma 1 for assamulgscm 21851 (induction base). (Contributed by AV, 26-Aug-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐺 = (mulGrp‘𝐹) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝐻 = (mulGrp‘𝑊) & ⊢ 𝐸 = (.g‘𝐻) ⇒ ⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → (0𝐸(𝐴 · 𝑋)) = ((0 ↑ 𝐴) · (0𝐸𝑋))) | ||
Theorem | assamulgscmlem2 21850 | Lemma for assamulgscm 21851 (induction step). (Contributed by AV, 26-Aug-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐺 = (mulGrp‘𝐹) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝐻 = (mulGrp‘𝑊) & ⊢ 𝐸 = (.g‘𝐻) ⇒ ⊢ (𝑦 ∈ ℕ0 → (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → ((𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋)) → ((𝑦 + 1)𝐸(𝐴 · 𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))))) | ||
Theorem | assamulgscm 21851 | 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 | asclmulg 21852 | Apply group multiplication to the algebra scalars. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ↑ = (.g‘𝑊) & ⊢ ∗ = (.g‘𝐹) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → (𝐴‘(𝑁 ∗ 𝑋)) = (𝑁 ↑ (𝐴‘𝑋))) | ||
Theorem | zlmassa 21853 | The ℤ-module operation turns a ring into an associative algebra over ℤ. Also see zlmlmod 21469. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ Ring ↔ 𝑊 ∈ AssAlg) | ||
Syntax | cmps 21854 | Multivariate power series. |
class mPwSer | ||
Syntax | cmvr 21855 | Multivariate power series variables. |
class mVar | ||
Syntax | cmpl 21856 | Multivariate polynomials. |
class mPoly | ||
Syntax | cltb 21857 | Ordering on terms of a multivariate polynomial. |
class <bag | ||
Syntax | copws 21858 | Ordered set of power series. |
class ordPwSer | ||
Definition | df-psr 21859* | 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 21860* | 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 21861* | 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 21862* | 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 21863* | 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 21864 | The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ Rel dom mPwSer | ||
Theorem | psrval 21865* | 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 21866 | 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 21867* | Elementhood in the set of finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝐹 ∈ 𝐷 ↔ (𝐹:𝐼⟶ℕ0 ∧ (◡𝐹 “ ℕ) ∈ Fin))) | ||
Theorem | psrbagf 21868* | 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 21869* | Obsolete version of psrbag 21867 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 21870* | 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 21871* | Obsolete version of psrbagfsupp 21870 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 21872* | 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 21873* | The constant function equal to zero is a finite bag. (Contributed by AV, 8-Jul-2019.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷) | ||
Theorem | psrbaglesupp 21874* | 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 21875* | Obsolete version of psrbaglesupp 21874 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 21876* | 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 21877* | Obsolete version of psrbaglecl 21876 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 21878* | 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 21879* | Obsolete version of psrbagaddcl 21878 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 21880* | 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 21881* | Obsolete version of psrbagcon 21880 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 21882* | 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 21883* | Obsolete version of psrbaglefi 21882 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 21884* | 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 21885* | Obsolete version of psrbagconcl 21884 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 | psrbagleadd1 21886* | The analogue of "𝑋 ≤ 𝐹 implies 𝑋 + 𝐺 ≤ 𝐹 + 𝐺 " (compare leadd1d 11840) for bags. (Contributed by SN, 2-May-2025.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} & ⊢ 𝑇 = {𝑧 ∈ 𝐷 ∣ 𝑧 ∘r ≤ (𝐹 ∘f + 𝐺)} ⇒ ⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → (𝑋 ∘f + 𝐺) ∈ 𝑇) | ||
Theorem | psrbagconf1o 21887* | 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 21888* | Obsolete version of psrbagconf1o 21887 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 21889* | Obsolete version of gsumbagdiaglem 21892 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 21890* | Obsolete version of gsumbagdiag 21893 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 21891* | Obsolete version of psrass1lem 21894 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 21892* | Lemma for gsumbagdiag 21893. (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 21893* | Two-dimensional commutation of a group sum over a "triangular" region. fsum0diag 15759 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 21894* | A group sum commutation used by psrass1 21926. (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 21895* | 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 21896* | 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 21897 | An element of the set of power series is a function. (Contributed by AV, 17-Jul-2019.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝑋 ∈ 𝐵 → Fun 𝑋) | ||
Theorem | psrplusg 21898 | 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 21899 | The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ + = (+g‘𝑅) & ⊢ ✚ = (+g‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ✚ 𝑌) = (𝑋 ∘f + 𝑌)) | ||
Theorem | psraddcl 21900 | Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014.) Generalize to magmas. (Revised by SN, 12-Apr-2025.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Mgm) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |