![]() |
Metamath
Proof Explorer Theorem List (p. 483 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | zlmodzxzscm 48201 | 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 48202 | 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 48203 | 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 48204 | 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 48205* | 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 48206* | 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 48207* | 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 48208 | 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 48209 | Every symmetric group on a set with at most 2 elements is abelian. (Contributed by AV, 16-Mar-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ (♯‘𝐴) ≤ 2) → 𝐺 ∈ Abel) | ||
Theorem | pgrpgt2nabl 48210 | 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 48211 | 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 48212* | 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 48213* | 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 48214* | 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 | scmsuppss 48215* | 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 48216* | 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 48217* | 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 | scmsuppfi 48218* | 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 48219* | 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 48220* | 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 48221* | 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 48222* | A mapping with a finite domain is finitely supported. (Contributed by AV, 4-Sep-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑌) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | lmodvsmdi 48223 | Multiple distributive law for scalar product (left-distributivity). (Contributed by AV, 5-Sep-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ↑ = (.g‘𝑊) & ⊢ 𝐸 = (.g‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋)) | ||
Theorem | gsumlsscl 48224* | 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 48225 | 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 48226 | 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 48227 | 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 | ply1sclrmsm 48228 | 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 48229* | 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 48230 | 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 48231* | Lemma 1 for ply1mulgsum 48235. (Contributed by AV, 19-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (coe1‘𝐾) & ⊢ 𝐶 = (coe1‘𝐿) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅)))) | ||
Theorem | ply1mulgsumlem2 48232* | Lemma 2 for ply1mulgsum 48235. (Contributed by AV, 19-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (coe1‘𝐾) & ⊢ 𝐶 = (coe1‘𝐿) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅))) | ||
Theorem | ply1mulgsumlem3 48233* | Lemma 3 for ply1mulgsum 48235. (Contributed by AV, 20-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (coe1‘𝐾) & ⊢ 𝐶 = (coe1‘𝐿) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))))) finSupp (0g‘𝑅)) | ||
Theorem | ply1mulgsumlem4 48234* | Lemma 4 for ply1mulgsum 48235. (Contributed by AV, 19-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (coe1‘𝐾) & ⊢ 𝐶 = (coe1‘𝐿) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑃)) | ||
Theorem | ply1mulgsum 48235* | 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 48236 | Polynomial evaluation for the 0 scalar. (Contributed by AV, 10-Aug-2019.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑃) ⇒ ⊢ (𝑅 ∈ CRing → ((𝑂‘𝑍)‘ 0 ) = 0 ) | ||
Theorem | evl1at1 48237 | Polynomial evaluation for the 1 scalar. (Contributed by AV, 10-Aug-2019.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐼 = (1r‘𝑃) ⇒ ⊢ (𝑅 ∈ CRing → ((𝑂‘𝐼)‘ 1 ) = 1 ) | ||
Theorem | linply1 48238 | A term of the form 𝑥 − 𝐶 is a (univariate) polynomial, also called "linear polynomial". (Part of ply1remlem 26218). (Contributed by AV, 3-Jul-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐵) | ||
Theorem | lineval 48239 | A term of the form 𝑥 − 𝐶 evaluated for 𝑥 = 𝑉 results in 𝑉 − 𝐶 (part of ply1remlem 26218). (Contributed by AV, 3-Jul-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑉 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑂‘𝐺)‘𝑉) = (𝑉(-g‘𝑅)𝐶)) | ||
Theorem | linevalexample 48240 | 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 22511 and df-scmat 22512 define diagonal and scalar matrices as sets. | ||
Syntax | cdmatalt 48241 | Alternative notation for the algebra of diagonal matrices. |
class DMatALT | ||
Syntax | cscmatalt 48242 | Alternative notation for the algebra of scalar matrices. |
class ScMatALT | ||
Definition | df-dmatalt 48243* | 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 48244* | 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 48245* | 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 48246* | 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 48247* | 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 48248 | 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 48251, 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 48252,
so that we can show that such sets are submodules of the corresponding
modules, see lincolss 48279.
| ||
Syntax | clinc 48249 | Extend class notation with the operation constructing a linear combination (of vectors from a left module). |
class linC | ||
Syntax | clinco 48250 | 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 48251* | 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 48252* | 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 48253* | A linear combination as operation. (Contributed by AV, 30-Mar-2019.) |
⊢ (𝑀 ∈ 𝑋 → ( linC ‘𝑀) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑀)𝑥))))) | ||
Theorem | lincval 48254* | The value of a linear combination. (Contributed by AV, 30-Mar-2019.) |
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝑆( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝑆‘𝑥)( ·𝑠 ‘𝑀)𝑥)))) | ||
Theorem | dflinc2 48255* | 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 48256* | 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 48257* | 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 48258 | 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 48259 | A linear combination of vectors is a vector. (Contributed by AV, 31-Mar-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Base‘(Scalar‘𝑀)) ⇒ ⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑m 𝑉))) → (𝑆( linC ‘𝑀)𝑉) ∈ 𝐵) | ||
Theorem | lincval0 48260 | The value of an empty linear combination. (Contributed by AV, 12-Apr-2019.) |
⊢ (𝑀 ∈ 𝑋 → (∅( linC ‘𝑀)∅) = (0g‘𝑀)) | ||
Theorem | lincvalsng 48261 | The linear combination over a singleton. (Contributed by AV, 25-May-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → ({〈𝑉, 𝑌〉} ( linC ‘𝑀){𝑉}) = (𝑌 · 𝑉)) | ||
Theorem | lincvalsn 48262 | 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 48263 | The linear combination over an unordered pair. (Contributed by AV, 16-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝐹 = {〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉} ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = ((𝑋 · 𝑉) + (𝑌 · 𝑊))) | ||
Theorem | lincval1 48264 | The linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐹 = {〈𝑉, (0g‘𝑆)〉} ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵) → (𝐹( linC ‘𝑀){𝑉}) = (0g‘𝑀)) | ||
Theorem | lcosn0 48265 | 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 48266* | The linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ 0 ) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹( linC ‘𝑀)𝑉) = 𝑍) | ||
Theorem | lcoc0 48267* | 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 48268* | 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 48269 | 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 48270* | 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 48271 | 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 48272 | 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 48273 | 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 48274 | 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 48275* | 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 48276 | 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 48277 | 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 48278 | 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 48279 | 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 48280* | 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 48281 | 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 48282 | Lemma for lspeqlco 48284. (Contributed by AV, 17-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → ((LSpan‘𝑀)‘𝑉) ⊆ (𝑀 LinCo 𝑉)) | ||
Theorem | lcosslsp 48283 | Lemma for lspeqlco 48284. (Contributed by AV, 20-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 LinCo 𝑉) ⊆ ((LSpan‘𝑀)‘𝑉)) | ||
Theorem | lspeqlco 48284 | 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 20987) 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 48287 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 48285 | Extend class notation with the relation between a module and its linearly independent subsets. |
class linIndS | ||
Syntax | clindeps 48286 | Extend class notation with the relation between a module and its linearly dependent subsets. |
class linDepS | ||
Definition | df-lininds 48287* | Define the relation between a module and its linearly independent subsets. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 24-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ linIndS = {〈𝑠, 𝑚〉 ∣ (𝑠 ∈ 𝒫 (Base‘𝑚) ∧ ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑠)((𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚)) → ∀𝑥 ∈ 𝑠 (𝑓‘𝑥) = (0g‘(Scalar‘𝑚))))} | ||
Theorem | rellininds 48288 | The class defining the relation between a module and its linearly independent subsets is a relation. (Contributed by AV, 13-Apr-2019.) |
⊢ Rel linIndS | ||
Definition | df-lindeps 48289* | Define the relation between a module and its linearly dependent subsets. (Contributed by AV, 26-Apr-2019.) |
⊢ linDepS = {〈𝑠, 𝑚〉 ∣ ¬ 𝑠 linIndS 𝑚} | ||
Theorem | linindsv 48290 | The classes of the module and its linearly independent subsets are sets. (Contributed by AV, 13-Apr-2019.) |
⊢ (𝑆 linIndS 𝑀 → (𝑆 ∈ V ∧ 𝑀 ∈ V)) | ||
Theorem | islininds 48291* | The property of being a linearly independent subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → (𝑆 linIndS 𝑀 ↔ (𝑆 ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )))) | ||
Theorem | linindsi 48292* | The implications of being a linearly independent subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑆 linIndS 𝑀 → (𝑆 ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) | ||
Theorem | linindslinci 48293* | The implications of being a linearly independent subset and a linear combination of this subset being 0. (Contributed by AV, 24-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑆 linIndS 𝑀 ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ 𝐹 finSupp 0 ∧ (𝐹( linC ‘𝑀)𝑆) = 𝑍)) → ∀𝑥 ∈ 𝑆 (𝐹‘𝑥) = 0 ) | ||
Theorem | islinindfis 48294* | The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊) → (𝑆 linIndS 𝑀 ↔ (𝑆 ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓( linC ‘𝑀)𝑆) = 𝑍 → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )))) | ||
Theorem | islinindfiss 48295* | The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝑊 ∧ 𝑆 ∈ Fin ∧ 𝑆 ∈ 𝒫 𝐵) → (𝑆 linIndS 𝑀 ↔ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓( linC ‘𝑀)𝑆) = 𝑍 → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) | ||
Theorem | linindscl 48296 | A linearly independent set is a subset of (the base set of) a module. (Contributed by AV, 13-Apr-2019.) |
⊢ (𝑆 linIndS 𝑀 → 𝑆 ∈ 𝒫 (Base‘𝑀)) | ||
Theorem | lindepsnlininds 48297 | A linearly dependent subset is not a linearly independent subset. (Contributed by AV, 26-Apr-2019.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → (𝑆 linDepS 𝑀 ↔ ¬ 𝑆 linIndS 𝑀)) | ||
Theorem | islindeps 48298* | The property of being a linearly dependent subset. (Contributed by AV, 26-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵) → (𝑆 linDepS 𝑀 ↔ ∃𝑓 ∈ (𝐸 ↑m 𝑆)(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍 ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠ 0 ))) | ||
Theorem | lincext1 48299* | Property 1 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 29-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐹 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑋, (𝑁‘𝑌), (𝐺‘𝑧))) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑m (𝑆 ∖ {𝑋})))) → 𝐹 ∈ (𝐸 ↑m 𝑆)) | ||
Theorem | lincext2 48300* | Property 2 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐹 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑋, (𝑁‘𝑌), (𝐺‘𝑧))) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑m (𝑆 ∖ {𝑋}))) ∧ 𝐺 finSupp 0 ) → 𝐹 finSupp 0 ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |