Home | Metamath
Proof Explorer Theorem List (p. 192 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cdomn 19101 | Class of (ring theoretic) domains. |
class Domn | ||
Syntax | cidom 19102 | Class of integral domains. |
class IDomn | ||
Syntax | cpid 19103 | Class of principal ideal domains. |
class PID | ||
Definition | df-rlreg 19104* | Define the set of left-regular elements in a ring as those elements which are not left zero divisors, meaning that multiplying a nonzero element on the left by a left-regular element gives a nonzero product. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ RLReg = (𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))}) | ||
Definition | df-domn 19105* | A domain is a nonzero ring in which there are no nontrivial zero divisors. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ Domn = {𝑟 ∈ NzRing ∣ [(Base‘𝑟) / 𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))} | ||
Definition | df-idom 19106 | An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ IDomn = (CRing ∩ Domn) | ||
Definition | df-pid 19107 | A principal ideal domain is an integral domain satisfying the left principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ PID = (IDomn ∩ LPIR) | ||
Theorem | rrgval 19108* | Value of the set or left-regular elements in a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} | ||
Theorem | isrrg 19109* | Membership in the set of left-regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ((𝑋 · 𝑦) = 0 → 𝑦 = 0 ))) | ||
Theorem | rrgeq0i 19110 | Property of a left-regular element. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 → 𝑌 = 0 )) | ||
Theorem | rrgeq0 19111 | Left-multiplication by a left regular element does not change zeroness. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 ↔ 𝑌 = 0 )) | ||
Theorem | rrgsupp 19112 | Left multiplication by a left regular element does not change the support set of a vector. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Revised by AV, 20-Jul-2019.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌:𝐼⟶𝐵) ⇒ ⊢ (𝜑 → (((𝐼 × {𝑋}) ∘𝑓 · 𝑌) supp 0 ) = (𝑌 supp 0 )) | ||
Theorem | rrgss 19113 | Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐸 ⊆ 𝐵 | ||
Theorem | unitrrg 19114 | Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑈 ⊆ 𝐸) | ||
Theorem | isdomn 19115* | Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) | ||
Theorem | domnnzr 19116 | A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) | ||
Theorem | domnring 19117 | A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring) | ||
Theorem | domneq0 19118 | In a domain, a product is zero iff it has a zero factor. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 ↔ (𝑋 = 0 ∨ 𝑌 = 0 ))) | ||
Theorem | domnmuln0 19119 | In a domain, a product of nonzero elements is nonzero. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 )) → (𝑋 · 𝑌) ≠ 0 ) | ||
Theorem | isdomn2 19120 | A ring is a domain iff all nonzero elements are nonzero-divisors. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ (𝐵 ∖ { 0 }) ⊆ 𝐸)) | ||
Theorem | domnrrg 19121 | In a domain, any nonzero element is a nonzero-divisor. (Contributed by Mario Carneiro, 28-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝐸) | ||
Theorem | opprdomn 19122 | The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn → 𝑂 ∈ Domn) | ||
Theorem | abvn0b 19123 | Another characterization of domains, hinted at in abvtriv 18664: a nonzero ring is a domain iff it has an absolute value. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ 𝐴 = (AbsVal‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ 𝐴 ≠ ∅)) | ||
Theorem | drngdomn 19124 | A division ring is a domain. (Contributed by Mario Carneiro, 29-Mar-2015.) |
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Domn) | ||
Theorem | isidom 19125 | An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.) |
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) | ||
Theorem | fldidom 19126 | A field is an integral domain. (Contributed by Mario Carneiro, 29-Mar-2015.) |
⊢ (𝑅 ∈ Field → 𝑅 ∈ IDomn) | ||
Theorem | fidomndrnglem 19127* | Lemma for fidomndrng 19128. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ { 0 })) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝐴)) ⇒ ⊢ (𝜑 → 𝐴 ∥ 1 ) | ||
Theorem | fidomndrng 19128 | A finite domain is a division ring. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐵 ∈ Fin → (𝑅 ∈ Domn ↔ 𝑅 ∈ DivRing)) | ||
Theorem | fiidomfld 19129 | A finite integral domain is a field. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐵 ∈ Fin → (𝑅 ∈ IDomn ↔ 𝑅 ∈ Field)) | ||
Syntax | casa 19130 | Associative algebra. |
class AssAlg | ||
Syntax | casp 19131 | Algebraic span function. |
class AlgSpan | ||
Syntax | cascl 19132 | Class of algebra scalar injection function. |
class algSc | ||
Definition | df-assa 19133* | Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a (commutative) 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.) |
⊢ AssAlg = {𝑤 ∈ (LMod ∩ Ring) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))} | ||
Definition | df-asp 19134* | 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 19135* | Every unital algebra contains a canonical homomorphic image of its ring of scalars as scalar multiples of the unit. This names the homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015.) |
⊢ algSc = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑤)) ↦ (𝑥( ·𝑠 ‘𝑤)(1r‘𝑤)))) | ||
Theorem | isassa 19136* | The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) ⇒ ⊢ (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing) ∧ ∀𝑟 ∈ 𝐵 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦)) ∧ (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))))) | ||
Theorem | assalem 19137 | The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌)))) | ||
Theorem | assaass 19138 | Left-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌))) | ||
Theorem | assaassr 19139 | Right-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌))) | ||
Theorem | assalmod 19140 | An associative algebra is a left module. (Contributed by Mario Carneiro, 5-Dec-2014.) |
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) | ||
Theorem | assaring 19141 | An associative algebra is a ring. (Contributed by Mario Carneiro, 5-Dec-2014.) |
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) | ||
Theorem | assasca 19142 | An associative algebra's scalar field is a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ AssAlg → 𝐹 ∈ CRing) | ||
Theorem | assa2ass 19143 | 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 19144* | Sufficient condition for being an associative algebra. (Contributed by Mario Carneiro, 5-Dec-2014.) |
⊢ (𝜑 → 𝑉 = (Base‘𝑊)) & ⊢ (𝜑 → 𝐹 = (Scalar‘𝑊)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐹)) & ⊢ (𝜑 → · = ( ·𝑠 ‘𝑊)) & ⊢ (𝜑 → × = (.r‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑊 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ CRing) & ⊢ ((𝜑 ∧ (𝑟 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝑟 · 𝑥) × 𝑦) = (𝑟 · (𝑥 × 𝑦))) & ⊢ ((𝜑 ∧ (𝑟 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 × (𝑟 · 𝑦)) = (𝑟 · (𝑥 × 𝑦))) ⇒ ⊢ (𝜑 → 𝑊 ∈ AssAlg) | ||
Theorem | issubassa 19145 | 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 | sraassa 19146 | The subring algebra over a commutative ring is an associative algebra. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆) ⇒ ⊢ ((𝑊 ∈ CRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → 𝐴 ∈ AssAlg) | ||
Theorem | rlmassa 19147 | The ring module over a commutative ring is an associative algebra. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ (𝑅 ∈ CRing → (ringLMod‘𝑅) ∈ AssAlg) | ||
Theorem | assapropd 19148* | 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 19149* | Value of the algebraic closure operation inside an associative algebra. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝐴 = (AlgSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (𝐴‘𝑆) = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) | ||
Theorem | asplss 19150 | 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 19151 | The algebraic span of a subalgebra is itself. (spanid 27590 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝐴 = (AlgSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊) ∧ 𝑆 ∈ 𝐿) → (𝐴‘𝑆) = 𝑆) | ||
Theorem | aspsubrg 19152 | 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 19153 | Span preserves subset ordering. (spanss 27591 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝐴 = (AlgSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆) → (𝐴‘𝑇) ⊆ (𝐴‘𝑆)) | ||
Theorem | aspssid 19154 | A set of vectors is a subset of its span. (spanss2 27588 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝐴 = (AlgSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ (𝐴‘𝑆)) | ||
Theorem | asclfval 19155* | Function value of the algebraic scalars function. (Contributed by Mario Carneiro, 8-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 1 = (1r‘𝑊) ⇒ ⊢ 𝐴 = (𝑥 ∈ 𝐾 ↦ (𝑥 · 1 )) | ||
Theorem | asclval 19156 | Value of a mapped algebra scalar. (Contributed by Mario Carneiro, 8-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 1 = (1r‘𝑊) ⇒ ⊢ (𝑋 ∈ 𝐾 → (𝐴‘𝑋) = (𝑋 · 1 )) | ||
Theorem | asclfn 19157 | Unconditional functionality of the algebra scalars function. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ 𝐴 Fn 𝐾 | ||
Theorem | asclf 19158 | 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 19159 | The algebra scalars function is a group homomorphism. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ Ring) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐹 GrpHom 𝑊)) | ||
Theorem | asclmul1 19160 | 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 19161 | 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 | asclinvg 19162 | 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 19163 | The scalar injection is a ring homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ AssAlg → 𝐴 ∈ (𝐹 RingHom 𝑊)) | ||
Theorem | rnascl 19164 | 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 | ressascl 19165 | The injection of scalars is invariant between subalgebras and superalgebras. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝑋 = (𝑊 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 = (algSc‘𝑋)) | ||
Theorem | issubassa2 19166 | 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 | asclpropd 19167* | 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 19168 | 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 19169 | Lemma 1 for assamulgscm 19171 (induction base). (Contributed by AV, 26-Aug-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐺 = (mulGrp‘𝐹) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝐻 = (mulGrp‘𝑊) & ⊢ 𝐸 = (.g‘𝐻) ⇒ ⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → (0𝐸(𝐴 · 𝑋)) = ((0 ↑ 𝐴) · (0𝐸𝑋))) | ||
Theorem | assamulgscmlem2 19170 | Lemma for assamulgscm 19171 (induction step). (Contributed by AV, 26-Aug-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐺 = (mulGrp‘𝐹) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝐻 = (mulGrp‘𝑊) & ⊢ 𝐸 = (.g‘𝐻) ⇒ ⊢ (𝑦 ∈ ℕ0 → (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → ((𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋)) → ((𝑦 + 1)𝐸(𝐴 · 𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))))) | ||
Theorem | assamulgscm 19171 | Exponentiation of a scalar multiplication in an associative algebra: (𝑎 · 𝑋)↑𝑁 = (𝑎↑𝑁) × (𝑋↑𝑁). (Contributed by AV, 26-Aug-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐺 = (mulGrp‘𝐹) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝐻 = (mulGrp‘𝑊) & ⊢ 𝐸 = (.g‘𝐻) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ (𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉)) → (𝑁𝐸(𝐴 · 𝑋)) = ((𝑁 ↑ 𝐴) · (𝑁𝐸𝑋))) | ||
Syntax | cmps 19172 | Multivariate power series. |
class mPwSer | ||
Syntax | cmvr 19173 | Multivariate power series variables. |
class mVar | ||
Syntax | cmpl 19174 | Multivariate polynomials. |
class mPoly | ||
Syntax | cltb 19175 | Ordering on terms of a multivariate polynomial. |
class <bag | ||
Syntax | copws 19176 | Ordered set of power series. |
class ordPwSer | ||
Definition | df-psr 19177* | 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 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))〉, 〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))〉} ∪ {〈(Scalar‘ndx), 𝑟〉, 〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))〉, 〈(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))〉})) | ||
Definition | df-mvr 19178* | Define the generating elements of the power series algebra. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ mVar = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟))))) | ||
Definition | df-mpl 19179* | 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 19180* | 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 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∧ ∃𝑧 ∈ 𝑖 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))}) | ||
Definition | df-opsr 19181* | 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 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉))) | ||
Theorem | reldmpsr 19182 | The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ Rel dom mPwSer | ||
Theorem | psrval 19183* | Value of the multivariate power series structure. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑂 = (TopOpen‘𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐵 = (𝐾 ↑𝑚 𝐷)) & ⊢ ✚ = ( ∘𝑓 + ↾ (𝐵 × 𝐵)) & ⊢ × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) & ⊢ ∙ = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓)) & ⊢ (𝜑 → 𝐽 = (∏t‘(𝐷 × {𝑂}))) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑆 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), ✚ 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑅〉, 〈( ·𝑠 ‘ndx), ∙ 〉, 〈(TopSet‘ndx), 𝐽〉})) | ||
Theorem | psrvalstr 19184 | 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 19185* | Elementhood in the set of finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝐹 ∈ 𝐷 ↔ (𝐹:𝐼⟶ℕ0 ∧ (◡𝐹 “ ℕ) ∈ Fin))) | ||
Theorem | psrbagf 19186* | A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐼⟶ℕ0) | ||
Theorem | snifpsrbag 19187* | A bag containing one element is a finite bag. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 8-Jul-2019.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 𝑁, 0)) ∈ 𝐷) | ||
Theorem | fczpsrbag 19188* | The constant function equal to zero is a finite bag. (Contributed by AV, 8-Jul-2019.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ 0) ∈ 𝐷) | ||
Theorem | psrbaglesupp 19189* | The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟 ≤ 𝐹)) → (◡𝐺 “ ℕ) ⊆ (◡𝐹 “ ℕ)) | ||
Theorem | psrbaglecl 19190* | The set of finite bags is downward-closed. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟 ≤ 𝐹)) → 𝐺 ∈ 𝐷) | ||
Theorem | psrbagaddcl 19191* | The sum of two finite bags is a finite bag. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) → (𝐹 ∘𝑓 + 𝐺) ∈ 𝐷) | ||
Theorem | psrbagcon 19192* | The analogue of the statement "0 ≤ 𝐺 ≤ 𝐹 implies 0 ≤ 𝐹 − 𝐺 ≤ 𝐹 " for finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟 ≤ 𝐹)) → ((𝐹 ∘𝑓 − 𝐺) ∈ 𝐷 ∧ (𝐹 ∘𝑓 − 𝐺) ∘𝑟 ≤ 𝐹)) | ||
Theorem | psrbaglefi 19193* | There are finitely many bags dominated by a given bag. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 25-Jan-2015.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} ∈ Fin) | ||
Theorem | psrbagconcl 19194* | The complement of a bag is a bag. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → (𝐹 ∘𝑓 − 𝑋) ∈ 𝑆) | ||
Theorem | psrbagconf1o 19195* | Bag complementation is a bijection on the set of bags dominated by a given bag 𝐹. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → (𝑥 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑥)):𝑆–1-1-onto→𝑆) | ||
Theorem | gsumbagdiaglem 19196* | Lemma for gsumbagdiag 19197. (Contributed by Mario Carneiro, 5-Jan-2015.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑋)})) → (𝑌 ∈ 𝑆 ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑌)})) | ||
Theorem | gsumbagdiag 19197* | Two-dimensional commutation of a group sum over a "triangular" region. fsum0diag 14351 analogue for finite bags. (Contributed by Mario Carneiro, 5-Jan-2015.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑗)})) → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝑆, 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑗)} ↦ 𝑋)) = (𝐺 Σg (𝑘 ∈ 𝑆, 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑘)} ↦ 𝑋))) | ||
Theorem | psrass1lem 19198* | A group sum commutation used by psrass1 19226. (Contributed by Mario Carneiro, 5-Jan-2015.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑗)})) → 𝑋 ∈ 𝐵) & ⊢ (𝑘 = (𝑛 ∘𝑓 − 𝑗) → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑗)} ↦ 𝑋))))) | ||
Theorem | psrbas 19199* | 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 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐵 = (𝐾 ↑𝑚 𝐷)) | ||
Theorem | psrelbas 19200* | An element of the set of power series is a function on the coefficients. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋:𝐷⟶𝐾) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |