P. 492 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49101-49200   *Has distinct variable group(s)

Type	Label	Description
Statement
21.49.20.3  The ` ZZ `-module ` ZZ X. ZZ `
Theorem	zlmodzxzlmod 49101	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 49102	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 49103	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 49104	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 49105	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 49106	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 49107	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, (𝐶 − 𝐷)⟩})
21.49.20.4  Group sum operation (extension 2)
Theorem	mgpsumunsn 49108*	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 49109*	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 49110*	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 (𝑘 ∈ (𝑁 ∖ {𝐼}) ↦ 𝐴)))
21.49.20.5  Symmetric groups (extension)
Theorem	exple2lt6 49111	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 49112	Every symmetric group on a set with at most 2 elements is abelian. (Contributed by AV, 16-Mar-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ (♯‘𝐴) ≤ 2) → 𝐺 ∈ Abel)
Theorem	pgrpgt2nabl 49113	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)
21.49.20.6  Divisibility (extension)
Theorem	invginvrid 49114	Identity for a multiplication with additive and multiplicative inverses in a ring. (Contributed by AV, 18-May-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑁‘𝑌) · ((𝐼‘(𝑁‘𝑌)) · 𝑋)) = 𝑋)
21.49.20.7  The support of functions (extension)
Theorem	rmsupp0 49115*	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 49116*	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 49117*	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 49118*	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‘𝑆)))
21.49.20.8  Finitely supported functions (extension)
Theorem	rmsuppfi 49119*	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 49120*	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 49121*	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 49122*	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 49123*	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 49124*	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 49125*	A mapping with a finite domain is finitely supported. (Contributed by AV, 4-Sep-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
21.49.20.9  Left modules (extension)
Theorem	lmodvsmdi 49126	Multiple distributive law for scalar product (left-distributivity). (Contributed by AV, 5-Sep-2019.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ↑ = (.g‘𝑊)    &   ⊢ 𝐸 = (.g‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))
Theorem	gsumlsscl 49127*	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 (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠 ‘𝑀)𝑣))) ∈ 𝑍))
21.49.20.10  Associative algebras (extension)
Theorem	assaascl0 49128	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 49129	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‘𝑊))
21.49.20.11  Univariate polynomials (extension)
Theorem	ply1vr1smo 49130	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 49131	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	coe1sclmulval 49132	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 49133*	Lemma 1 for ply1mulgsum 49137. (Contributed by AV, 19-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐶 = (coe1‘𝐿)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ × = (.r‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∗ = (.r‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))))
Theorem	ply1mulgsumlem2 49134*	Lemma 2 for ply1mulgsum 49137. (Contributed by AV, 19-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐶 = (coe1‘𝐿)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ × = (.r‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∗ = (.r‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅)))
Theorem	ply1mulgsumlem3 49135*	Lemma 3 for ply1mulgsum 49137. (Contributed by AV, 20-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐶 = (coe1‘𝐿)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ × = (.r‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∗ = (.r‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))))) finSupp (0g‘𝑅))
Theorem	ply1mulgsumlem4 49136*	Lemma 4 for ply1mulgsum 49137. (Contributed by AV, 19-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐶 = (coe1‘𝐿)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ × = (.r‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∗ = (.r‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑃))
Theorem	ply1mulgsum 49137*	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 49138	Polynomial evaluation for the 0 scalar. (Contributed by AV, 10-Aug-2019.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑃)    ⇒   ⊢ (𝑅 ∈ CRing → ((𝑂‘𝑍)‘ 0 ) = 0 )
Theorem	evl1at1 49139	Polynomial evaluation for the 1 scalar. (Contributed by AV, 10-Aug-2019.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (1r‘𝑃)    ⇒   ⊢ (𝑅 ∈ CRing → ((𝑂‘𝐼)‘ 1 ) = 1 )
21.49.20.12  Univariate polynomials (examples)
Theorem	linply1 49140	A term of the form 𝑥 − 𝐶 is a (univariate) polynomial, also called "linear polynomial". (Part of ply1remlem 26301). (Contributed by AV, 3-Jul-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐺 = (𝑋 − (𝐴‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝐵)
Theorem	lineval 49141	A term of the form 𝑥 − 𝐶 evaluated for 𝑥 = 𝑉 results in 𝑉 − 𝐶 (part of ply1remlem 26301). (Contributed by AV, 3-Jul-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐺 = (𝑋 − (𝐴‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑂‘𝐺)‘𝑉) = (𝑉(-g‘𝑅)𝐶))
Theorem	linevalexample 49142	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
21.49.21  Linear algebra (extension)
21.49.21.1  The subalgebras of diagonal and scalar matrices (extension) 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 22626 and df-scmat 22627 define diagonal and scalar matrices as sets.
Syntax	cdmatalt 49143	Alternative notation for the algebra of diagonal matrices.
class DMatALT
Syntax	cscmatalt 49144	Alternative notation for the algebra of scalar matrices.
class ScMatALT
Definition	df-dmatalt 49145*	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 49146*	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 49147*	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 49148*	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 49149*	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 49150	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 𝑅)))
21.49.21.2  Linear combinations 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 49153, 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 49154, so that we can show that such sets are submodules of the corresponding modules, see lincolss 49181. Remark:According to Wikipedia ("Linear span", 28-Apr-2019, https://en.wikipedia.org/wiki/Linear_span 49181) "In linear algebra, the linear span (also called the linear hull or just span) of a set of vectors in a vector space [or module] is the intersection of all linear subspaces which each contain every vector in that set.", and "Alternately, the span of [a set] S may be defined as the set of all finite linear combinations of elements (vectors) of S". Whereas spans are defined according to the first approach in df-lsp 21072, the set of all linear combinations as defined by df-lco 49154 follows the alternative approach. That both definitions are equivalent is shown by lspeqlco 49186.
Syntax	clinc 49151	Extend class notation with the operation constructing a linear combination (of vectors from a left module).
class linC
Syntax	clinco 49152	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 49153*	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 49154*	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 49155*	A linear combination as operation. (Contributed by AV, 30-Mar-2019.)
⊢ (𝑀 ∈ 𝑋 → ( linC ‘𝑀) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑀)𝑥)))))
Theorem	lincval 49156*	The value of a linear combination. (Contributed by AV, 30-Mar-2019.)
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝑆( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝑆‘𝑥)( ·𝑠 ‘𝑀)𝑥))))
Theorem	dflinc2 49157*	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 49158*	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 49159*	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 49160	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 49161	A linear combination of vectors is a vector. (Contributed by AV, 31-Mar-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Base‘(Scalar‘𝑀))    ⇒   ⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑m 𝑉))) → (𝑆( linC ‘𝑀)𝑉) ∈ 𝐵)
Theorem	lincval0 49162	The value of an empty linear combination. (Contributed by AV, 12-Apr-2019.)
⊢ (𝑀 ∈ 𝑋 → (∅( linC ‘𝑀)∅) = (0g‘𝑀))
Theorem	lincvalsng 49163	The linear combination over a singleton. (Contributed by AV, 25-May-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → ({⟨𝑉, 𝑌⟩} ( linC ‘𝑀){𝑉}) = (𝑌 · 𝑉))
Theorem	lincvalsn 49164	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 49165	The linear combination over an unordered pair. (Contributed by AV, 16-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝐹 = {⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩}    ⇒   ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = ((𝑋 · 𝑉) + (𝑌 · 𝑊)))
Theorem	lincval1 49166	The linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐹 = {⟨𝑉, (0g‘𝑆)⟩}    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵) → (𝐹( linC ‘𝑀){𝑉}) = (0g‘𝑀))
Theorem	lcosn0 49167	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 49168*	The linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ 0 )    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹( linC ‘𝑀)𝑉) = 𝑍)
Theorem	lcoc0 49169*	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 49170*	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 49171	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 49172*	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 49173	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 49174	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 49175	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 49176	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 49177*	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 49178	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 49179	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 49180	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 49181	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 49182*	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 49183	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 49184	Lemma for lspeqlco 49186. (Contributed by AV, 17-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → ((LSpan‘𝑀)‘𝑉) ⊆ (𝑀 LinCo 𝑉))
Theorem	lcosslsp 49185	Lemma for lspeqlco 49186. (Contributed by AV, 20-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 LinCo 𝑉) ⊆ ((LSpan‘𝑀)‘𝑉))
Theorem	lspeqlco 49186	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 21072) 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‘𝑀)‘𝑉))
21.49.21.3  Linear independence 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 49189 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. Usually, the linear independence is defined for vector spaces, see Wikipedia ("Linear independence", 15-Apr-2019, https://en.wikipedia.org/wiki/Linear_independence 49189): "In the theory of vector spaces, a set of vectors is said to be linearly dependent if at least one of the vectors in the set can be defined as a linear combination of the others; if no vector in the set can be written in this way, then the vectors are said to be linearly independent." Furthermore, "In order to allow the number of linearly independent vectors in a vector space to be countably infinite, it is useful to define linear dependence as follows. More generally, let V be a vector space over a field K, and let {vi | i∈I} be a family of elements of V. The family is linearly dependent over K if there exists a finite family {aj | j∈J} of elements of K, all nonzero, such that ∑j∈J ajvj=0. A set X of elements of V is linearly independent if the corresponding family{x}x∈X is linearly independent". Remark 1: There are already definitions of (linearly) independent families (df-lindf 21935) and (linearly) independent sets (df-linds 21936). These definitions are based on the principle "of vectors, no nonzero multiple of which can be expressed as a linear combination of other elements" or (see lbsind2 21181) "every element is not in the span of the remainder of the [set]". The equivalence of Definitions df-linds 21936 and df-lininds 49189 for (linear) independence for (left) modules is shown in lindslininds 49211. Remark 2: Subsets of the base set of a (left) module are linearly dependent if they are not linearly independent (see df-lindeps 49191) or, according to Wikipedia, "if at least one of the vectors in the set can be defined as a linear combination of the others", see islindeps2 49230. The reversed implication is not valid for arbitrary modules (but for arbitrary vector spaces), because it requires a division by a coefficient. Therefore, the definition of Wikipedia is equivalent to our definition for (left) vector spaces (see isldepslvec2 49232) and not for (left) modules in general.
Syntax	clininds 49187	Extend class notation with the relation between a module and its linearly independent subsets.
class linIndS
Syntax	clindeps 49188	Extend class notation with the relation between a module and its linearly dependent subsets.
class linDepS
Definition	df-lininds 49189*	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 49190	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 49191*	Define the relation between a module and its linearly dependent subsets. (Contributed by AV, 26-Apr-2019.)
⊢ linDepS = {⟨𝑠, 𝑚⟩ ∣ ¬ 𝑠 linIndS 𝑚}
Theorem	linindsv 49192	The classes of the module and its linearly independent subsets are sets. (Contributed by AV, 13-Apr-2019.)
⊢ (𝑆 linIndS 𝑀 → (𝑆 ∈ V ∧ 𝑀 ∈ V))
Theorem	islininds 49193*	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 49194*	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 49195*	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 49196*	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 49197*	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 49198	A linearly independent set is a subset of (the base set of) a module. (Contributed by AV, 13-Apr-2019.)
⊢ (𝑆 linIndS 𝑀 → 𝑆 ∈ 𝒫 (Base‘𝑀))
Theorem	lindepsnlininds 49199	A linearly dependent subset is not a linearly independent subset. (Contributed by AV, 26-Apr-2019.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → (𝑆 linDepS 𝑀 ↔ ¬ 𝑆 linIndS 𝑀))
Theorem	islindeps 49200*	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 )))