Home | Metamath
Proof Explorer Theorem List (p. 420 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 | ||
Theorem | rhmsubcALTV 41901 | According to df-subc 16295, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 ( see subcssc 16323 and subcss2 16326). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ (𝜑 → 𝐻 ∈ (Subcat‘(RngCatALTV‘𝑈))) | ||
Theorem | rhmsubcALTVcat 41902 | The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020.) (New usage is discouraged.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ (𝜑 → ((RngCatALTV‘𝑈) ↾cat 𝐻) ∈ Cat) | ||
Theorem | xpprsng 41903 | The Cartesian product of an unordered pair and a singleton. (Contributed by AV, 20-May-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈) → ({𝐴, 𝐵} × {𝐶}) = {〈𝐴, 𝐶〉, 〈𝐵, 𝐶〉}) | ||
Theorem | opeliun2xp 41904 | Membership of an ordered pair in a union of Cartesian products over its second component, analogous to opeliunxp 5093. (Contributed by AV, 30-Mar-2019.) |
⊢ (〈𝐶, 𝑦〉 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴)) | ||
Theorem | eliunxp2 41905* | Membership in a union of Cartesian products over its second component, analogous to eliunxp 5181. (Contributed by AV, 30-Mar-2019.) |
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∃𝑥∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) | ||
Theorem | mpt2mptx2 41906* | Express a two-argument function as a one-argument function, or vice-versa. In this version 𝐴(𝑦) is not assumed to be constant w.r.t 𝑦, analogous to mpt2mptx 6649. (Contributed by AV, 30-Mar-2019.) |
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) | ||
Theorem | cbvmpt2x2 41907* | Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 6632 allows 𝐴 to be a function of 𝑦, analogous to cbvmpt2x 6631. (Contributed by AV, 30-Mar-2019.) |
⊢ Ⅎ𝑧𝐴 & ⊢ Ⅎ𝑦𝐷 & ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑤𝐶 & ⊢ Ⅎ𝑥𝐸 & ⊢ Ⅎ𝑦𝐸 & ⊢ (𝑦 = 𝑧 → 𝐴 = 𝐷) & ⊢ ((𝑦 = 𝑧 ∧ 𝑥 = 𝑤) → 𝐶 = 𝐸) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑤 ∈ 𝐷, 𝑧 ∈ 𝐵 ↦ 𝐸) | ||
Theorem | dmmpt2ssx2 41908* | The domain of a mapping is a subset of its base classes expressed as union of Cartesian products over its second component, analogous to dmmpt2ssx 7124. (Contributed by AV, 30-Mar-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ dom 𝐹 ⊆ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) | ||
Theorem | mpt2exxg2 41909* | Existence of an operation class abstraction (version for dependent domains, i.e. the first base class may depend on the second base class), analogous to mpt2exxg 7133. (Contributed by AV, 30-Mar-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐵 𝐴 ∈ 𝑆) → 𝐹 ∈ V) | ||
Theorem | ovmpt2rdxf 41910* | Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpt2dxf 6684. (Contributed by AV, 30-Mar-2019.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) & ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝐿) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑆 & ⊢ Ⅎ𝑦𝑆 ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpt2rdx 41911* | Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpt2dxf 6684. (Contributed by AV, 30-Mar-2019.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) & ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝐿) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpt2x2 41912* | The value of an operation class abstraction. Variant of ovmpt2ga 6688 which does not require 𝐷 and 𝑥 to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) & ⊢ (𝑦 = 𝐵 → 𝐶 = 𝐿) & ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐿 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | fdmdifeqresdif 41913* | The restriction of a conditional mapping to function values of a function having a domain which is a difference with a singleton equals this function. (Contributed by AV, 23-Apr-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝑌, 𝑋, (𝐺‘𝑥))) ⇒ ⊢ (𝐺:(𝐷 ∖ {𝑌})⟶𝑅 → 𝐺 = (𝐹 ↾ (𝐷 ∖ {𝑌}))) | ||
Theorem | offvalfv 41914* | The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) | ||
Theorem | ofaddmndmap 41915 | The function operation applied to the addition for functions (with the same domain) into a monoid is a function (with the same domain) into the monoid. (Contributed by AV, 6-Apr-2019.) |
⊢ 𝑅 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑌 ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴 ∘𝑓 + 𝐵) ∈ (𝑅 ↑𝑚 𝑉)) | ||
Theorem | mapsnop 41916 | A singleton of an ordered pair as an element of the mapping operation. (Contributed by AV, 12-Apr-2019.) |
⊢ 𝐹 = {〈𝑋, 𝑌〉} ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑅 ∧ 𝑅 ∈ 𝑊) → 𝐹 ∈ (𝑅 ↑𝑚 {𝑋})) | ||
Theorem | mapprop 41917 | An unordered pair containing two ordered pairs as an element of the mapping operation. (Contributed by AV, 16-Apr-2019.) |
⊢ 𝐹 = {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ⇒ ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) ∧ (𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊)) → 𝐹 ∈ (𝑅 ↑𝑚 {𝑋, 𝑌})) | ||
Theorem | ztprmneprm 41918 | A prime is not an integer multiple of another prime. (Contributed by AV, 23-May-2019.) |
⊢ ((𝑍 ∈ ℤ ∧ 𝐴 ∈ ℙ ∧ 𝐵 ∈ ℙ) → ((𝑍 · 𝐴) = 𝐵 → 𝐴 = 𝐵)) | ||
Theorem | 2t6m3t4e0 41919 | 2 times 6 minus 3 times 4 equals 0. (Contributed by AV, 24-May-2019.) |
⊢ ((2 · 6) − (3 · 4)) = 0 | ||
Theorem | ssnn0ssfz 41920* | For any finite subset of ℕ0, find a superset in the form of a set of sequential integers, analogous to ssnnssfz 28937. (Contributed by AV, 30-Sep-2019.) |
⊢ (𝐴 ∈ (𝒫 ℕ0 ∩ Fin) → ∃𝑛 ∈ ℕ0 𝐴 ⊆ (0...𝑛)) | ||
Theorem | nn0sumltlt 41921 | If the sum of two nonnegative integers is less than a third integer, then one of the summands is already less than this third integer. (Contributed by AV, 19-Oct-2019.) |
⊢ ((𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0) → ((𝑎 + 𝑏) < 𝑐 → 𝑏 < 𝑐)) | ||
Theorem | bcpascm1 41922 | Pascal's rule for the binomial coefficient, generalized to all integers 𝐾, shifted down by 1. (Contributed by AV, 8-Sep-2019.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) → (((𝑁 − 1)C𝐾) + ((𝑁 − 1)C(𝐾 − 1))) = (𝑁C𝐾)) | ||
Theorem | altgsumbc 41923* | The sum of binomial coefficients for a fixed positive 𝑁 with alternating signs is zero. Notice that this is not valid for 𝑁 = 0 (since ((-1↑0) · (0C0)) = (1 · 1) = 1). For a proof using Pascal's rule (bcpascm1 41922) instead of the binomial theorem (binom 14401) , see altgsumbcALT 41924. (Contributed by AV, 13-Sep-2019.) |
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0) | ||
Theorem | altgsumbcALT 41924* | Alternate proof of altgsumbc 41923, using Pascal's rule (bcpascm1 41922) instead of the binomial theorem (binom 14401). (Contributed by AV, 8-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0) | ||
Theorem | zlmodzxzlmod 41925 | The ℤ-module ℤ × ℤ is a (left) module with the ring of integers as base set. (Contributed by AV, 20-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) ⇒ ⊢ (𝑍 ∈ LMod ∧ ℤring = (Scalar‘𝑍)) | ||
Theorem | zlmodzxzel 41926 | An element of the (base set of the) ℤ-module ℤ × ℤ. (Contributed by AV, 21-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → {〈0, 𝐴〉, 〈1, 𝐵〉} ∈ (Base‘𝑍)) | ||
Theorem | zlmodzxz0 41927 | The 0 of the ℤ-module ℤ × ℤ. (Contributed by AV, 20-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ 0 = {〈0, 0〉, 〈1, 0〉} ⇒ ⊢ 0 = (0g‘𝑍) | ||
Theorem | zlmodzxzscm 41928 | The scalar multiplication of the ℤ-module ℤ × ℤ. (Contributed by AV, 20-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ ∙ = ( ·𝑠 ‘𝑍) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∙ {〈0, 𝐵〉, 〈1, 𝐶〉}) = {〈0, (𝐴 · 𝐵)〉, 〈1, (𝐴 · 𝐶)〉}) | ||
Theorem | zlmodzxzadd 41929 | The addition of the ℤ-module ℤ × ℤ. (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ + = (+g‘𝑍) ⇒ ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → ({〈0, 𝐴〉, 〈1, 𝐶〉} + {〈0, 𝐵〉, 〈1, 𝐷〉}) = {〈0, (𝐴 + 𝐵)〉, 〈1, (𝐶 + 𝐷)〉}) | ||
Theorem | zlmodzxzsubm 41930 | The subtraction of the ℤ-module ℤ × ℤ expressed as addition. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ − = (-g‘𝑍) ⇒ ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → ({〈0, 𝐴〉, 〈1, 𝐶〉} − {〈0, 𝐵〉, 〈1, 𝐷〉}) = ({〈0, 𝐴〉, 〈1, 𝐶〉} (+g‘𝑍)(-1( ·𝑠 ‘𝑍){〈0, 𝐵〉, 〈1, 𝐷〉}))) | ||
Theorem | zlmodzxzsub 41931 | The subtraction of the ℤ-module ℤ × ℤ. (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ − = (-g‘𝑍) ⇒ ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → ({〈0, 𝐴〉, 〈1, 𝐶〉} − {〈0, 𝐵〉, 〈1, 𝐷〉}) = {〈0, (𝐴 − 𝐵)〉, 〈1, (𝐶 − 𝐷)〉}) | ||
Theorem | gsumpr 41932* | Group sum of a pair. (Contributed by AV, 6-Dec-2018.) (Proof shortened by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐶) & ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐷) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → (𝐺 Σg (𝑘 ∈ {𝑀, 𝑁} ↦ 𝐴)) = (𝐶 + 𝐷)) | ||
Theorem | mgpsumunsn 41933* | Extract a summand/factor from the group sum for the multiplicative group of a unital ring. (Contributed by AV, 29-Dec-2018.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁) → 𝐴 ∈ (Base‘𝑅)) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑅)) & ⊢ (𝑘 = 𝐼 → 𝐴 = 𝑋) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ 𝑁 ↦ 𝐴)) = ((𝑀 Σg (𝑘 ∈ (𝑁 ∖ {𝐼}) ↦ 𝐴)) · 𝑋)) | ||
Theorem | mgpsumz 41934* | If the group sum for the multiplicative group of a unital ring contains a summand/factor that is the zero of the ring, the group sum itself is zero. (Contributed by AV, 29-Dec-2018.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁) → 𝐴 ∈ (Base‘𝑅)) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝑘 = 𝐼 → 𝐴 = 0 ) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ 𝑁 ↦ 𝐴)) = 0 ) | ||
Theorem | mgpsumn 41935* | If the group sum for the multiplicative group of a unital ring contains a summand/factor that is the one of the ring, this summand/ factor can be removed from the group sum. (Contributed by AV, 29-Dec-2018.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁) → 𝐴 ∈ (Base‘𝑅)) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝑘 = 𝐼 → 𝐴 = 1 ) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ 𝑁 ↦ 𝐴)) = (𝑀 Σg (𝑘 ∈ (𝑁 ∖ {𝐼}) ↦ 𝐴))) | ||
Theorem | gsumsplit2f 41936* | Split a group sum into two parts. (Contributed by AV, 4-Sep-2019.) |
⊢ Ⅎ𝑘𝜑 & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷)) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋)) + (𝐺 Σg (𝑘 ∈ 𝐷 ↦ 𝑋)))) | ||
Theorem | gsumdifsndf 41937* | Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019.) |
⊢ Ⅎ𝑘𝑌 & ⊢ Ⅎ𝑘𝜑 & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp (0g‘𝐺)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ (𝐴 ∖ {𝑀}) ↦ 𝑋)) + 𝑌)) | ||
Theorem | nn0le2is012 41938 | A nonnegative integer which is less than or equal to 2 is either 0 or 1 or 2. (Contributed by AV, 16-Mar-2019.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 2) → (𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2)) | ||
Theorem | exple2lt6 41939 | A nonnegative integer to the power of itself is less than 6 if it is less than or equal to 2. (Contributed by AV, 16-Mar-2019.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 2) → (𝑁↑𝑁) < 6) | ||
Theorem | pgrple2abl 41940 | Every symmetric group on a set with at most 2 elements is abelian. (Contributed by AV, 16-Mar-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ (#‘𝐴) ≤ 2) → 𝐺 ∈ Abel) | ||
Theorem | pgrpgt2nabl 41941 | Every symmetric group on a set with more than 2 elements is not abelian, see also the remark in [Rotman] p. 28. (Contributed by AV, 21-Mar-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (#‘𝐴)) → 𝐺 ∉ Abel) | ||
Theorem | invginvrid 41942 | Identity for a multiplication with additive and multiplicative inverses in a ring. (Contributed by AV, 18-May-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑁‘𝑌) · ((𝐼‘(𝑁‘𝑌)) · 𝑋)) = 𝑋) | ||
Theorem | rmsupp0 41943* | The support of a mapping of a multiplication of zero with a function into a ring is empty. (Contributed by AV, 10-Apr-2019.) |
⊢ 𝑅 = (Base‘𝑀) ⇒ ⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) = ∅) | ||
Theorem | domnmsuppn0 41944* | The support of a mapping of a multiplication of a nonzero constant with a function into a (ring theoretic) domain equals the support of the function. (Contributed by AV, 11-Apr-2019.) |
⊢ 𝑅 = (Base‘𝑀) ⇒ ⊢ (((𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋) ∧ (𝐶 ∈ 𝑅 ∧ 𝐶 ≠ (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) = (𝐴 supp (0g‘𝑀))) | ||
Theorem | rmsuppss 41945* | The support of a mapping of a multiplication of a constant with a function into a ring is a subset of the support of the function. (Contributed by AV, 11-Apr-2019.) |
⊢ 𝑅 = (Base‘𝑀) ⇒ ⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) ⊆ (𝐴 supp (0g‘𝑀))) | ||
Theorem | mndpsuppss 41946 | The support of a mapping of a scalar multiplication with a function of scalars is a subset of the support of the function of scalars. (Contributed by AV, 5-Apr-2019.) |
⊢ 𝑅 = (Base‘𝑀) ⇒ ⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝐴 ∘𝑓 (+g‘𝑀)𝐵) supp (0g‘𝑀)) ⊆ ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀)))) | ||
Theorem | scmsuppss 41947* | The support of a mapping of a scalar multiplication with a function of scalars is a subset of the support of the function of scalars. (Contributed by AV, 5-Apr-2019.) |
⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠 ‘𝑀)𝑣)) supp (0g‘𝑀)) ⊆ (𝐴 supp (0g‘𝑆))) | ||
Theorem | rmsuppfi 41948* | The support of a mapping of a multiplication of a constant with a function into a ring is finite if the support of the function is finite. (Contributed by AV, 11-Apr-2019.) |
⊢ 𝑅 = (Base‘𝑀) ⇒ ⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝐴 supp (0g‘𝑀)) ∈ Fin) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) ∈ Fin) | ||
Theorem | rmfsupp 41949* | A mapping of a multiplication of a constant with a function into a ring is finitely supported if the function is finitely supported. (Contributed by AV, 9-Jun-2019.) |
⊢ 𝑅 = (Base‘𝑀) ⇒ ⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐴 finSupp (0g‘𝑀)) → (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) finSupp (0g‘𝑀)) | ||
Theorem | mndpsuppfi 41950 | The support of a mapping of a scalar multiplication with a function of scalars is finite if the support of the function of scalars is finite. (Contributed by AV, 5-Apr-2019.) |
⊢ 𝑅 = (Base‘𝑀) ⇒ ⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ ((𝐴 supp (0g‘𝑀)) ∈ Fin ∧ (𝐵 supp (0g‘𝑀)) ∈ Fin)) → ((𝐴 ∘𝑓 (+g‘𝑀)𝐵) supp (0g‘𝑀)) ∈ Fin) | ||
Theorem | mndpfsupp 41951 | A mapping of a scalar multiplication with a function of scalars is finitely supported if the function of scalars is finitely supported. (Contributed by AV, 9-Jun-2019.) |
⊢ 𝑅 = (Base‘𝑀) ⇒ ⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑀) ∧ 𝐵 finSupp (0g‘𝑀))) → (𝐴 ∘𝑓 (+g‘𝑀)𝐵) finSupp (0g‘𝑀)) | ||
Theorem | scmsuppfi 41952* | The support of a mapping of a scalar multiplication with a function of scalars is finite if the support of the function of scalars is finite. (Contributed by AV, 5-Apr-2019.) |
⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝐴 supp (0g‘𝑆)) ∈ Fin) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠 ‘𝑀)𝑣)) supp (0g‘𝑀)) ∈ Fin) | ||
Theorem | scmfsupp 41953* | A mapping of a scalar multiplication with a function of scalars is finitely supported if the function of scalars is finitely supported. (Contributed by AV, 9-Jun-2019.) |
⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐴 finSupp (0g‘𝑆)) → (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠 ‘𝑀)𝑣)) finSupp (0g‘𝑀)) | ||
Theorem | suppmptcfin 41954* | The support of a mapping with value 0 except of one is finite. (Contributed by AV, 27-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑋, 1 , 0 )) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝐹 supp 0 ) ∈ Fin) | ||
Theorem | mptcfsupp 41955* | A mapping with value 0 except of one is finitely supported. (Contributed by AV, 9-Jun-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑋, 1 , 0 )) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → 𝐹 finSupp 0 ) | ||
Theorem | fsuppmptdmf 41956* | A mapping with a finite domain is finitely supported. (Contributed by AV, 4-Sep-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑌) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | lmodvsmdi 41957 | Multiple distributive law for scalar product (left-distributivity). (Contributed by AV, 5-Sep-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ↑ = (.g‘𝑊) & ⊢ 𝐸 = (.g‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋)) | ||
Theorem | gsumlsscl 41958* | Closure of a group sum in a linear subspace: A (finitely supported) sum of scalar multiplications of vectors of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ 𝑆 = (LSubSp‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → ((𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅)) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠 ‘𝑀)𝑣))) ∈ 𝑍)) | ||
Theorem | ascl0 41959 | 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 41960 | 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 | assaascl0 41961 | The scalar 0 embedded into an associative algebra corresponds to the 0 of the associative algebra. (Contributed by AV, 31-Jul-2019.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) ⇒ ⊢ (𝜑 → (𝐴‘(0g‘𝐹)) = (0g‘𝑊)) | ||
Theorem | assaascl1 41962 | The scalar 1 embedded into an associative algebra corresponds to the 1 of the an associative algebra. (Contributed by AV, 31-Jul-2019.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) ⇒ ⊢ (𝜑 → (𝐴‘(1r‘𝐹)) = (1r‘𝑊)) | ||
Theorem | ply1vr1smo 41963 | The variable in a polynomial expressed as scaled monomial. (Contributed by AV, 12-Aug-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝑋 = (var1‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → ( 1 · (1 ↑ 𝑋)) = 𝑋) | ||
Theorem | ply1ass23l 41964 | Associative identity with scalar and ring multiplication for the polynomial ring. (Contributed by AV, 14-Aug-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌))) | ||
Theorem | ply1sclrmsm 41965 | The ring multiplication of a polynomial with a scalar polynomial is equal to the scalar multiplication of the polynomial with the corresponding scalar. (Contributed by AV, 14-Aug-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐸 = (Base‘𝑃) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ × = (.r‘𝑃) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝑍 ∈ 𝐸) → ((𝐴‘𝐹) × 𝑍) = (𝐹 · 𝑍)) | ||
Theorem | coe1id 41966* | Coefficient vector of the unit polynomial. (Contributed by AV, 9-Aug-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐼 = (1r‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (coe1‘𝐼) = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, 1 , 0 ))) | ||
Theorem | coe1sclmulval 41967 | The value of the coefficient vector of a polynomial multiplied on the left by a scalar. (Contributed by AV, 14-Aug-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝑆 = ( ·𝑠 ‘𝑃) & ⊢ ∙ = (.r‘𝑃) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) → ((coe1‘(𝑌𝑆𝑍))‘𝑁) = (𝑌 · ((coe1‘𝑍)‘𝑁))) | ||
Theorem | ply1mulgsumlem1 41968* | Lemma 1 for ply1mulgsum 41972. (Contributed by AV, 19-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (coe1‘𝐾) & ⊢ 𝐶 = (coe1‘𝐿) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅)))) | ||
Theorem | ply1mulgsumlem2 41969* | Lemma 2 for ply1mulgsum 41972. (Contributed by AV, 19-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (coe1‘𝐾) & ⊢ 𝐶 = (coe1‘𝐿) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅))) | ||
Theorem | ply1mulgsumlem3 41970* | Lemma 3 for ply1mulgsum 41972. (Contributed by AV, 20-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (coe1‘𝐾) & ⊢ 𝐶 = (coe1‘𝐿) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))))) finSupp (0g‘𝑅)) | ||
Theorem | ply1mulgsumlem4 41971* | Lemma 4 for ply1mulgsum 41972. (Contributed by AV, 19-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (coe1‘𝐾) & ⊢ 𝐶 = (coe1‘𝐿) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑃)) | ||
Theorem | ply1mulgsum 41972* | The product of two polynomials expressed as group sum of scaled monomials. (Contributed by AV, 20-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (coe1‘𝐾) & ⊢ 𝐶 = (coe1‘𝐿) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝐾 × 𝐿) = (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))))) | ||
Theorem | evl1at0 41973 | Polynomial evaluation for the 0 scalar. (Contributed by AV, 10-Aug-2019.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑃) ⇒ ⊢ (𝑅 ∈ CRing → ((𝑂‘𝑍)‘ 0 ) = 0 ) | ||
Theorem | evl1at1 41974 | Polynomial evaluation for the 1 scalar. (Contributed by AV, 10-Aug-2019.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐼 = (1r‘𝑃) ⇒ ⊢ (𝑅 ∈ CRing → ((𝑂‘𝐼)‘ 1 ) = 1 ) | ||
Theorem | linply1 41975 | A term of the form 𝑥 − 𝐶 is a (univariate) polynomial, also called "linear polynomial". (Part of ply1remlem 23726). (Contributed by AV, 3-Jul-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐵) | ||
Theorem | lineval 41976 | A term of the form 𝑥 − 𝐶 evaluated for 𝑥 = 𝑉 results in 𝑉 − 𝐶 (part of ply1remlem 23726). (Contributed by AV, 3-Jul-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑉 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑂‘𝐺)‘𝑉) = (𝑉(-g‘𝑅)𝐶)) | ||
Theorem | zringsubgval 41977 | Subtraction in the ring of integers. (Contributed by AV, 3-Aug-2019.) |
⊢ − = (-g‘ℤring) ⇒ ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑋 − 𝑌) = (𝑋 − 𝑌)) | ||
Theorem | linevalexample 41978 | The polynomial 𝑥 − 3 over ℤ evaluated for 𝑥 = 5 results in 2. (Contributed by AV, 3-Jul-2019.) |
⊢ 𝑃 = (Poly1‘ℤring) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑋 = (var1‘ℤring) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘3)) & ⊢ 𝑂 = (eval1‘ℤring) ⇒ ⊢ ((𝑂‘(𝑋 − (𝐴‘3)))‘5) = 2 | ||
In the following, alternative definitions for diagonal and scalar matrices are provided. These definitions define diagonal and scalar matrices as extensible structures, whereas the definitions df-dmat 20115 and df-scmat 20116 define diagonal and scalar matrices as sets. | ||
Syntax | cdmatalt 41979 | Alternative notation for the algebra of diagonal matrices. |
class DMatALT | ||
Syntax | cscmatalt 41980 | Alternative notation for the algebra of scalar matrices. |
class ScMatALT | ||
Definition | df-dmatalt 41981* | Define the set of n x n diagonal (square) matrices over a set (usually a ring) r, see definition in [Roman] p. 4 or Definition 3.12 in [Hefferon] p. 240. (Contributed by AV, 8-Dec-2019.) |
⊢ DMatALT = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌(𝑎 ↾s {𝑚 ∈ (Base‘𝑎) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))})) | ||
Definition | df-scmatalt 41982* | Define the algebra of n x n scalar matrices over a set (usually a ring) r, see definition in [Connell] p. 57: "A scalar matrix is a diagonal matrix for which all the diagonal terms are equal, i.e., a matrix of the form cIn". (Contributed by AV, 8-Dec-2019.) |
⊢ ScMatALT = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌(𝑎 ↾s {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑟))})) | ||
Theorem | dmatALTval 41983* | The algebra of 𝑁 x 𝑁 diagonal matrices over a ring 𝑅. (Contributed by AV, 8-Dec-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐷 = (𝑁 DMatALT 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐷 = (𝐴 ↾s {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 )})) | ||
Theorem | dmatALTbas 41984* | The base set of the algebra of 𝑁 x 𝑁 diagonal matrices over a ring 𝑅, i.e. the set of all 𝑁 x 𝑁 diagonal matrices over the ring 𝑅. (Contributed by AV, 8-Dec-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐷 = (𝑁 DMatALT 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (Base‘𝐷) = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 )}) | ||
Theorem | dmatALTbasel 41985* | An element of the base set of the algebra of 𝑁 x 𝑁 diagonal matrices over a ring 𝑅, i.e. an 𝑁 x 𝑁 diagonal matrix over the ring 𝑅. (Contributed by AV, 8-Dec-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐷 = (𝑁 DMatALT 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (𝑀 ∈ (Base‘𝐷) ↔ (𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )))) | ||
Theorem | dmatbas 41986 | The set of all 𝑁 x 𝑁 diagonal matrices over (the ring) 𝑅 is the base set of the algebra of 𝑁 x 𝑁 diagonal matrices over (the ring) 𝑅. (Contributed by AV, 8-Dec-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐷 = (𝑁 DMat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐷 = (Base‘(𝑁 DMatALT 𝑅))) | ||
According to Wikipedia ("Linear combination", 29-Mar-2019,
https://en.wikipedia.org/wiki/Linear_combination) "In mathematics, a
linear combination is an expression constructed from a set of terms by
multiplying each term by a constant and adding the results (e.g., a linear
combination of x and y would be any expression of the form ax + by, where a and
b are constants). The concept of linear combinations is central to linear
algebra and related fields of mathematics." In linear algebra, these "terms"
are "vectors" (elements from vector spaces or left modules), and the constants
are elements of the underlying field resp. ring. This corresponds to the
definition in [Lang] p. 129: "Let M be a module over a ring A and let S be a
subset of M. By a linear combination of elements of S (with
coefficients in A) one means a sum ∑x ∈S
axx where {ax} is a set of elements of A, ...". In the
definition in [Lang] p. 129, it is additionally claimed that "..., almost all
of which [elements of A] are equal to 0.". This is not necessarily required in
the following definition df-linc 41989, but it is essential if additions and
scalar multiplications of linear combinations are considered. Therefore, we
define the set of all linear combinations with finite support in df-lco 41990, so
that we can show that such sets are submodules of the corresponding modules,
see lincolss 42017.
| ||
Syntax | clinc 41987 | Extend class notation with the operation constructing a linear combination (of vectors from a left module). |
class linC | ||
Syntax | clinco 41988 | Extend class notation with the operation constructing a set of linear combinations (of vectors from a left module) with finite support. |
class LinCo | ||
Definition | df-linc 41989* | Define the operation constructing a linear combination. Although this definition is taylored for linear combinations of vectors from left modules, it can be used for any structure having a Base, Scalar s and a scalar multiplication ·𝑠. (Contributed by AV, 29-Mar-2019.) |
⊢ linC = (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥))))) | ||
Definition | df-lco 41990* | Define the operation constructing the set of all linear combinations for a set of vectors. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ LinCo = (𝑚 ∈ V, 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))}) | ||
Theorem | lincop 41991* | A linear combination as operation. (Contributed by AV, 30-Mar-2019.) |
⊢ (𝑀 ∈ 𝑋 → ( linC ‘𝑀) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑀)𝑥))))) | ||
Theorem | lincval 41992* | The value of a linear combination. (Contributed by AV, 30-Mar-2019.) |
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝑆( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝑆‘𝑥)( ·𝑠 ‘𝑀)𝑥)))) | ||
Theorem | dflinc2 41993* | Alternative definition of linear combinations using the function operation. (Contributed by AV, 1-Apr-2019.) |
⊢ linC = (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑠 ∘𝑓 ( ·𝑠 ‘𝑚)( I ↾ 𝑣))))) | ||
Theorem | lcoop 41994* | A linear combination as operation. (Contributed by AV, 5-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) ⇒ ⊢ ((𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 LinCo 𝑉) = {𝑐 ∈ 𝐵 ∣ ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉))}) | ||
Theorem | lcoval 41995* | The value of a linear combination. (Contributed by AV, 5-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) ⇒ ⊢ ((𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐶 ∈ (𝑀 LinCo 𝑉) ↔ (𝐶 ∈ 𝐵 ∧ ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝐶 = (𝑠( linC ‘𝑀)𝑉))))) | ||
Theorem | lincfsuppcl 41996 | A linear combination of vectors (with finite support) is a vector. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝑆 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑𝑚 𝑉) ∧ 𝐹 finSupp 0 )) → (𝐹( linC ‘𝑀)𝑉) ∈ 𝐵) | ||
Theorem | linccl 41997 | A linear combination of vectors is a vector. (Contributed by AV, 31-Mar-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Base‘(Scalar‘𝑀)) ⇒ ⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑆( linC ‘𝑀)𝑉) ∈ 𝐵) | ||
Theorem | lincval0 41998 | The value of an empty linear combination. (Contributed by AV, 12-Apr-2019.) |
⊢ (𝑀 ∈ 𝑋 → (∅( linC ‘𝑀)∅) = (0g‘𝑀)) | ||
Theorem | lincvalsng 41999 | The linear combination over a singleton. (Contributed by AV, 25-May-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → ({〈𝑉, 𝑌〉} ( linC ‘𝑀){𝑉}) = (𝑌 · 𝑉)) | ||
Theorem | lincvalsn 42000 | The linear combination over a singleton. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 25-May-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 𝐹 = {〈𝑉, 𝑌〉} ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → (𝐹( linC ‘𝑀){𝑉}) = (𝑌 · 𝑉)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |