P. 489 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48801-48900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lcoval 48801*	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 48802	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 48803	A linear combination of vectors is a vector. (Contributed by AV, 31-Mar-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Base‘(Scalar‘𝑀))    ⇒   ⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑m 𝑉))) → (𝑆( linC ‘𝑀)𝑉) ∈ 𝐵)
Theorem	lincval0 48804	The value of an empty linear combination. (Contributed by AV, 12-Apr-2019.)
⊢ (𝑀 ∈ 𝑋 → (∅( linC ‘𝑀)∅) = (0g‘𝑀))
Theorem	lincvalsng 48805	The linear combination over a singleton. (Contributed by AV, 25-May-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → ({⟨𝑉, 𝑌⟩} ( linC ‘𝑀){𝑉}) = (𝑌 · 𝑉))
Theorem	lincvalsn 48806	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 48807	The linear combination over an unordered pair. (Contributed by AV, 16-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝐹 = {⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩}    ⇒   ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = ((𝑋 · 𝑉) + (𝑌 · 𝑊)))
Theorem	lincval1 48808	The linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐹 = {⟨𝑉, (0g‘𝑆)⟩}    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵) → (𝐹( linC ‘𝑀){𝑉}) = (0g‘𝑀))
Theorem	lcosn0 48809	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 48810*	The linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ 0 )    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹( linC ‘𝑀)𝑉) = 𝑍)
Theorem	lcoc0 48811*	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 48812*	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 48813	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 48814*	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 48815	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 48816	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 48817	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 48818	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 48819*	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 48820	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 48821	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 48822	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 48823	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 48824*	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 48825	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 48826	Lemma for lspeqlco 48828. (Contributed by AV, 17-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → ((LSpan‘𝑀)‘𝑉) ⊆ (𝑀 LinCo 𝑉))
Theorem	lcosslsp 48827	Lemma for lspeqlco 48828. (Contributed by AV, 20-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 LinCo 𝑉) ⊆ ((LSpan‘𝑀)‘𝑉))
Theorem	lspeqlco 48828	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 20940) 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.48.20.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 48831 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 48831): "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 21778) and (linearly) independent sets (df-linds 21779). 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 21050) "every element is not in the span of the remainder of the [set]". The equivalence of Definitions df-linds 21779 and df-lininds 48831 for (linear) independence for (left) modules is shown in lindslininds 48853. Remark 2: Subsets of the base set of a (left) module are linearly dependent if they are not linearly independent (see df-lindeps 48833) 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 48872. 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 48874) and not for (left) modules in general.
Syntax	clininds 48829	Extend class notation with the relation between a module and its linearly independent subsets.
class linIndS
Syntax	clindeps 48830	Extend class notation with the relation between a module and its linearly dependent subsets.
class linDepS
Definition	df-lininds 48831*	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 48832	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 48833*	Define the relation between a module and its linearly dependent subsets. (Contributed by AV, 26-Apr-2019.)
⊢ linDepS = {⟨𝑠, 𝑚⟩ ∣ ¬ 𝑠 linIndS 𝑚}
Theorem	linindsv 48834	The classes of the module and its linearly independent subsets are sets. (Contributed by AV, 13-Apr-2019.)
⊢ (𝑆 linIndS 𝑀 → (𝑆 ∈ V ∧ 𝑀 ∈ V))
Theorem	islininds 48835*	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 48836*	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 48837*	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 48838*	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 48839*	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 48840	A linearly independent set is a subset of (the base set of) a module. (Contributed by AV, 13-Apr-2019.)
⊢ (𝑆 linIndS 𝑀 → 𝑆 ∈ 𝒫 (Base‘𝑀))
Theorem	lindepsnlininds 48841	A linearly dependent subset is not a linearly independent subset. (Contributed by AV, 26-Apr-2019.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → (𝑆 linDepS 𝑀 ↔ ¬ 𝑆 linIndS 𝑀))
Theorem	islindeps 48842*	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 48843*	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 48844*	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 )
Theorem	lincext3 48845*	Property 3 of an extension of a linear combination. (Contributed by AV, 23-Apr-2019.) (Revised by AV, 30-Jul-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐹 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑋, (𝑁‘𝑌), (𝐺‘𝑧)))    ⇒   ⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑m (𝑆 ∖ {𝑋}))) ∧ (𝐺 finSupp 0 ∧ (𝑌( ·𝑠 ‘𝑀)𝑋) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})))) → (𝐹( linC ‘𝑀)𝑆) = 𝑍)
Theorem	lindslinindsimp1 48846*	Implication 1 for lindslininds 48853. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) (Proof shortened by II, 16-Feb-2023.)
⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    ⇒   ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → ((𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )) → (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠 ∈ 𝑆 ∀𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))))
Theorem	lindslinindimp2lem1 48847*	Lemma 1 for lindslinindsimp2 48852. (Contributed by AV, 25-Apr-2019.)
⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑌 = ((invg‘𝑅)‘(𝑓‘𝑥))    &   ⊢ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥}))    ⇒   ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ (𝐵 ↑m 𝑆))) → 𝑌 ∈ 𝐵)
Theorem	lindslinindimp2lem2 48848*	Lemma 2 for lindslinindsimp2 48852. (Contributed by AV, 25-Apr-2019.)
⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑌 = ((invg‘𝑅)‘(𝑓‘𝑥))    &   ⊢ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥}))    ⇒   ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ (𝐵 ↑m 𝑆))) → 𝐺 ∈ (𝐵 ↑m (𝑆 ∖ {𝑥})))
Theorem	lindslinindimp2lem3 48849*	Lemma 3 for lindslinindsimp2 48852. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.)
⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑌 = ((invg‘𝑅)‘(𝑓‘𝑥))    &   ⊢ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥}))    ⇒   ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) ∧ (𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 )) → 𝐺 finSupp 0 )
Theorem	lindslinindimp2lem4 48850*	Lemma 4 for lindslinindsimp2 48852. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) (Proof shortened by II, 16-Feb-2023.)
⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑌 = ((invg‘𝑅)‘(𝑓‘𝑥))    &   ⊢ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥}))    ⇒   ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) ∧ (𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = (𝑌( ·𝑠 ‘𝑀)𝑥))
Theorem	lindslinindsimp2lem5 48851*	Lemma 5 for lindslinindsimp2 48852. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.)
⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    ⇒   ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → ((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠 ‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → (𝑓‘𝑥) = 0 )))
Theorem	lindslinindsimp2 48852*	Implication 2 for lindslininds 48853. (Contributed by AV, 26-Apr-2019.) (Revised by AV, 30-Jul-2019.)
⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    ⇒   ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → ((𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠 ∈ 𝑆 ∀𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))) → (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))))
Theorem	lindslininds 48853	Equivalence of definitions df-linds 21779 and df-lininds 48831 for (linear) independence for (left) modules. (Contributed by AV, 26-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → (𝑆 linIndS 𝑀 ↔ 𝑆 ∈ (LIndS‘𝑀)))
Theorem	linds0 48854	The empty set is always a linearly independent subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 27-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ (𝑀 ∈ 𝑉 → ∅ linIndS 𝑀)
Theorem	el0ldep 48855	A set containing the zero element of a module is always linearly dependent, if the underlying ring has at least two elements. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 27-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ (((𝑀 ∈ LMod ∧ 1 < (♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝑆) → 𝑆 linDepS 𝑀)
Theorem	el0ldepsnzr 48856	A set containing the zero element of a module over a nonzero ring is always linearly dependent. (Contributed by AV, 14-Apr-2019.) (Revised by AV, 27-Apr-2019.)
⊢ (((𝑀 ∈ LMod ∧ (Scalar‘𝑀) ∈ NzRing) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝑆) → 𝑆 linDepS 𝑀)
Theorem	lindsrng01 48857	Any subset of a module is always linearly independent if the underlying ring has at most one element. Since the underlying ring cannot be the empty set (see lmodsn0 20842), this means that the underlying ring has only one element, so it is a zero ring. (Contributed by AV, 14-Apr-2019.) (Revised by AV, 27-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ ((♯‘𝐸) = 0 ∨ (♯‘𝐸) = 1) ∧ 𝑆 ∈ 𝒫 𝐵) → 𝑆 linIndS 𝑀)
Theorem	lindszr 48858	Any subset of a module over a zero ring is always linearly independent. (Contributed by AV, 27-Apr-2019.)
⊢ ((𝑀 ∈ LMod ∧ ¬ (Scalar‘𝑀) ∈ NzRing ∧ 𝑆 ∈ 𝒫 (Base‘𝑀)) → 𝑆 linIndS 𝑀)
Theorem	snlindsntorlem 48859*	Lemma for snlindsntor 48860. (Contributed by AV, 15-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝑆 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ · = ( ·𝑠 ‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ) → ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )))
Theorem	snlindsntor 48860*	A singleton is linearly independent iff it does not contain a torsion element. According to Wikipedia ("Torsion (algebra)", 15-Apr-2019, https://en.wikipedia.org/wiki/Torsion_(algebra)): "An element m of a module M over a ring R is called a torsion element of the module if there exists a regular element r of the ring (an element that is neither a left nor a right zero divisor) that annihilates m, i.e., (𝑟 · 𝑚) = 0. In an integral domain (a commutative ring without zero divisors), every nonzero element is regular, so a torsion element of a module over an integral domain is one annihilated by a nonzero element of the integral domain." Analogously, the definition in [Lang] p. 147 states that "An element x of [a module] E [over a ring R] is called a torsion element if there exists 𝑎 ∈ 𝑅, 𝑎 ≠ 0, such that 𝑎 · 𝑥 = 0. This definition includes the zero element of the module. Some authors, however, exclude the zero element from the definition of torsion elements. (Contributed by AV, 14-Apr-2019.) (Revised by AV, 27-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝑆 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ · = ( ·𝑠 ‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ (𝑆 ∖ { 0 })(𝑠 · 𝑋) ≠ 𝑍 ↔ {𝑋} linIndS 𝑀))
Theorem	ldepsprlem 48861	Lemma for ldepspr 48862. (Contributed by AV, 16-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝑆 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ · = ( ·𝑠 ‘𝑀)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → (𝑋 = (𝐴 · 𝑌) → (( 1 · 𝑋)(+g‘𝑀)((𝑁‘𝐴) · 𝑌)) = 𝑍))
Theorem	ldepspr 48862	If a vector is a scalar multiple of another vector, the (unordered pair containing the) two vectors are linearly dependent. (Contributed by AV, 16-Apr-2019.) (Revised by AV, 27-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝑆 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ · = ( ·𝑠 ‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) → ((𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌)) → {𝑋, 𝑌} linDepS 𝑀))
Theorem	lincresunit3lem3 48863	Lemma 3 for lincresunit3 48870. (Contributed by AV, 18-May-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑀)    ⇒   ⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐴 ∈ 𝑈) → (((𝑁‘𝐴) · 𝑋) = ((𝑁‘𝐴) · 𝑌) ↔ 𝑋 = 𝑌))
Theorem	lincresunitlem1 48864	Lemma 1 for properties of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈)) → (𝐼‘(𝑁‘(𝐹‘𝑋))) ∈ 𝐸)
Theorem	lincresunitlem2 48865	Lemma for properties of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈)) ∧ 𝑌 ∈ 𝑆) → ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑌)) ∈ 𝐸)
Theorem	lincresunit1 48866*	Property 1 of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈)) → 𝐺 ∈ (𝐸 ↑m (𝑆 ∖ {𝑋})))
Theorem	lincresunit2 48867*	Property 2 of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → 𝐺 finSupp 0 )
Theorem	lincresunit3lem1 48868*	Lemma 1 for lincresunit3 48870. (Contributed by AV, 17-May-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝑧 ∈ (𝑆 ∖ {𝑋}))) → ((𝑁‘(𝐹‘𝑋))( ·𝑠 ‘𝑀)((𝐺‘𝑧)( ·𝑠 ‘𝑀)𝑧)) = ((𝐹‘𝑧)( ·𝑠 ‘𝑀)𝑧))
Theorem	lincresunit3lem2 48869*	Lemma 2 for lincresunit3 48870. (Contributed by AV, 18-May-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → ((𝑁‘(𝐹‘𝑋))( ·𝑠 ‘𝑀)(𝑀 Σg (𝑧 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐺‘𝑧)( ·𝑠 ‘𝑀)𝑧)))) = ((𝐹 ↾ (𝑆 ∖ {𝑋}))( linC ‘𝑀)(𝑆 ∖ {𝑋})))
Theorem	lincresunit3 48870*	Property 3 of a specially modified restriction of a linear combination in a vector space. (Contributed by AV, 18-May-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ∧ (𝐹( linC ‘𝑀)𝑆) = 𝑍) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})) = 𝑋)
Theorem	lincreslvec3 48871*	Property 3 of a specially modified restriction of a linear combination in a vector space. (Contributed by AV, 18-May-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠)))    ⇒   ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LVec ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ≠ 0 ∧ 𝐹 finSupp 0 ) ∧ (𝐹( linC ‘𝑀)𝑆) = 𝑍) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})) = 𝑋)
Theorem	islindeps2 48872*	Conditions for being a linearly dependent subset of a (left) module over a nonzero ring. (Contributed by AV, 29-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing) → (∃𝑠 ∈ 𝑆 ∃𝑓 ∈ (𝐸 ↑m (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠) → 𝑆 linDepS 𝑀))
Theorem	islininds2 48873*	Implication of being a linearly independent subset of a (left) module over a nonzero ring. (Contributed by AV, 29-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing) → (𝑆 linIndS 𝑀 → ∀𝑠 ∈ 𝑆 ∀𝑓 ∈ (𝐸 ↑m (𝑆 ∖ {𝑠}))(¬ 𝑓 finSupp 0 ∨ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) ≠ 𝑠)))
Theorem	isldepslvec2 48874*	Alternative definition of being a linearly dependent subset of a (left) vector space. In this case, the reverse implication of islindeps2 48872 holds, so that both definitions are equivalent (see theorem 1.6 in [Roman] p. 46 and the note in [Roman] p. 112: if a nontrivial linear combination of elements (where not all of the coefficients are 0) in an R-vector space is 0, then and only then each of the elements is a linear combination of the others. (Contributed by AV, 30-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (0g‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) → (∃𝑠 ∈ 𝑆 ∃𝑓 ∈ (𝐸 ↑m (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠) ↔ 𝑆 linDepS 𝑀))
Theorem	lindssnlvec 48875	A singleton not containing the zero element of a vector space is always linearly independent. (Contributed by AV, 16-Apr-2019.) (Revised by AV, 28-Apr-2019.)
⊢ ((𝑀 ∈ LVec ∧ 𝑆 ∈ (Base‘𝑀) ∧ 𝑆 ≠ (0g‘𝑀)) → {𝑆} linIndS 𝑀)
21.48.20.4  Simple left modules and the ` ZZ `-module
Theorem	lmod1lem1 48876*	Lemma 1 for lmod1 48881. (Contributed by AV, 28-Apr-2019.)
⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)⟩})    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ (Base‘𝑅)) → (𝑟( ·𝑠 ‘𝑀)𝐼) ∈ {𝐼})
Theorem	lmod1lem2 48877*	Lemma 2 for lmod1 48881. (Contributed by AV, 28-Apr-2019.)
⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)⟩})    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ (Base‘𝑅)) → (𝑟( ·𝑠 ‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠 ‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠 ‘𝑀)𝐼)))
Theorem	lmod1lem3 48878*	Lemma 3 for lmod1 48881. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)⟩})    ⇒   ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠 ‘𝑀)𝐼) = ((𝑞( ·𝑠 ‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠 ‘𝑀)𝐼)))
Theorem	lmod1lem4 48879*	Lemma 4 for lmod1 48881. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)⟩})    ⇒   ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → ((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠 ‘𝑀)𝐼) = (𝑞( ·𝑠 ‘𝑀)(𝑟( ·𝑠 ‘𝑀)𝐼)))
Theorem	lmod1lem5 48880*	Lemma 5 for lmod1 48881. (Contributed by AV, 28-Apr-2019.)
⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)⟩})    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → ((1r‘(Scalar‘𝑀))( ·𝑠 ‘𝑀)𝐼) = 𝐼)
Theorem	lmod1 48881*	The (smallest) structure representing a zero module over an arbitrary ring. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)⟩})    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑀 ∈ LMod)
Theorem	lmod1zr 48882	The (smallest) structure representing a zero module over a zero ring. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑅 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    &   ⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), {⟨⟨𝑍, 𝐼⟩, 𝐼⟩}⟩})    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑀 ∈ LMod)
Theorem	lmod1zrnlvec 48883	There is a (left) module (a zero module) which is not a (left) vector space. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑅 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    &   ⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), {⟨⟨𝑍, 𝐼⟩, 𝐼⟩}⟩})    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑀 ∉ LVec)
Theorem	lmodn0 48884	Left modules exist. (Contributed by AV, 29-Apr-2019.)
⊢ LMod ≠ ∅
Theorem	zlmodzxzequa 48885	Example of an equation within the ℤ-module ℤ × ℤ (see example in [Roman] p. 112 for a linearly dependent set). (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 0 = {⟨0, 0⟩, ⟨1, 0⟩}    &   ⊢ ∙ = ( ·𝑠 ‘𝑍)    &   ⊢ − = (-g‘𝑍)    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ ((2 ∙ 𝐴) − (3 ∙ 𝐵)) = 0
Theorem	zlmodzxznm 48886	Example of a linearly dependent set whose elements are not linear combinations of the others, see note in [Roman] p. 112). (Contributed by AV, 23-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 0 = {⟨0, 0⟩, ⟨1, 0⟩}    &   ⊢ ∙ = ( ·𝑠 ‘𝑍)    &   ⊢ − = (-g‘𝑍)    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ ∀𝑖 ∈ ℤ ((𝑖 ∙ 𝐴) ≠ 𝐵 ∧ (𝑖 ∙ 𝐵) ≠ 𝐴)
Theorem	zlmodzxzldeplem 48887	A and B are not equal. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ 𝐴 ≠ 𝐵
Theorem	zlmodzxzequap 48888	Example of an equation within the ℤ-module ℤ × ℤ (see example in [Roman] p. 112 for a linearly dependent set), written as a sum. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    &   ⊢ 0 = {⟨0, 0⟩, ⟨1, 0⟩}    &   ⊢ + = (+g‘𝑍)    &   ⊢ ∙ = ( ·𝑠 ‘𝑍)    ⇒   ⊢ ((2 ∙ 𝐴) + (-3 ∙ 𝐵)) = 0
Theorem	zlmodzxzldeplem1 48889	Lemma 1 for zlmodzxzldep 48893. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    &   ⊢ 𝐹 = {⟨𝐴, 2⟩, ⟨𝐵, -3⟩}    ⇒   ⊢ 𝐹 ∈ (ℤ ↑m {𝐴, 𝐵})
Theorem	zlmodzxzldeplem2 48890	Lemma 2 for zlmodzxzldep 48893. (Contributed by AV, 24-May-2019.) (Revised by AV, 30-Jul-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    &   ⊢ 𝐹 = {⟨𝐴, 2⟩, ⟨𝐵, -3⟩}    ⇒   ⊢ 𝐹 finSupp 0
Theorem	zlmodzxzldeplem3 48891	Lemma 3 for zlmodzxzldep 48893. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    &   ⊢ 𝐹 = {⟨𝐴, 2⟩, ⟨𝐵, -3⟩}    ⇒   ⊢ (𝐹( linC ‘𝑍){𝐴, 𝐵}) = (0g‘𝑍)
Theorem	zlmodzxzldeplem4 48892*	Lemma 4 for zlmodzxzldep 48893. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    &   ⊢ 𝐹 = {⟨𝐴, 2⟩, ⟨𝐵, -3⟩}    ⇒   ⊢ ∃𝑦 ∈ {𝐴, 𝐵} (𝐹‘𝑦) ≠ 0
Theorem	zlmodzxzldep 48893	{ A , B } is a linearly dependent set within the ℤ-module ℤ × ℤ (see example in [Roman] p. 112). (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ {𝐴, 𝐵} linDepS 𝑍
Theorem	ldepsnlinclem1 48894	Lemma 1 for ldepsnlinc 48897. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ (𝐹 ∈ ((Base‘ℤring) ↑m {𝐵}) → (𝐹( linC ‘𝑍){𝐵}) ≠ 𝐴)
Theorem	ldepsnlinclem2 48895	Lemma 2 for ldepsnlinc 48897. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ (𝐹 ∈ ((Base‘ℤring) ↑m {𝐴}) → (𝐹( linC ‘𝑍){𝐴}) ≠ 𝐵)
21.48.20.5  Differences between (left) modules and (left) vector spaces
Theorem	lvecpsslmod 48896	The class of all (left) vector spaces is a proper subclass of the class of all (left) modules. Although it is obvious (and proven by lveclmod 21075) that every left vector space is a left module, there is (at least) one left module which is no left vector space, for example the zero module over the zero ring, see lmod1zrnlvec 48883. (Contributed by AV, 29-Apr-2019.)
⊢ LVec ⊊ LMod
Theorem	ldepsnlinc 48897*	The reverse implication of islindeps2 48872 does not hold for arbitrary (left) modules, see note in [Roman] p. 112: "... if a nontrivial linear combination of the elements ... in an R-module M is 0, ... where not all of the coefficients are 0, then we cannot conclude ... that one of the elements ... is a linear combination of the others." This means that there is at least one left module having a linearly dependent subset in which there is at least one element which is not a linear combination of the other elements of this subset. Such a left module can be constructed by using zlmodzxzequa 48885 and zlmodzxznm 48886. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.)
⊢ ∃𝑚 ∈ LMod ∃𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ∧ ∀𝑣 ∈ 𝑠 ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣))
Theorem	ldepslinc 48898*	For (left) vector spaces, isldepslvec2 48874 provides an alternative definition of being a linearly dependent subset, whereas ldepsnlinc 48897 indicates that there is not an analogous alternative definition for arbitrary (left) modules. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.)
⊢ (∀𝑚 ∈ LVec ∀𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ↔ ∃𝑣 ∈ 𝑠 ∃𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) = 𝑣)) ∧ ¬ ∀𝑚 ∈ LMod ∀𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ↔ ∃𝑣 ∈ 𝑠 ∃𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) = 𝑣)))
21.48.21  Complexity theory
21.48.21.1  Auxiliary theorems
Theorem	suppdm 48899	If the range of a function does not contain the zero, the support of the function equals its domain. (Contributed by AV, 20-May-2020.)
⊢ (((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝑍 ∉ ran 𝐹) → (𝐹 supp 𝑍) = dom 𝐹)
Theorem	eluz2cnn0n1 48900	An integer greater than 1 is a complex number not equal to 0 or 1. (Contributed by AV, 23-May-2020.)
⊢ (𝐵 ∈ (ℤ≥‘2) → 𝐵 ∈ (ℂ ∖ {0, 1}))