![]() |
Metamath
Proof Explorer Theorem List (p. 452 of 457) | < 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-28785) |
![]() (28786-30308) |
![]() (30309-45683) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ztprmneprm 45101 | A prime is not an integer multiple of another prime. (Contributed by AV, 23-May-2019.) |
⊢ ((𝑍 ∈ ℤ ∧ 𝐴 ∈ ℙ ∧ 𝐵 ∈ ℙ) → ((𝑍 · 𝐴) = 𝐵 → 𝐴 = 𝐵)) | ||
Theorem | 2t6m3t4e0 45102 | 2 times 6 minus 3 times 4 equals 0. (Contributed by AV, 24-May-2019.) |
⊢ ((2 · 6) − (3 · 4)) = 0 | ||
Theorem | ssnn0ssfz 45103* | For any finite subset of ℕ0, find a superset in the form of a set of sequential integers, analogous to ssnnssfz 30617. (Contributed by AV, 30-Sep-2019.) |
⊢ (𝐴 ∈ (𝒫 ℕ0 ∩ Fin) → ∃𝑛 ∈ ℕ0 𝐴 ⊆ (0...𝑛)) | ||
Theorem | nn0sumltlt 45104 | 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 45105 | 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 45106* | 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 45105) instead of the binomial theorem (binom 15218) , see altgsumbcALT 45107. (Contributed by AV, 13-Sep-2019.) |
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0) | ||
Theorem | altgsumbcALT 45107* | Alternate proof of altgsumbc 45106, using Pascal's rule (bcpascm1 45105) instead of the binomial theorem (binom 15218). (Contributed by AV, 8-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0) | ||
Theorem | zlmodzxzlmod 45108 | 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 45109 | 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 45110 | 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 45111 | 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 45112 | 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 45113 | 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 45114 | 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 | mgpsumunsn 45115* | 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 45116* | 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 45117* | 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 | exple2lt6 45118 | 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 45119 | Every symmetric group on a set with at most 2 elements is abelian. (Contributed by AV, 16-Mar-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ (♯‘𝐴) ≤ 2) → 𝐺 ∈ Abel) | ||
Theorem | pgrpgt2nabl 45120 | 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 45121 | 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 45122* | 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‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) = ∅) | ||
Theorem | domnmsuppn0 45123* | 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‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) = (𝐴 supp (0g‘𝑀))) | ||
Theorem | rmsuppss 45124* | 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 ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) ⊆ (𝐴 supp (0g‘𝑀))) | ||
Theorem | mndpsuppss 45125 | 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 ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → ((𝐴 ∘f (+g‘𝑀)𝐵) supp (0g‘𝑀)) ⊆ ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀)))) | ||
Theorem | scmsuppss 45126* | 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‘𝑀) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉)) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠 ‘𝑀)𝑣)) supp (0g‘𝑀)) ⊆ (𝐴 supp (0g‘𝑆))) | ||
Theorem | rmsuppfi 45127* | 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 ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉) ∧ (𝐴 supp (0g‘𝑀)) ∈ Fin) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) ∈ Fin) | ||
Theorem | rmfsupp 45128* | 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 ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐴 finSupp (0g‘𝑀)) → (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) finSupp (0g‘𝑀)) | ||
Theorem | mndpsuppfi 45129 | 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 ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ ((𝐴 supp (0g‘𝑀)) ∈ Fin ∧ (𝐵 supp (0g‘𝑀)) ∈ Fin)) → ((𝐴 ∘f (+g‘𝑀)𝐵) supp (0g‘𝑀)) ∈ Fin) | ||
Theorem | mndpfsupp 45130 | 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 ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑀) ∧ 𝐵 finSupp (0g‘𝑀))) → (𝐴 ∘f (+g‘𝑀)𝐵) finSupp (0g‘𝑀)) | ||
Theorem | scmsuppfi 45131* | 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‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉) ∧ (𝐴 supp (0g‘𝑆)) ∈ Fin) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠 ‘𝑀)𝑣)) supp (0g‘𝑀)) ∈ Fin) | ||
Theorem | scmfsupp 45132* | 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‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐴 finSupp (0g‘𝑆)) → (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠 ‘𝑀)𝑣)) finSupp (0g‘𝑀)) | ||
Theorem | suppmptcfin 45133* | 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 45134* | 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 45135* | A mapping with a finite domain is finitely supported. (Contributed by AV, 4-Sep-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑌) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | lmodvsmdi 45136 | Multiple distributive law for scalar product (left-distributivity). (Contributed by AV, 5-Sep-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ↑ = (.g‘𝑊) & ⊢ 𝐸 = (.g‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋)) | ||
Theorem | gsumlsscl 45137* | 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 ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → ((𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅)) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠 ‘𝑀)𝑣))) ∈ 𝑍)) | ||
Theorem | assaascl0 45138 | 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 45139 | 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 45140 | 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 45141 | Associative identity with scalar and ring multiplication for the polynomial ring. (Contributed by AV, 14-Aug-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌))) | ||
Theorem | ply1sclrmsm 45142 | 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 45143* | 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 45144 | 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 45145* | Lemma 1 for ply1mulgsum 45149. (Contributed by AV, 19-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (coe1‘𝐾) & ⊢ 𝐶 = (coe1‘𝐿) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅)))) | ||
Theorem | ply1mulgsumlem2 45146* | Lemma 2 for ply1mulgsum 45149. (Contributed by AV, 19-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (coe1‘𝐾) & ⊢ 𝐶 = (coe1‘𝐿) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅))) | ||
Theorem | ply1mulgsumlem3 45147* | Lemma 3 for ply1mulgsum 45149. (Contributed by AV, 20-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (coe1‘𝐾) & ⊢ 𝐶 = (coe1‘𝐿) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))))) finSupp (0g‘𝑅)) | ||
Theorem | ply1mulgsumlem4 45148* | Lemma 4 for ply1mulgsum 45149. (Contributed by AV, 19-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (coe1‘𝐾) & ⊢ 𝐶 = (coe1‘𝐿) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑃)) | ||
Theorem | ply1mulgsum 45149* | 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 45150 | Polynomial evaluation for the 0 scalar. (Contributed by AV, 10-Aug-2019.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑃) ⇒ ⊢ (𝑅 ∈ CRing → ((𝑂‘𝑍)‘ 0 ) = 0 ) | ||
Theorem | evl1at1 45151 | Polynomial evaluation for the 1 scalar. (Contributed by AV, 10-Aug-2019.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐼 = (1r‘𝑃) ⇒ ⊢ (𝑅 ∈ CRing → ((𝑂‘𝐼)‘ 1 ) = 1 ) | ||
Theorem | linply1 45152 | A term of the form 𝑥 − 𝐶 is a (univariate) polynomial, also called "linear polynomial". (Part of ply1remlem 24847). (Contributed by AV, 3-Jul-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐵) | ||
Theorem | lineval 45153 | A term of the form 𝑥 − 𝐶 evaluated for 𝑥 = 𝑉 results in 𝑉 − 𝐶 (part of ply1remlem 24847). (Contributed by AV, 3-Jul-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑉 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑂‘𝐺)‘𝑉) = (𝑉(-g‘𝑅)𝐶)) | ||
Theorem | linevalexample 45154 | 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 Definitions df-dmat 21175 and df-scmat 21176 define diagonal and scalar matrices as sets. | ||
Syntax | cdmatalt 45155 | Alternative notation for the algebra of diagonal matrices. |
class DMatALT | ||
Syntax | cscmatalt 45156 | Alternative notation for the algebra of scalar matrices. |
class ScMatALT | ||
Definition | df-dmatalt 45157* | 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 45158* | 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 45159* | 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 45160* | 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 45161* | 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 45162 | 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 45165, 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 45166,
so that we can show that such sets are submodules of the corresponding
modules, see lincolss 45193.
| ||
Syntax | clinc 45163 | Extend class notation with the operation constructing a linear combination (of vectors from a left module). |
class linC | ||
Syntax | clinco 45164 | 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 45165* | 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‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥))))) | ||
Definition | df-lco 45166* | 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‘𝑚)) ↑m 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))}) | ||
Theorem | lincop 45167* | A linear combination as operation. (Contributed by AV, 30-Mar-2019.) |
⊢ (𝑀 ∈ 𝑋 → ( linC ‘𝑀) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑀)𝑥))))) | ||
Theorem | lincval 45168* | The value of a linear combination. (Contributed by AV, 30-Mar-2019.) |
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝑆( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝑆‘𝑥)( ·𝑠 ‘𝑀)𝑥)))) | ||
Theorem | dflinc2 45169* | Alternative definition of linear combinations using the function operation. (Contributed by AV, 1-Apr-2019.) |
⊢ linC = (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑠 ∘f ( ·𝑠 ‘𝑚)( I ↾ 𝑣))))) | ||
Theorem | lcoop 45170* | A linear combination as operation. (Contributed by AV, 5-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) ⇒ ⊢ ((𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 LinCo 𝑉) = {𝑐 ∈ 𝐵 ∣ ∃𝑠 ∈ (𝑅 ↑m 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉))}) | ||
Theorem | lcoval 45171* | The value of a linear combination. (Contributed by AV, 5-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) ⇒ ⊢ ((𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐶 ∈ (𝑀 LinCo 𝑉) ↔ (𝐶 ∈ 𝐵 ∧ ∃𝑠 ∈ (𝑅 ↑m 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝐶 = (𝑠( linC ‘𝑀)𝑉))))) | ||
Theorem | lincfsuppcl 45172 | 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 ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → (𝐹( linC ‘𝑀)𝑉) ∈ 𝐵) | ||
Theorem | linccl 45173 | A linear combination of vectors is a vector. (Contributed by AV, 31-Mar-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Base‘(Scalar‘𝑀)) ⇒ ⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑m 𝑉))) → (𝑆( linC ‘𝑀)𝑉) ∈ 𝐵) | ||
Theorem | lincval0 45174 | The value of an empty linear combination. (Contributed by AV, 12-Apr-2019.) |
⊢ (𝑀 ∈ 𝑋 → (∅( linC ‘𝑀)∅) = (0g‘𝑀)) | ||
Theorem | lincvalsng 45175 | The linear combination over a singleton. (Contributed by AV, 25-May-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → ({〈𝑉, 𝑌〉} ( linC ‘𝑀){𝑉}) = (𝑌 · 𝑉)) | ||
Theorem | lincvalsn 45176 | The linear combination over a singleton. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 25-May-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 𝐹 = {〈𝑉, 𝑌〉} ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → (𝐹( linC ‘𝑀){𝑉}) = (𝑌 · 𝑉)) | ||
Theorem | lincvalpr 45177 | The linear combination over an unordered pair. (Contributed by AV, 16-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝐹 = {〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉} ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = ((𝑋 · 𝑉) + (𝑌 · 𝑊))) | ||
Theorem | lincval1 45178 | The linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐹 = {〈𝑉, (0g‘𝑆)〉} ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵) → (𝐹( linC ‘𝑀){𝑉}) = (0g‘𝑀)) | ||
Theorem | lcosn0 45179 | Properties of a linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐹 = {〈𝑉, (0g‘𝑆)〉} ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵) → (𝐹 ∈ (𝑅 ↑m {𝑉}) ∧ 𝐹 finSupp (0g‘𝑆) ∧ (𝐹( linC ‘𝑀){𝑉}) = (0g‘𝑀))) | ||
Theorem | lincvalsc0 45180* | The linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ 0 ) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹( linC ‘𝑀)𝑉) = 𝑍) | ||
Theorem | lcoc0 45181* | Properties of a linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ 0 ) & ⊢ 𝑅 = (Base‘𝑆) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹 ∈ (𝑅 ↑m 𝑉) ∧ 𝐹 finSupp 0 ∧ (𝐹( linC ‘𝑀)𝑉) = 𝑍)) | ||
Theorem | linc0scn0 45182* | If a set contains the zero element of a module, there is a linear combination being 0 where not all scalars are 0. (Contributed by AV, 13-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ 1 = (1r‘𝑆) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑍, 1 , 0 )) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹( linC ‘𝑀)𝑉) = 𝑍) | ||
Theorem | lincdifsn 45183 | A vector is a linear combination of a set containing this vector. (Contributed by AV, 21-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝑆 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝐹( linC ‘𝑀)𝑉) = ((𝐺( linC ‘𝑀)(𝑉 ∖ {𝑋})) + ((𝐹‘𝑋) · 𝑋))) | ||
Theorem | linc1 45184* | A vector is a linear combination of a set containing this vector. (Contributed by AV, 18-Apr-2019.) (Proof shortened by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ 1 = (1r‘𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑋, 1 , 0 )) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝐹( linC ‘𝑀)𝑉) = 𝑋) | ||
Theorem | lincellss 45185 | A linear combination 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.) |
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) → ((𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝐹 finSupp (0g‘(Scalar‘𝑀))) → (𝐹( linC ‘𝑀)𝑉) ∈ 𝑆)) | ||
Theorem | lco0 45186 | The set of empty linear combinations over a monoid is the singleton with the identity element of the monoid. (Contributed by AV, 12-Apr-2019.) |
⊢ (𝑀 ∈ Mnd → (𝑀 LinCo ∅) = {(0g‘𝑀)}) | ||
Theorem | lcoel0 45187 | The zero vector is always a linear combination. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (0g‘𝑀) ∈ (𝑀 LinCo 𝑉)) | ||
Theorem | lincsum 45188 | The sum of two linear combinations is a linear combination, see also the proof in [Lang] p. 129. (Contributed by AV, 4-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ + = (+g‘𝑀) & ⊢ 𝑋 = (𝐴( linC ‘𝑀)𝑉) & ⊢ 𝑌 = (𝐵( linC ‘𝑀)𝑉) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ ✚ = (+g‘𝑆) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑋 + 𝑌) = ((𝐴 ∘f ✚ 𝐵)( linC ‘𝑀)𝑉)) | ||
Theorem | lincscm 45189* | A linear combinations multiplied with a scalar is a linear combination, see also the proof in [Lang] p. 129. (Contributed by AV, 9-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ ∙ = ( ·𝑠 ‘𝑀) & ⊢ · = (.r‘(Scalar‘𝑀)) & ⊢ 𝑋 = (𝐴( linC ‘𝑀)𝑉) & ⊢ 𝑅 = (Base‘(Scalar‘𝑀)) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ (𝑆 · (𝐴‘𝑥))) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp (0g‘(Scalar‘𝑀))) → (𝑆 ∙ 𝑋) = (𝐹( linC ‘𝑀)𝑉)) | ||
Theorem | lincsumcl 45190 | The sum of two linear combinations is a linear combination, see also the proof in [Lang] p. 129. (Contributed by AV, 4-Apr-2019.) (Proof shortened by AV, 28-Jul-2019.) |
⊢ + = (+g‘𝑀) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐶 ∈ (𝑀 LinCo 𝑉) ∧ 𝐷 ∈ (𝑀 LinCo 𝑉))) → (𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉)) | ||
Theorem | lincscmcl 45191 | The multiplication of a linear combination with a scalar is a linear combination, see also the proof in [Lang] p. 129. (Contributed by AV, 11-Apr-2019.) (Proof shortened by AV, 28-Jul-2019.) |
⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 𝑅 = (Base‘(Scalar‘𝑀)) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ (𝑀 LinCo 𝑉)) → (𝐶 · 𝐷) ∈ (𝑀 LinCo 𝑉)) | ||
Theorem | lincsumscmcl 45192 | The sum of a linear combination and a multiplication of a linear combination with a scalar is a linear combination. (Contributed by AV, 11-Apr-2019.) |
⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 𝑅 = (Base‘(Scalar‘𝑀)) & ⊢ + = (+g‘𝑀) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ (𝑀 LinCo 𝑉) ∧ 𝐵 ∈ (𝑀 LinCo 𝑉))) → ((𝐶 · 𝐷) + 𝐵) ∈ (𝑀 LinCo 𝑉)) | ||
Theorem | lincolss 45193 | According to the statement in [Lang] p. 129, the set (LSubSp‘𝑀) of all linear combinations of a set of vectors V is a submodule (generated by V) of the module M. The elements of V are called generators of (LSubSp‘𝑀). (Contributed by AV, 12-Apr-2019.) |
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝑀 LinCo 𝑉) ∈ (LSubSp‘𝑀)) | ||
Theorem | ellcoellss 45194* | Every linear combination of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) → ∀𝑥 ∈ (𝑀 LinCo 𝑉)𝑥 ∈ 𝑆) | ||
Theorem | lcoss 45195 | A set of vectors of a module is a subset of the set of all linear combinations of the set. (Contributed by AV, 18-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑉 ⊆ (𝑀 LinCo 𝑉)) | ||
Theorem | lspsslco 45196 | Lemma for lspeqlco 45198. (Contributed by AV, 17-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → ((LSpan‘𝑀)‘𝑉) ⊆ (𝑀 LinCo 𝑉)) | ||
Theorem | lcosslsp 45197 | Lemma for lspeqlco 45198. (Contributed by AV, 20-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 LinCo 𝑉) ⊆ ((LSpan‘𝑀)‘𝑉)) | ||
Theorem | lspeqlco 45198 | Equivalence of a span of a set of vectors of a left module defined as the intersection of all linear subspaces which each contain every vector in that set (see df-lsp 19797) and as the set of all linear combinations of the vectors of the set with finite support. (Contributed by AV, 20-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 LinCo 𝑉) = ((LSpan‘𝑀)‘𝑉)) | ||
According to the definition in [Lang] p. 129: "A subset S of a module M is said
to be linearly independent (over [the ring] A) if whenever we have a
linear combination ∑x ∈S axx which is equal to
0, then ax=0 for all x∈S." This definition does not care for
the finiteness of the set S (because the definition of a linear combination
in [Lang] p.129 does already assure that only a finite number of coefficients
can be 0 in the sum). Our definition df-lininds 45201 does also neither claim that
the subset must be finite, nor that almost all coefficients within the linear
combination are 0. If this is required, it must be explicitly stated as
precondition in the corresponding theorems. | ||
Syntax | clininds 45199 | Extend class notation with the relation between a module and its linearly independent subsets. |
class linIndS | ||
Syntax | clindeps 45200 | Extend class notation with the relation between a module and its linearly dependent subsets. |
class linDepS |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |