P. 399 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39801-39900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ply1mulgsumlem3 39801*	Lemma 3 for ply1mulgsum 39803. (Contributed by AV, 20-Oct-2019.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- A = (coe1 ` K )   &    |- C = (coe1 ` L )   &    |- X = (var1 ` R )   &    |- .X. = ( .r ` P )   &    |- .x. = ( .s ` P )   &    |- .* = ( .r ` R )   &    |- M = (mulGrp ` P )   &    |- .^ = (.g ` M )   =>    |- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( k e. NN0 |-> ( R gsumg ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) ) finSupp ( 0g ` R ) )
Theorem	ply1mulgsumlem4 39802*	Lemma 4 for ply1mulgsum 39803. (Contributed by AV, 19-Oct-2019.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- A = (coe1 ` K )   &    |- C = (coe1 ` L )   &    |- X = (var1 ` R )   &    |- .X. = ( .r ` P )   &    |- .x. = ( .s ` P )   &    |- .* = ( .r ` R )   &    |- M = (mulGrp ` P )   &    |- .^ = (.g ` M )   =>    |- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( k e. NN0 |-> ( ( R gsumg ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) finSupp ( 0g ` P ) )
Theorem	ply1mulgsum 39803*	The product of two polynomials expressed as group sum of scaled monomials. (Contributed by AV, 20-Oct-2019.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- A = (coe1 ` K )   &    |- C = (coe1 ` L )   &    |- X = (var1 ` R )   &    |- .X. = ( .r ` P )   &    |- .x. = ( .s ` P )   &    |- .* = ( .r ` R )   &    |- M = (mulGrp ` P )   &    |- .^ = (.g ` M )   =>    |- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( K .X. L ) = ( P gsumg ( k e. NN0 |-> ( ( R gsumg ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) ) )
Theorem	evl1at0 39804	Polynomial evaluation for the 0 scalar. (Contributed by AV, 10-Aug-2019.)
|- O = (eval1 ` R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` P )   =>    |- ( R e. CRing -> ( ( O ` Z ) ` .0. ) = .0. )
Theorem	evl1at1 39805	Polynomial evaluation for the 1 scalar. (Contributed by AV, 10-Aug-2019.)
|- O = (eval1 ` R )   &    |- P = (Poly1 ` R )   &    |- .1. = ( 1r ` R )   &    |- I = ( 1r ` P )   =>    |- ( R e. CRing -> ( ( O ` I ) ` .1. ) = .1. )
21.33.14.12  Univariate polynomials (examples)
Theorem	linply1 39806	A term of the form x - C is a (univariate) polynomial, also called "linear polynomial". (Part of ply1remlem 23111). (Contributed by AV, 3-Jul-2019.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- K = ( Base ` R )   &    |- X = (var1 ` R )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   &    |- G = ( X .- ( A ` C ) )   &    |- ( ph -> C e. K )   &    |- ( ph -> R e. Ring )   =>    |- ( ph -> G e. B )
Theorem	lineval 39807	A term of the form x - C evaluated for x = V results in V - C (part of ply1remlem 23111). (Contributed by AV, 3-Jul-2019.)
|- P = (Poly1 ` R )   &    |- B = ( Base ` P )   &    |- K = ( Base ` R )   &    |- X = (var1 ` R )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   &    |- G = ( X .- ( A ` C ) )   &    |- ( ph -> C e. K )   &    |- O = (eval1 ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> V e. K )   =>    |- ( ph -> ( ( O ` G ) ` V ) = ( V ( -g ` R ) C ) )
Theorem	zringsubgval 39808	Subtraction in the ring of integers. (Contributed by AV, 3-Aug-2019.)
|- .- = ( -g ` ℤring )   =>    |- ( ( X e. ZZ /\ Y e. ZZ ) -> ( X - Y ) = ( X .- Y ) )
Theorem	linevalexample 39809	The polynomial x - 3 over ZZ evaluated for x = 5 results in 2. (Contributed by AV, 3-Jul-2019.)
|- P = (Poly1 ` ℤring )   &    |- B = ( Base ` P )   &    |- X = (var1 ` ℤring )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   &    |- G = ( X .- ( A ` 3 ) )   &    |- O = (eval1 ` ℤring )   =>    |- ( ( O ` ( X .- ( A ` 3 ) ) ) ` 5 ) = 2
21.33.15  Linear algebra (extension)
21.33.15.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 the definitions df-dmat 19513 and df-scmat 19514 define diagonal and scalar matrices as sets.
Syntax	cdmatalt 39810	Alternative notation for the algebra of diagonal matrices.
class DMatALT
Syntax	cscmatalt 39811	Alternative notation for the algebra of scalar matrices.
class ScMatALT
Definition	df-dmatalt 39812*	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 = ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ ( a ↾s { m e. ( Base ` a ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } ) )
Definition	df-scmatalt 39813*	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 = ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ ( a ↾s { m e. ( Base ` a ) | E. c e. ( Base ` r ) A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) ) } ) )
Theorem	dmatALTval 39814*	The algebra of N x N diagonal matrices over a ring R. (Contributed by AV, 8-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- D = ( N DMatALT R )   =>    |- ( ( N e. Fin /\ R e. _V ) -> D = ( A ↾s { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } ) )
Theorem	dmatALTbas 39815*	The base set of the algebra of N x N diagonal matrices over a ring R, i.e. the set of all N x N diagonal matrices over the ring R. (Contributed by AV, 8-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- D = ( N DMatALT R )   =>    |- ( ( N e. Fin /\ R e. _V ) -> ( Base ` D ) = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
Theorem	dmatALTbasel 39816*	An element of the base set of the algebra of N x N diagonal matrices over a ring R, i.e. an N x N diagonal matrix over the ring R. (Contributed by AV, 8-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- D = ( N DMatALT R )   =>    |- ( ( N e. Fin /\ R e. _V ) -> ( M e. ( Base ` D ) <-> ( M e. B /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) ) )
Theorem	dmatbas 39817	The set of all N x N diagonal matrices over (the ring) R is the base set of the algebra of N x N diagonal matrices over (the ring) R. (Contributed by AV, 8-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- D = ( N DMat R )   =>    |- ( ( N e. Fin /\ R e. V ) -> D = ( Base ` ( N DMatALT R ) ) )
21.33.15.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 39820, 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 39821, so that we can show that such sets are submodules of the corresponding modules, see lincolss 39848. Remark:According to Wikipedia ("Linear span", 28-Apr-2019, https://en.wikipedia.org/wiki/Linear_span) "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 "Alternatively, 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 18194, the set of all linear combinations as defined by df-lco 39821 follows the alternative approach. That both definitions are equivalent is shown by lspeqlco 39853.
Syntax	clinc 39818	Extend class notation with the operation constructing a linear combination (of vectors from a left module).
class linC
Syntax	clinco 39819	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 39820*	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 .s. (Contributed by AV, 29-Mar-2019.)
|- linC = ( m e. _V |-> ( s e. ( ( Base ` (Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsumg ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) ) ) ) )
Definition	df-lco 39821*	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 = ( m e. _V , v e. ~P ( Base ` m ) |-> { c e. ( Base ` m ) | E. s e. ( ( Base ` (Scalar ` m ) ) ^m v ) ( s finSupp ( 0g ` (Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) ) } )
Theorem	lincop 39822*	A linear combination as operation. (Contributed by AV, 30-Mar-2019.)
|- ( M e. X -> ( linC ` M ) = ( s e. ( ( Base ` (Scalar ` M ) ) ^m v ) , v e. ~P ( Base ` M ) |-> ( M gsumg ( x e. v |-> ( ( s ` x ) ( .s ` M ) x ) ) ) ) )
Theorem	lincval 39823*	The value of a linear combination. (Contributed by AV, 30-Mar-2019.)
|- ( ( M e. X /\ S e. ( ( Base ` (Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( S ( linC ` M ) V ) = ( M gsumg ( x e. V |-> ( ( S ` x ) ( .s ` M ) x ) ) ) )
Theorem	dflinc2 39824*	Alternative definition of linear combinations using the function operation. (Contributed by AV, 1-Apr-2019.)
|- linC = ( m e. _V |-> ( s e. ( ( Base ` (Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsumg ( s oF ( .s ` m ) ( _I |` v ) ) ) ) )
Theorem	lcoop 39825*	A linear combination as operation. (Contributed by AV, 5-Apr-2019.) (Revised by AV, 28-Jul-2019.)
|- B = ( Base ` M )   &    |- S = (Scalar ` M )   &    |- R = ( Base ` S )   =>    |- ( ( M e. X /\ V e. ~P B ) -> ( M LinCo V ) = { c e. B | E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ c = ( s ( linC ` M ) V ) ) } )
Theorem	lcoval 39826*	The value of a linear combination. (Contributed by AV, 5-Apr-2019.) (Revised by AV, 28-Jul-2019.)
|- B = ( Base ` M )   &    |- S = (Scalar ` M )   &    |- R = ( Base ` S )   =>    |- ( ( M e. X /\ V e. ~P B ) -> ( C e. ( M LinCo V ) <-> ( C e. B /\ E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ C = ( s ( linC ` M ) V ) ) ) ) )
Theorem	lincfsuppcl 39827	A linear combination of vectors (with finite support) is a vector. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 28-Jul-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- S = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> ( F ( linC ` M ) V ) e. B )
Theorem	linccl 39828	A linear combination of vectors is a vector. (Contributed by AV, 31-Mar-2019.)
|- B = ( Base ` M )   &    |- R = ( Base ` (Scalar ` M ) )   =>    |- ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> ( S ( linC ` M ) V ) e. B )
Theorem	lincval0 39829	The value of an empty linear combination. (Contributed by AV, 12-Apr-2019.)
|- ( M e. X -> ( (/) ( linC ` M ) (/) ) = ( 0g ` M ) )
Theorem	lincvalsng 39830	The linear combination over a singleton. (Contributed by AV, 25-May-2019.)
|- B = ( Base ` M )   &    |- S = (Scalar ` M )   &    |- R = ( Base ` S )   &    |- .x. = ( .s ` M )   =>    |- ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( { <. V , Y >. } ( linC ` M ) { V } ) = ( Y .x. V ) )
Theorem	lincvalsn 39831	The linear combination over a singleton. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 25-May-2019.)
|- B = ( Base ` M )   &    |- S = (Scalar ` M )   &    |- R = ( Base ` S )   &    |- .x. = ( .s ` M )   &    |- F = { <. V , Y >. }   =>    |- ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( F ( linC ` M ) { V } ) = ( Y .x. V ) )
Theorem	lincvalpr 39832	The linear combination over an unordered pair. (Contributed by AV, 16-Apr-2019.)
|- B = ( Base ` M )   &    |- S = (Scalar ` M )   &    |- R = ( Base ` S )   &    |- .x. = ( .s ` M )   &    |- .+ = ( +g ` M )   &    |- F = { <. V , X >. , <. W , Y >. }   =>    |- ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> ( F ( linC ` M ) { V , W } ) = ( ( X .x. V ) .+ ( Y .x. W ) ) )
Theorem	lincval1 39833	The linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019.)
|- B = ( Base ` M )   &    |- S = (Scalar ` M )   &    |- R = ( Base ` S )   &    |- F = { <. V , ( 0g ` S ) >. }   =>    |- ( ( M e. LMod /\ V e. B ) -> ( F ( linC ` M ) { V } ) = ( 0g ` M ) )
Theorem	lcosn0 39834	Properties of a linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 28-Jul-2019.)
|- B = ( Base ` M )   &    |- S = (Scalar ` M )   &    |- R = ( Base ` S )   &    |- F = { <. V , ( 0g ` S ) >. }   =>    |- ( ( M e. LMod /\ V e. B ) -> ( F e. ( R ^m { V } ) /\ F finSupp ( 0g ` S ) /\ ( F ( linC ` M ) { V } ) = ( 0g ` M ) ) )
Theorem	lincvalsc0 39835*	The linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019.)
|- B = ( Base ` M )   &    |- S = (Scalar ` M )   &    |- .0. = ( 0g ` S )   &    |- Z = ( 0g ` M )   &    |- F = ( x e. V |-> .0. )   =>    |- ( ( M e. LMod /\ V e. ~P B ) -> ( F ( linC ` M ) V ) = Z )
Theorem	lcoc0 39836*	Properties of a linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 28-Jul-2019.)
|- B = ( Base ` M )   &    |- S = (Scalar ` M )   &    |- .0. = ( 0g ` S )   &    |- Z = ( 0g ` M )   &    |- F = ( x e. V |-> .0. )   &    |- R = ( Base ` S )   =>    |- ( ( M e. LMod /\ V e. ~P B ) -> ( F e. ( R ^m V ) /\ F finSupp .0. /\ ( F ( linC ` M ) V ) = Z ) )
Theorem	linc0scn0 39837*	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.)
|- B = ( Base ` M )   &    |- S = (Scalar ` M )   &    |- .0. = ( 0g ` S )   &    |- .1. = ( 1r ` S )   &    |- Z = ( 0g ` M )   &    |- F = ( x e. V |-> if ( x = Z , .1. , .0. ) )   =>    |- ( ( M e. LMod /\ V e. ~P B ) -> ( F ( linC ` M ) V ) = Z )
Theorem	lincdifsn 39838	A vector is a linear combination of a set containing this vector. (Contributed by AV, 21-Apr-2019.) (Revised by AV, 28-Jul-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- S = ( Base ` R )   &    |- .x. = ( .s ` M )   &    |- .+ = ( +g ` M )   &    |- .0. = ( 0g ` R )   =>    |- ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( F ( linC ` M ) V ) = ( ( G ( linC ` M ) ( V \ { X } ) ) .+ ( ( F ` X ) .x. X ) ) )
Theorem	linc1 39839*	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.)
|- B = ( Base ` M )   &    |- S = (Scalar ` M )   &    |- .0. = ( 0g ` S )   &    |- .1. = ( 1r ` S )   &    |- F = ( x e. V |-> if ( x = X , .1. , .0. ) )   =>    |- ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F ( linC ` M ) V ) = X )
Theorem	lincellss 39840	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.)
|- ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> ( ( F e. ( ( Base ` (Scalar ` M ) ) ^m V ) /\ F finSupp ( 0g ` (Scalar ` M ) ) ) -> ( F ( linC ` M ) V ) e. S ) )
Theorem	lco0 39841	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.)
|- ( M e. Mnd -> ( M LinCo (/) ) = { ( 0g ` M ) } )
Theorem	lcoel0 39842	The zero vector is always a linear combination. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
|- ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( 0g ` M ) e. ( M LinCo V ) )
Theorem	lincsum 39843	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 ` M )   &    |- X = ( A ( linC ` M ) V )   &    |- Y = ( B ( linC ` M ) V )   &    |- S = (Scalar ` M )   &    |- R = ( Base ` S )   &    |- .+b = ( +g ` S )   =>    |- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( X .+ Y ) = ( ( A oF .+b B ) ( linC ` M ) V ) )
Theorem	lincscm 39844*	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.)
|- .xb = ( .s ` M )   &    |- .x. = ( .r ` (Scalar ` M ) )   &    |- X = ( A ( linC ` M ) V )   &    |- R = ( Base ` (Scalar ` M ) )   &    |- F = ( x e. V |-> ( S .x. ( A ` x ) ) )   =>    |- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` (Scalar ` M ) ) ) -> ( S .xb X ) = ( F ( linC ` M ) V ) )
Theorem	lincsumcl 39845	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 ` M )   =>    |- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( C e. ( M LinCo V ) /\ D e. ( M LinCo V ) ) ) -> ( C .+ D ) e. ( M LinCo V ) )
Theorem	lincscmcl 39846	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.)
|- .x. = ( .s ` M )   &    |- R = ( Base ` (Scalar ` M ) )   =>    |- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R /\ D e. ( M LinCo V ) ) -> ( C .x. D ) e. ( M LinCo V ) )
Theorem	lincsumscmcl 39847	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.)
|- .x. = ( .s ` M )   &    |- R = ( Base ` (Scalar ` M ) )   &    |- .+ = ( +g ` M )   =>    |- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( C e. R /\ D e. ( M LinCo V ) /\ B e. ( M LinCo V ) ) ) -> ( ( C .x. D ) .+ B ) e. ( M LinCo V ) )
Theorem	lincolss 39848	According to the statement in [Lang] p. 129, the set ( LSubSp ` M ) 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 ` M ). (Contributed by AV, 12-Apr-2019.)
|- ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( M LinCo V ) e. ( LSubSp ` M ) )
Theorem	ellcoellss 39849*	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.)
|- ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> A. x e. ( M LinCo V ) x e. S )
Theorem	lcoss 39850	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.)
|- ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> V C_ ( M LinCo V ) )
Theorem	lspsslco 39851	Lemma for lspeqlco 39853. (Contributed by AV, 17-Apr-2019.)
|- B = ( Base ` M )   =>    |- ( ( M e. LMod /\ V e. ~P B ) -> ( ( LSpan ` M ) ` V ) C_ ( M LinCo V ) )
Theorem	lcosslsp 39852	Lemma for lspeqlco 39853. (Contributed by AV, 20-Apr-2019.)
|- B = ( Base ` M )   =>    |- ( ( M e. LMod /\ V e. ~P B ) -> ( M LinCo V ) C_ ( ( LSpan ` M ) ` V ) )
Theorem	lspeqlco 39853	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 18194) and as the set of all linear combinations of the vectors of the set with finite support. (Contributed by AV, 20-Apr-2019.)
|- B = ( Base ` M )   =>    |- ( ( M e. LMod /\ V e. ~P B ) -> ( M LinCo V ) = ( ( LSpan ` M ) ` V ) )
21.33.15.3  Linear independency 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 39856 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 independency is defined for vector spaces, see Wikipedia ("Linear independence", 15-Apr-2019, https://en.wikipedia.org/wiki/Linear_independence): "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 non-zero, 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 19362) and (linearly) independent sets (df-linds 19363). 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 18303) "every element is not in the span of the remainder of the [set]". The equivalence of the definitions df-linds 19363 and df-lininds 39856 for (linear) independency for (left) modules is shown in lindslininds 39878. Remark 2: Subsets of the base set of a (left) module are linearly dependent if they are not linearly indepent (see df-lindeps 39858) 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 39897. 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 with our definition for (left) vector spaces (see isldepslvec2 39899) and not for (left) modules in general.
Syntax	clininds 39854	Extend class notation with the relation between a module and its linearly independent subsets.
class linIndS
Syntax	clindeps 39855	Extend class notation with the relation between a module and its linearly dependent subsets.
class linDepS
Definition	df-lininds 39856*	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 = { <. s , m >. | ( s e. ~P ( Base ` m ) /\ A. f e. ( ( Base ` (Scalar ` m ) ) ^m s ) ( ( f finSupp ( 0g ` (Scalar ` m ) ) /\ ( f ( linC ` m ) s ) = ( 0g ` m ) ) -> A. x e. s ( f ` x ) = ( 0g ` (Scalar ` m ) ) ) ) }
Theorem	rellininds 39857	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 39858*	Define the relation between a module and its linearly dependent subsets. (Contributed by AV, 26-Apr-2019.)
|- linDepS = { <. s , m >. | -. s linIndS m }
Theorem	linindsv 39859	The classes of the module and its linearly independent subsets are sets. (Contributed by AV, 13-Apr-2019.)
|- ( S linIndS M -> ( S e. _V /\ M e. _V ) )
Theorem	islininds 39860*	The property of being a linearly independent subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 30-Jul-2019.)
|- B = ( Base ` M )   &    |- Z = ( 0g ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( S e. V /\ M e. W ) -> ( S linIndS M <-> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) )
Theorem	linindsi 39861*	The implications of being a linearly independent subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 30-Jul-2019.)
|- B = ( Base ` M )   &    |- Z = ( 0g ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( S linIndS M -> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) )
Theorem	linindslinci 39862*	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.)
|- B = ( Base ` M )   &    |- Z = ( 0g ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( S linIndS M /\ ( F e. ( E ^m S ) /\ F finSupp .0. /\ ( F ( linC ` M ) S ) = Z ) ) -> A. x e. S ( F ` x ) = .0. )
Theorem	islinindfis 39863*	The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-2019.)
|- B = ( Base ` M )   &    |- Z = ( 0g ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( S e. Fin /\ M e. W ) -> ( S linIndS M <-> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) ) )
Theorem	islinindfiss 39864*	The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-2019.)
|- B = ( Base ` M )   &    |- Z = ( 0g ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( M e. W /\ S e. Fin /\ S e. ~P B ) -> ( S linIndS M <-> A. f e. ( E ^m S ) ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) )
Theorem	linindscl 39865	A linearly independent set is a subset of (the base set of) a module. (Contributed by AV, 13-Apr-2019.)
|- ( S linIndS M -> S e. ~P ( Base ` M ) )
Theorem	lindepsnlininds 39866	A linearly dependent subset is not a linearly independent subset. (Contributed by AV, 26-Apr-2019.)
|- ( ( S e. V /\ M e. W ) -> ( S linDepS M <-> -. S linIndS M ) )
Theorem	islindeps 39867*	The property of being a linearly dependent subset. (Contributed by AV, 26-Apr-2019.) (Revised by AV, 30-Jul-2019.)
|- B = ( Base ` M )   &    |- Z = ( 0g ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( M e. W /\ S e. ~P B ) -> ( S linDepS M <-> E. f e. ( E ^m S ) ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z /\ E. x e. S ( f ` x ) =/= .0. ) ) )
Theorem	lincext1 39868*	Property 1 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 29-Apr-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- N = ( invg ` R )   &    |- F = ( z e. S |-> if ( z = X , ( N ` Y ) , ( G ` z ) ) )   =>    |- ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> F e. ( E ^m S ) )
Theorem	lincext2 39869*	Property 2 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 30-Jul-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- N = ( invg ` R )   &    |- F = ( z e. S |-> if ( z = X , ( N ` Y ) , ( G ` z ) ) )   =>    |- ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ G finSupp .0. ) -> F finSupp .0. )
Theorem	lincext3 39870*	Property 3 of an extension of a linear combination. (Contributed by AV, 23-Apr-2019.) (Revised by AV, 30-Jul-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- N = ( invg ` R )   &    |- F = ( z e. S |-> if ( z = X , ( N ` Y ) , ( G ` z ) ) )   =>    |- ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ ( G finSupp .0. /\ ( Y ( .s ` M ) X ) = ( G ( linC ` M ) ( S \ { X } ) ) ) ) -> ( F ( linC ` M ) S ) = Z )
Theorem	lindslinindsimp1 39871*	Implication 1 for lindslininds 39878. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.)
|- R = (Scalar ` M )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   =>    |- ( ( S e. V /\ M e. LMod ) -> ( ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) -> ( S C_ ( Base ` M ) /\ A. s e. S A. y e. ( B \ { .0. } ) -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) ) )
Theorem	lindslinindimp2lem1 39872*	Lemma 1 for lindslinindsimp2 39877. (Contributed by AV, 25-Apr-2019.)
|- R = (Scalar ` M )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- Y = ( ( invg ` R ) ` ( f ` x ) )   &    |- G = ( f |` ( S \ { x } ) )   =>    |- ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S /\ f e. ( B ^m S ) ) ) -> Y e. B )
Theorem	lindslinindimp2lem2 39873*	Lemma 2 for lindslinindsimp2 39877. (Contributed by AV, 25-Apr-2019.)
|- R = (Scalar ` M )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- Y = ( ( invg ` R ) ` ( f ` x ) )   &    |- G = ( f |` ( S \ { x } ) )   =>    |- ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S /\ f e. ( B ^m S ) ) ) -> G e. ( B ^m ( S \ { x } ) ) )
Theorem	lindslinindimp2lem3 39874*	Lemma 3 for lindslinindsimp2 39877. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.)
|- R = (Scalar ` M )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- Y = ( ( invg ` R ) ` ( f ` x ) )   &    |- G = ( f |` ( S \ { x } ) )   =>    |- ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) /\ ( f e. ( B ^m S ) /\ f finSupp .0. ) ) -> G finSupp .0. )
Theorem	lindslinindimp2lem4 39875*	Lemma 4 for lindslinindsimp2 39877. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.)
|- R = (Scalar ` M )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- Y = ( ( invg ` R ) ` ( f ` x ) )   &    |- G = ( f |` ( S \ { x } ) )   =>    |- ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) /\ ( f e. ( B ^m S ) /\ f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) -> ( M gsumg ( y e. ( S \ { x } ) |-> ( ( f ` y ) ( .s ` M ) y ) ) ) = ( Y ( .s ` M ) x ) )
Theorem	lindslinindsimp2lem5 39876*	Lemma 5 for lindslinindsimp2 39877. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.)
|- R = (Scalar ` M )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   =>    |- ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( ( f e. ( B ^m S ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) -> ( A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) -> ( f ` x ) = .0. ) ) )
Theorem	lindslinindsimp2 39877*	Implication 2 for lindslininds 39878. (Contributed by AV, 26-Apr-2019.) (Revised by AV, 30-Jul-2019.)
|- R = (Scalar ` M )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   =>    |- ( ( S e. V /\ M e. LMod ) -> ( ( S C_ ( Base ` M ) /\ A. s e. S A. y e. ( B \ { .0. } ) -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) -> ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) )
Theorem	lindslininds 39878	Equivalence of definitions df-linds 19363 and df-lininds 39856 for (linear) independency for (left) modules. (Contributed by AV, 26-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
|- ( ( S e. V /\ M e. LMod ) -> ( S linIndS M <-> S e. (LIndS ` M ) ) )
Theorem	linds0 39879	The empty set is always a linearly independet subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 27-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
|- ( M e. V -> (/) linIndS M )
Theorem	el0ldep 39880	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.)
|- ( ( ( M e. LMod /\ 1 < ( # ` ( Base ` (Scalar ` M ) ) ) ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> S linDepS M )
Theorem	el0ldepsnzr 39881	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.)
|- ( ( ( M e. LMod /\ (Scalar ` M ) e. NzRing ) /\ S e. ~P ( Base ` M ) /\ ( 0g ` M ) e. S ) -> S linDepS M )
Theorem	lindsrng01 39882	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 18103), 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.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   =>    |- ( ( M e. LMod /\ ( ( # ` E ) = 0 \/ ( # ` E ) = 1 ) /\ S e. ~P B ) -> S linIndS M )
Theorem	lindszr 39883	Any subset of a module over a zero ring is always linearly independent. (Contributed by AV, 27-Apr-2019.)
|- ( ( M e. LMod /\ -. (Scalar ` M ) e. NzRing /\ S e. ~P ( Base ` M ) ) -> S linIndS M )
Theorem	snlindsntorlem 39884*	Lemma for snlindsntor 39885. (Contributed by AV, 15-Apr-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- S = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- .x. = ( .s ` M )   =>    |- ( ( M e. LMod /\ X e. B ) -> ( A. f e. ( S ^m { X } ) ( ( f ( linC ` M ) { X } ) = Z -> ( f ` X ) = .0. ) -> A. s e. S ( ( s .x. X ) = Z -> s = .0. ) ) )
Theorem	snlindsntor 39885*	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., ( r .x. m ) = 0. In an integral domain (a commutative ring without zero divisors), every non-zero element is regular, so a torsion element of a module over an integral domain is one annihilated by a non-zero 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 a e. R, a =/= 0, such that a .x. x = 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.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- S = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- .x. = ( .s ` M )   =>    |- ( ( M e. LMod /\ X e. B ) -> ( A. s e. ( S \ { .0. } ) ( s .x. X ) =/= Z <-> { X } linIndS M ) )
Theorem	ldepsprlem 39886	Lemma for ldepspr 39887. (Contributed by AV, 16-Apr-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- S = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- .x. = ( .s ` M )   &    |- .1. = ( 1r ` R )   &    |- N = ( invg ` R )   =>    |- ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( X = ( A .x. Y ) -> ( ( .1. .x. X ) ( +g ` M ) ( ( N ` A ) .x. Y ) ) = Z ) )
Theorem	ldepspr 39887	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.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- S = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- .x. = ( .s ` M )   =>    |- ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) -> ( ( A e. S /\ X = ( A .x. Y ) ) -> { X , Y } linDepS M ) )
Theorem	lincresunit3lem3 39888	Lemma 3 for lincresunit3 39895. (Contributed by AV, 18-May-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- U = (Unit ` R )   &    |- N = ( invg ` R )   &    |- .x. = ( .s ` M )   =>    |- ( ( ( M e. LMod /\ X e. B /\ Y e. B ) /\ A e. U ) -> ( ( ( N ` A ) .x. X ) = ( ( N ` A ) .x. Y ) <-> X = Y ) )
Theorem	lincresunitlem1 39889	Lemma 1 for properties of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- N = ( invg ` R )   &    |- I = ( invr ` R )   &    |- .x. = ( .r ` R )   &    |- G = ( s e. ( S \ { X } ) |-> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) )   =>    |- ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) -> ( I ` ( N ` ( F ` X ) ) ) e. E )
Theorem	lincresunitlem2 39890	Lemma for properties of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- N = ( invg ` R )   &    |- I = ( invr ` R )   &    |- .x. = ( .r ` R )   &    |- G = ( s e. ( S \ { X } ) |-> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) )   =>    |- ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) /\ Y e. S ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` Y ) ) e. E )
Theorem	lincresunit1 39891*	Property 1 of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- N = ( invg ` R )   &    |- I = ( invr ` R )   &    |- .x. = ( .r ` R )   &    |- G = ( s e. ( S \ { X } ) |-> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) )   =>    |- ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) -> G e. ( E ^m ( S \ { X } ) ) )
Theorem	lincresunit2 39892*	Property 2 of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- N = ( invg ` R )   &    |- I = ( invr ` R )   &    |- .x. = ( .r ` R )   &    |- G = ( s e. ( S \ { X } ) |-> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) )   =>    |- ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> G finSupp .0. )
Theorem	lincresunit3lem1 39893*	Lemma 1 for lincresunit3 39895. (Contributed by AV, 17-May-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- N = ( invg ` R )   &    |- I = ( invr ` R )   &    |- .x. = ( .r ` R )   &    |- G = ( s e. ( S \ { X } ) |-> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) )   =>    |- ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( ( N ` ( F ` X ) ) ( .s ` M ) ( ( G ` z ) ( .s ` M ) z ) ) = ( ( F ` z ) ( .s ` M ) z ) )
Theorem	lincresunit3lem2 39894*	Lemma 2 for lincresunit3 39895. (Contributed by AV, 18-May-2019.) (Proof shortened by AV, 30-Jul-2019.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- N = ( invg ` R )   &    |- I = ( invr ` R )   &    |- .x. = ( .r ` R )   &    |- G = ( s e. ( S \ { X } ) |-> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) )   =>    |- ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsumg ( z e. ( S \ { X } ) |-> ( ( G ` z ) ( .s ` M ) z ) ) ) ) = ( ( F |` ( S \ { X } ) ) ( linC ` M ) ( S \ { X } ) ) )
Theorem	lincresunit3 39895*	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.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- N = ( invg ` R )   &    |- I = ( invr ` R )   &    |- .x. = ( .r ` R )   &    |- G = ( s e. ( S \ { X } ) |-> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) )   =>    |- ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) /\ ( F ( linC ` M ) S ) = Z ) -> ( G ( linC ` M ) ( S \ { X } ) ) = X )
Theorem	lincreslvec3 39896*	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.)
|- B = ( Base ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   &    |- Z = ( 0g ` M )   &    |- N = ( invg ` R )   &    |- I = ( invr ` R )   &    |- .x. = ( .r ` R )   &    |- G = ( s e. ( S \ { X } ) |-> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) )   =>    |- ( ( ( S e. ~P B /\ M e. LVec /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) =/= .0. /\ F finSupp .0. ) /\ ( F ( linC ` M ) S ) = Z ) -> ( G ( linC ` M ) ( S \ { X } ) ) = X )
Theorem	islindeps2 39897*	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.)
|- B = ( Base ` M )   &    |- Z = ( 0g ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) -> S linDepS M ) )
Theorem	islininds2 39898*	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.)
|- B = ( Base ` M )   &    |- Z = ( 0g ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( S linIndS M -> A. s e. S A. f e. ( E ^m ( S \ { s } ) ) ( -. f finSupp .0. \/ ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) ) )
Theorem	isldepslvec2 39899*	Alternative definition of being a linearly dependent subset of a (left) vector space. In this case, the reverse implication of islindeps2 39897 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.)
|- B = ( Base ` M )   &    |- Z = ( 0g ` M )   &    |- R = (Scalar ` M )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( M e. LVec /\ S e. ~P B ) -> ( E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) <-> S linDepS M ) )
Theorem	lindssnlvec 39900	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.)
|- ( ( M e. LVec /\ S e. ( Base ` M ) /\ S =/= ( 0g ` M ) ) -> { S } linIndS M )