HomeTheorem List (p. 219 of 503)
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. 219 of 503) | < 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-31009) |
Hilbert Space Explorer
(31010-32532) |
Users' Mathboxes
(32533-50277) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | islinds2 21801* | Expanded property of an independent set of vectors. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (LSpan‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝑁 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) ⇒ ⊢ (𝑊 ∈ 𝑌 → (𝐹 ∈ (LIndS‘𝑊) ↔ (𝐹 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥}))))) | ||
| Theorem | islindf2 21802* | Property of an independent family of vectors with prior constrained domain and codomain. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (LSpan‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝑁 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) ⇒ ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑥 ∈ 𝐼 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (𝐼 ∖ {𝑥}))))) | ||
| Theorem | lindff 21803 | Functional property of a linearly independent family. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝐹 LIndF 𝑊 ∧ 𝑊 ∈ 𝑌) → 𝐹:dom 𝐹⟶𝐵) | ||
| Theorem | lindfind 21804 | A linearly independent family is independent: no nonzero element multiple can be expressed as a linear combination of the others. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
| ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐿 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐿) & ⊢ 𝐾 = (Base‘𝐿) ⇒ ⊢ (((𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹) ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 )) → ¬ (𝐴 · (𝐹‘𝐸)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝐸})))) | ||
| Theorem | lindsind 21805 | A linearly independent set is independent: no nonzero element multiple can be expressed as a linear combination of the others. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
| ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐿 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐿) & ⊢ 𝐾 = (Base‘𝐿) ⇒ ⊢ (((𝐹 ∈ (LIndS‘𝑊) ∧ 𝐸 ∈ 𝐹) ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 )) → ¬ (𝐴 · 𝐸) ∈ (𝑁‘(𝐹 ∖ {𝐸}))) | ||
| Theorem | lindfind2 21806 | In a linearly independent family in a module over a nonzero ring, no element is contained in the span of any non-containing set. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
| ⊢ 𝐾 = (LSpan‘𝑊) & ⊢ 𝐿 = (Scalar‘𝑊) ⇒ ⊢ (((𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹) → ¬ (𝐹‘𝐸) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝐸})))) | ||
| Theorem | lindsind2 21807 | In a linearly independent set in a module over a nonzero ring, no element is contained in the span of any non-containing set. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
| ⊢ 𝐾 = (LSpan‘𝑊) & ⊢ 𝐿 = (Scalar‘𝑊) ⇒ ⊢ (((𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing) ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝐸 ∈ 𝐹) → ¬ 𝐸 ∈ (𝐾‘(𝐹 ∖ {𝐸}))) | ||
| Theorem | lindff1 21808 | A linearly independent family over a nonzero ring has no repeated elements. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐿 = (Scalar‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊) → 𝐹:dom 𝐹–1-1→𝐵) | ||
| Theorem | lindfrn 21809 | The range of an independent family is an independent set. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
| ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ran 𝐹 ∈ (LIndS‘𝑊)) | ||
| Theorem | f1lindf 21810 | Rearranging and deleting elements from an independent family gives an independent family. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
| ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → (𝐹 ∘ 𝐺) LIndF 𝑊) | ||
| Theorem | lindfres 21811 | Any restriction of an independent family is independent. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
| ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → (𝐹 ↾ 𝑋) LIndF 𝑊) | ||
| Theorem | lindsss 21812 | Any subset of an independent set is independent. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
| ⊢ ((𝑊 ∈ LMod ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝐺 ⊆ 𝐹) → 𝐺 ∈ (LIndS‘𝑊)) | ||
| Theorem | f1linds 21813 | A family constructed from non-repeated elements of an independent set is independent. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
| ⊢ ((𝑊 ∈ LMod ∧ 𝑆 ∈ (LIndS‘𝑊) ∧ 𝐹:𝐷–1-1→𝑆) → 𝐹 LIndF 𝑊) | ||
| Theorem | islindf3 21814 | In a nonzero ring, independent families can be equivalently characterized as renamings of independent sets. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
| ⊢ 𝐿 = (Scalar‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹–1-1→V ∧ ran 𝐹 ∈ (LIndS‘𝑊)))) | ||
| Theorem | lindfmm 21815 | Linear independence of a family is unchanged by injective linear functions. (Contributed by Stefan O'Rear, 26-Feb-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
| ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) ⇒ ⊢ ((𝐺 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺:𝐵–1-1→𝐶 ∧ 𝐹:𝐼⟶𝐵) → (𝐹 LIndF 𝑆 ↔ (𝐺 ∘ 𝐹) LIndF 𝑇)) | ||
| Theorem | lindsmm 21816 | Linear independence of a set is unchanged by injective linear functions. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) ⇒ ⊢ ((𝐺 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺:𝐵–1-1→𝐶 ∧ 𝐹 ⊆ 𝐵) → (𝐹 ∈ (LIndS‘𝑆) ↔ (𝐺 “ 𝐹) ∈ (LIndS‘𝑇))) | ||
| Theorem | lindsmm2 21817 | The monomorphic image of an independent set is independent. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) ⇒ ⊢ ((𝐺 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺:𝐵–1-1→𝐶 ∧ 𝐹 ∈ (LIndS‘𝑆)) → (𝐺 “ 𝐹) ∈ (LIndS‘𝑇)) | ||
| Theorem | lsslindf 21818 | Linear independence is unchanged by working in a subspace. (Contributed by Stefan O'Rear, 24-Feb-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
| ⊢ 𝑈 = (LSubSp‘𝑊) & ⊢ 𝑋 = (𝑊 ↾s 𝑆) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) → (𝐹 LIndF 𝑋 ↔ 𝐹 LIndF 𝑊)) | ||
| Theorem | lsslinds 21819 | Linear independence is unchanged by working in a subspace. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
| ⊢ 𝑈 = (LSubSp‘𝑊) & ⊢ 𝑋 = (𝑊 ↾s 𝑆) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ 𝐹 ⊆ 𝑆) → (𝐹 ∈ (LIndS‘𝑋) ↔ 𝐹 ∈ (LIndS‘𝑊))) | ||
| Theorem | islbs4 21820 | A basis is an independent spanning set. This could have been used as alternative definition of a basis: LBasis = (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ (((LSpan‘𝑤) ‘𝑏) = (Base‘𝑤) ∧ 𝑏 ∈ (LIndS‘𝑤))}). (Contributed by Stefan O'Rear, 24-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝐾 = (LSpan‘𝑊) ⇒ ⊢ (𝑋 ∈ 𝐽 ↔ (𝑋 ∈ (LIndS‘𝑊) ∧ (𝐾‘𝑋) = 𝐵)) | ||
| Theorem | lbslinds 21821 | A basis is independent. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
| ⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ 𝐽 ⊆ (LIndS‘𝑊) | ||
| Theorem | islinds3 21822 | A subset is linearly independent iff it is a basis of its span. (Contributed by Stefan O'Rear, 25-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐾 = (LSpan‘𝑊) & ⊢ 𝑋 = (𝑊 ↾s (𝐾‘𝑌)) & ⊢ 𝐽 = (LBasis‘𝑋) ⇒ ⊢ (𝑊 ∈ LMod → (𝑌 ∈ (LIndS‘𝑊) ↔ 𝑌 ∈ 𝐽)) | ||
| Theorem | islinds4 21823* | A set is independent in a vector space iff it is a subset of some basis. This is an axiom of choice equivalent. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
| ⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → (𝑌 ∈ (LIndS‘𝑊) ↔ ∃𝑏 ∈ 𝐽 𝑌 ⊆ 𝑏)) | ||
| Theorem | lmimlbs 21824 | The isomorphic image of a basis is a basis. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
| ⊢ 𝐽 = (LBasis‘𝑆) & ⊢ 𝐾 = (LBasis‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMIso 𝑇) ∧ 𝐵 ∈ 𝐽) → (𝐹 “ 𝐵) ∈ 𝐾) | ||
| Theorem | lmiclbs 21825 | Having a basis is an isomorphism invariant. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
| ⊢ 𝐽 = (LBasis‘𝑆) & ⊢ 𝐾 = (LBasis‘𝑇) ⇒ ⊢ (𝑆 ≃𝑚 𝑇 → (𝐽 ≠ ∅ → 𝐾 ≠ ∅)) | ||
| Theorem | islindf4 21826* | A family is independent iff it has no nontrivial representations of zero. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑌 = (0g‘𝑅) & ⊢ 𝐿 = (Base‘(𝑅 freeLMod 𝐼)) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})))) | ||
| Theorem | islindf5 21827* | A family is independent iff the linear combinations homomorphism is injective. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
| ⊢ 𝐹 = (𝑅 freeLMod 𝐼) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝐶 = (Base‘𝑇) & ⊢ · = ( ·𝑠 ‘𝑇) & ⊢ 𝐸 = (𝑥 ∈ 𝐵 ↦ (𝑇 Σg (𝑥 ∘f · 𝐴))) & ⊢ (𝜑 → 𝑇 ∈ LMod) & ⊢ (𝜑 → 𝐼 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 = (Scalar‘𝑇)) & ⊢ (𝜑 → 𝐴:𝐼⟶𝐶) ⇒ ⊢ (𝜑 → (𝐴 LIndF 𝑇 ↔ 𝐸:𝐵–1-1→𝐶)) | ||
| Theorem | indlcim 21828* | An independent, spanning family extends to an isomorphism from a free module. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
| ⊢ 𝐹 = (𝑅 freeLMod 𝐼) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝐶 = (Base‘𝑇) & ⊢ · = ( ·𝑠 ‘𝑇) & ⊢ 𝑁 = (LSpan‘𝑇) & ⊢ 𝐸 = (𝑥 ∈ 𝐵 ↦ (𝑇 Σg (𝑥 ∘f · 𝐴))) & ⊢ (𝜑 → 𝑇 ∈ LMod) & ⊢ (𝜑 → 𝐼 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 = (Scalar‘𝑇)) & ⊢ (𝜑 → 𝐴:𝐼–onto→𝐽) & ⊢ (𝜑 → 𝐴 LIndF 𝑇) & ⊢ (𝜑 → (𝑁‘𝐽) = 𝐶) ⇒ ⊢ (𝜑 → 𝐸 ∈ (𝐹 LMIso 𝑇)) | ||
| Theorem | lbslcic 21829 | A module with a basis is isomorphic to a free module with the same cardinality. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐽 ∧ 𝐼 ≈ 𝐵) → 𝑊 ≃𝑚 (𝐹 freeLMod 𝐼)) | ||
| Theorem | lmisfree 21830* | A module has a basis iff it is isomorphic to a free module. In settings where isomorphic objects are not distinguished, it is common to define "free module" as any module with a basis; thus for instance lbsex 21153 might be described as "every vector space is free". (Contributed by Stefan O'Rear, 26-Feb-2015.) |
| ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → (𝐽 ≠ ∅ ↔ ∃𝑘 𝑊 ≃𝑚 (𝐹 freeLMod 𝑘))) | ||
| Theorem | lvecisfrlm 21831* | Every vector space is isomorphic to a free module. (Contributed by AV, 7-Mar-2019.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → ∃𝑘 𝑊 ≃𝑚 (𝐹 freeLMod 𝑘)) | ||
| Theorem | lmimco 21832 | The composition of two isomorphisms of modules is an isomorphism of modules. (Contributed by AV, 10-Mar-2019.) |
| ⊢ ((𝐹 ∈ (𝑆 LMIso 𝑇) ∧ 𝐺 ∈ (𝑅 LMIso 𝑆)) → (𝐹 ∘ 𝐺) ∈ (𝑅 LMIso 𝑇)) | ||
| Theorem | lmictra 21833 | Module isomorphism is transitive. (Contributed by AV, 10-Mar-2019.) |
| ⊢ ((𝑅 ≃𝑚 𝑆 ∧ 𝑆 ≃𝑚 𝑇) → 𝑅 ≃𝑚 𝑇) | ||
| Theorem | uvcf1o 21834 | In a nonzero ring, the mapping of the index set of a free module onto the unit vectors of the free module is a 1-1 onto function. (Contributed by AV, 10-Mar-2019.) |
| ⊢ 𝑈 = (𝑅 unitVec 𝐼) ⇒ ⊢ ((𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊) → 𝑈:𝐼–1-1-onto→ran 𝑈) | ||
| Theorem | uvcendim 21835 | 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 21836 | 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 21837 | 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 21838 | Associative algebra. |
| class AssAlg | ||
| Syntax | casp 21839 | Algebraic span function. |
| class AlgSpan | ||
| Syntax | cascl 21840 | Class of algebra scalar lifting function. |
| class algSc | ||
| Definition | df-assa 21841* | 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 21842* | 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 21843* | 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 21844* | 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 21845 | The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)) ∧ (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌)))) | ||
| Theorem | assaass 21846 | Left-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌))) | ||
| Theorem | assaassr 21847 | Right-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑋 × (𝐴 · 𝑌)) = (𝐴 · (𝑋 × 𝑌))) | ||
| Theorem | assalmod 21848 | An associative algebra is a left module. (Contributed by Mario Carneiro, 5-Dec-2014.) |
| ⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) | ||
| Theorem | assaring 21849 | An associative algebra is a ring. (Contributed by Mario Carneiro, 5-Dec-2014.) |
| ⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) | ||
| Theorem | assasca 21850 | 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 21851 | Left- and right-associative property of an associative algebra. Notice that the scalars are commuted! (Contributed by AV, 14-Aug-2019.) (Proof shortened by Zhi Wang, 11-Sep-2025.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ ∗ = (.r‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝐴 · 𝑋) × (𝐶 · 𝑌)) = ((𝐶 ∗ 𝐴) · (𝑋 × 𝑌))) | ||
| Theorem | assa2ass2 21852 | Left- and right-associative property of an associative algebra. Notice that the scalars are not commuted! (Contributed by Zhi Wang, 11-Sep-2025.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ ∗ = (.r‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝐴 · 𝑋) × (𝐶 · 𝑌)) = ((𝐴 ∗ 𝐶) · (𝑋 × 𝑌))) | ||
| Theorem | isassad 21853* | 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 21854 | A subring that is also a subspace is a subalgebra. The key theorem is islss3 20943. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| ⊢ 𝑆 = (𝑊 ↾s 𝐴) & ⊢ 𝐿 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝑆 ∈ AssAlg) | ||
| Theorem | issubassa 21855 | 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 21856 | 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 21857 | 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 | rlmassa 21858 | The ring module over a commutative ring is an associative algebra. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ (𝑅 ∈ CRing → (ringLMod‘𝑅) ∈ AssAlg) | ||
| Theorem | assapropd 21859* | 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 21860* | Value of the algebraic closure operation inside an associative algebra. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| ⊢ 𝐴 = (AlgSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (𝐴‘𝑆) = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) | ||
| Theorem | asplss 21861 | 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 21862 | The algebraic span of a subalgebra is itself. (spanid 31438 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
| ⊢ 𝐴 = (AlgSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊) ∧ 𝑆 ∈ 𝐿) → (𝐴‘𝑆) = 𝑆) | ||
| Theorem | aspsubrg 21863 | 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 21864 | Span preserves subset ordering. (spanss 31439 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
| ⊢ 𝐴 = (AlgSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆) → (𝐴‘𝑇) ⊆ (𝐴‘𝑆)) | ||
| Theorem | aspssid 21865 | A set of vectors is a subset of its span. (spanss2 31436 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
| ⊢ 𝐴 = (AlgSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ (𝐴‘𝑆)) | ||
| Theorem | asclfval 21866* | Function value of the algebra scalar lifting function. (Contributed by Mario Carneiro, 8-Mar-2015.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 1 = (1r‘𝑊) ⇒ ⊢ 𝐴 = (𝑥 ∈ 𝐾 ↦ (𝑥 · 1 )) | ||
| Theorem | asclval 21867 | Value of a mapped algebra scalar. (Contributed by Mario Carneiro, 8-Mar-2015.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 1 = (1r‘𝑊) ⇒ ⊢ (𝑋 ∈ 𝐾 → (𝐴‘𝑋) = (𝑋 · 1 )) | ||
| Theorem | asclfn 21868 | Unconditional functionality of the algebra scalar lifting function. (Contributed by Mario Carneiro, 9-Mar-2015.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ 𝐴 Fn 𝐾 | ||
| Theorem | asclf 21869 | The algebra scalar lifting function is a function into the base set. (Contributed by Mario Carneiro, 4-Jul-2015.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ Ring) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝜑 → 𝐴:𝐾⟶𝐵) | ||
| Theorem | asclghm 21870 | The algebra scalar lifting function is a group homomorphism. (Contributed by Mario Carneiro, 4-Jul-2015.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ Ring) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐹 GrpHom 𝑊)) | ||
| Theorem | asclelbas 21871 | Lifted scalars are in the base set of the algebra. (Contributed by Zhi Wang, 11-Sep-2025.) (Proof shortened by Thierry Arnoux, 22-Sep-2025.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘𝐶) ∈ (Base‘𝑊)) | ||
| Theorem | ascl0 21872 | 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 21873 | 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 21874 | 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 21875 | 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 21876 | The algebra scalar lifting 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 21877 | 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 21878 | The algebra scalar lifting function is a ring homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ AssAlg → 𝐴 ∈ (𝐹 RingHom 𝑊)) | ||
| Theorem | rnascl 21879 | The set of lifted 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 21880 | 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 21881 | 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 21882 | (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 21883 | 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 21884 | The lifting of scalars is invariant between subalgebras and superalgebras. (Contributed by Mario Carneiro, 9-Mar-2015.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝑋 = (𝑊 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 = (algSc‘𝑋)) | ||
| Theorem | asclpropd 21885* | 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 21886 | 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 21887 | Lemma 1 for assamulgscm 21889 (induction base). (Contributed by AV, 26-Aug-2019.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐺 = (mulGrp‘𝐹) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝐻 = (mulGrp‘𝑊) & ⊢ 𝐸 = (.g‘𝐻) ⇒ ⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → (0𝐸(𝐴 · 𝑋)) = ((0 ↑ 𝐴) · (0𝐸𝑋))) | ||
| Theorem | assamulgscmlem2 21888 | Lemma for assamulgscm 21889 (induction step). (Contributed by AV, 26-Aug-2019.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐺 = (mulGrp‘𝐹) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝐻 = (mulGrp‘𝑊) & ⊢ 𝐸 = (.g‘𝐻) ⇒ ⊢ (𝑦 ∈ ℕ0 → (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → ((𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋)) → ((𝑦 + 1)𝐸(𝐴 · 𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))))) | ||
| Theorem | assamulgscm 21889 | 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 21890 | Apply group multiplication to the algebra scalars. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ↑ = (.g‘𝑊) & ⊢ ∗ = (.g‘𝐹) ⇒ ⊢ ((𝑊 ∈ AssAlg ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾) → (𝐴‘(𝑁 ∗ 𝑋)) = (𝑁 ↑ (𝐴‘𝑋))) | ||
| Theorem | zlmassa 21891 | The ℤ-module operation turns a ring into an associative algebra over ℤ. Also see zlmlmod 21510. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ Ring ↔ 𝑊 ∈ AssAlg) | ||
| Syntax | cmps 21892 | Multivariate power series. |
| class mPwSer | ||
| Syntax | cmvr 21893 | Multivariate power series variables. |
| class mVar | ||
| Syntax | cmpl 21894 | Multivariate polynomials. |
| class mPoly | ||
| Syntax | cltb 21895 | Ordering on terms of a multivariate polynomial. |
| class <bag | ||
| Syntax | copws 21896 | Ordered set of power series. |
| class ordPwSer | ||
| Definition | df-psr 21897* | 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 21898* | 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 21899* | 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 21900* | 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} ∧ ∃𝑧 ∈ 𝑖 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))}) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |