P. 326 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32501-32600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lincvalpr 32501	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 32502	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 32503	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 32504*	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 32505*	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 32506*	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 32507	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 32508*	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 32509	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 32510	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 32511	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 32512	The sum of two linear combinations is a linear combination, see also [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 32513*	A linear combinations multiplied with a scalar is a linear combination, see also [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 32514	The sum of two linear combinations is a linear combination, see also [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 32515	The multiplication of a linear combination with a scalar is a linear combination, see also [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 32516	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 32517	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 32518*	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 32519	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 32520	Lemma for lspeqlco 32522. (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 32521	Lemma for lspeqlco 32522. (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 32522	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 17489) 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.25.9.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 32525 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 18710) and (linearly) independent sets (df-linds 18711). 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 17598) "every element is not in the span of the remainder of the [set]". The equivalence of the definitions df-linds 18711 and df-lininds 32525 for (linear) independency for (left) modules is shown in lindslininds 32547. Remark 2: Subsets of the base set of a (left) module are linearly dependent if they are not linearly indepent (see df-lindeps 32527) 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 32566. 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 32568) and not for (left) modules in general.
Syntax	clininds 32523	Extend class notation with the relation between a module and its linearly independent subsets.
class linIndS
Syntax	clindeps 32524	Extend class notation with the relation between a module and its linearly dependent subsets.
class linDepS
Definition	df-lininds 32525*	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 32526	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 32527*	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 32528	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 32529*	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 32530*	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 32531*	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 32532*	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 32533*	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 32534	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 32535	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 32536*	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 32537*	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 32538*	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 32539*	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 32540*	Implication 1 for lindslininds 32547. (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 32541*	Lemma 1 for lindslinindsimp2 32546. (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 32542*	Lemma 2 for lindslinindsimp2 32546. (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 32543*	Lemma 3 for lindslinindsimp2 32546. (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 32544*	Lemma 4 for lindslinindsimp2 32546. (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 32545*	Lemma 5 for lindslinindsimp2 32546. (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 32546*	Implication 2 for lindslininds 32547. (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 32547	Equivalence of definitions df-linds 18711 and df-lininds 32525 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 32548	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 32549	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 32550	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 32551	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 17396), 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 32552	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 32553*	Lemma for snlindsntor 32554. (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 32554*	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 32555	Lemma for ldepspr 32556. (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 32556	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 32557	Lemma 3 for lincresunit3 32564. (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 32558	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 32559	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 32560*	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 32561*	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 32562*	Lemma 1 for lincresunit3 32564. (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 32563*	Lemma 2 for lincresunit3 32564. (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 32564*	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 32565*	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 32566*	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 32567*	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 32568*	Alternative definition of being a linearly dependent subset of a (left) vector space. In this case, the reverse implication of islindeps2 32566 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 32569	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 )
21.25.9.4  Simple left modules and the ` ZZ `-module
Theorem	lmod1lem1 32570*	Lemma 1 for lmod1 32575. (Contributed by AV, 28-Apr-2019.)
|- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. (Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } )   =>    |- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( r ( .s ` M ) I ) e. { I } )
Theorem	lmod1lem2 32571*	Lemma 2 for lmod1 32575. (Contributed by AV, 28-Apr-2019.)
|- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. (Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } )   =>    |- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) )
Theorem	lmod1lem3 32572*	Lemma 3 for lmod1 32575. (Contributed by AV, 29-Apr-2019.)
|- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. (Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } )   =>    |- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( q ( +g ` (Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) )
Theorem	lmod1lem4 32573*	Lemma 4 for lmod1 32575. (Contributed by AV, 29-Apr-2019.)
|- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. (Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } )   =>    |- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( q ( .r ` (Scalar ` M ) ) r ) ( .s ` M ) I ) = ( q ( .s ` M ) ( r ( .s ` M ) I ) ) )
Theorem	lmod1lem5 32574*	Lemma 5 for lmod1 32575. (Contributed by AV, 28-Apr-2019.)
|- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. (Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } )   =>    |- ( ( I e. V /\ R e. Ring ) -> ( ( 1r ` (Scalar ` M ) ) ( .s ` M ) I ) = I )
Theorem	lmod1 32575*	The (smallest) structure representing a zero module over an arbitrary ring. (Contributed by AV, 29-Apr-2019.)
|- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. (Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } )   =>    |- ( ( I e. V /\ R e. Ring ) -> M e. LMod )
Theorem	lmod1zr 32576	The (smallest) structure representing a zero module over a zero ring. (Contributed by AV, 29-Apr-2019.)
|- R = { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. }   &    |- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. (Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , { <. <. Z , I >. , I >. } >. } )   =>    |- ( ( I e. V /\ Z e. W ) -> M e. LMod )
Theorem	lmod1zrnlvec 32577	There is a (left) module (a zero module) which is not a (left) vector space. (Contributed by AV, 29-Apr-2019.)
|- R = { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. }   &    |- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. (Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , { <. <. Z , I >. , I >. } >. } )   =>    |- ( ( I e. V /\ Z e. W ) -> M e/ LVec )
Theorem	lmodn0 32578	Left modules exist. (Contributed by AV, 29-Apr-2019.)
|- LMod =/= (/)
Theorem	zlmodzxzequa 32579	Example of an equation within the ZZ-module ZZ X. ZZ (see example for a linearly dependent set in [Roman] p. 113). (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- .0. = { <. 0 , 0 >. , <. 1 , 0 >. }   &    |- .xb = ( .s ` Z )   &    |- .- = ( -g ` Z )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   =>    |- ( ( 2 .xb A ) .- ( 3 .xb B ) ) = .0.
Theorem	zlmodzxznm 32580	Example of a linearly dependent set whose elements are not linear combinations of the others, see note in [Roman] p. 113). (Contributed by AV, 23-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- .0. = { <. 0 , 0 >. , <. 1 , 0 >. }   &    |- .xb = ( .s ` Z )   &    |- .- = ( -g ` Z )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   =>    |- A. i e. ZZ ( ( i .xb A ) =/= B /\ ( i .xb B ) =/= A )
Theorem	zlmodzxzldeplem 32581	A and B are not equal. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   =>    |- A =/= B
Theorem	zlmodzxzequap 32582	Example of an equation within the ZZ-module ZZ X. ZZ (see example for a linearly dependent set in [Roman] p. 113), written as a sum. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   &    |- .0. = { <. 0 , 0 >. , <. 1 , 0 >. }   &    |- .+ = ( +g ` Z )   &    |- .xb = ( .s ` Z )   =>    |- ( ( 2 .xb A ) .+ ( -u 3 .xb B ) ) = .0.
Theorem	zlmodzxzldeplem1 32583	Lemma 1 for zlmodzxzldep 32587. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   &    |- F = { <. A , 2 >. , <. B , -u 3 >. }   =>    |- F e. ( ZZ ^m { A , B } )
Theorem	zlmodzxzldeplem2 32584	Lemma 2 for zlmodzxzldep 32587. (Contributed by AV, 24-May-2019.) (Revised by AV, 30-Jul-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   &    |- F = { <. A , 2 >. , <. B , -u 3 >. }   =>    |- F finSupp 0
Theorem	zlmodzxzldeplem3 32585	Lemma 3 for zlmodzxzldep 32587. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   &    |- F = { <. A , 2 >. , <. B , -u 3 >. }   =>    |- ( F ( linC ` Z ) { A , B } ) = ( 0g ` Z )
Theorem	zlmodzxzldeplem4 32586*	Lemma 4 for zlmodzxzldep 32587. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   &    |- F = { <. A , 2 >. , <. B , -u 3 >. }   =>    |- E. y e. { A , B } ( F ` y ) =/= 0
Theorem	zlmodzxzldep 32587	{ A , B } is a linearly dependent set within the ZZ-module ZZ X. ZZ (see [Roman] p. 113). (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   =>    |- { A , B } linDepS Z
Theorem	ldepsnlinclem1 32588	Lemma 1 for ldepsnlinc 32591. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   =>    |- ( F e. ( ( Base ` ℤring ) ^m { B } ) -> ( F ( linC ` Z ) { B } ) =/= A )
Theorem	ldepsnlinclem2 32589	Lemma 2 for ldepsnlinc 32591. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   =>    |- ( F e. ( ( Base ` ℤring ) ^m { A } ) -> ( F ( linC ` Z ) { A } ) =/= B )
21.25.9.5  Differences between (left) modules and (left) vector spaces
Theorem	lvecpsslmod 32590	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 17623) 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 32577. (Contributed by AV, 29-Apr-2019.)
|- LVec C. LMod
Theorem	ldepsnlinc 32591*	The reverse implication of islindeps2 32566 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 combinantion of the other elements of this subset. Such a left module can be constructed by using zlmodzxzequa 32579 and zlmodzxznm 32580 (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.)
|- E. m e. LMod E. s e. ~P ( Base ` m ) ( s linDepS m /\ A. v e. s A. f e. ( ( Base ` (Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` (Scalar ` m ) ) -> ( f ( linC ` m ) ( s \ { v } ) ) =/= v ) )
Theorem	ldepslinc 32592*	For (left) vector spaces, isldepslvec2 32568 provides an alternative definition of being a linearly dependent subset, whereas ldepsnlinc 32591 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.)
|- ( A. m e. LVec A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` (Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` (Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) /\ -. A. m e. LMod A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` (Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` (Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) )
21.26  Mathbox for David A. Wheeler This is the mathbox of David A. Wheeler, dwheeler at dwheeler dot com. Among other things, I have added a number of formal definitions for widely-used functions, e.g., those defined in ISO 80000-2:2009(E) Quantities and units - Part 2: Mathematical signs and symbols used in the natural sciences and technology and the NIST Digital Library of Mathematical Functions http://dlmf.nist.gov/.
21.26.1  Natural deduction
Theorem	19.8ad 32593	If a wff is true, it is true for at least one instance. Deductive form of 19.8a 1806. (Contributed by DAW, 13-Feb-2017.)
|- ( ph -> ps )   =>    |- ( ph -> E. x ps )
Theorem	sbidd 32594	An identity theorem for substitution. See sbid 1965. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.)
|- ( ph -> [ x / x ] ps )   =>    |- ( ph -> ps )
Theorem	sbidd-misc 32595	An identity theorem for substitution. See sbid 1965. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.)
|- ( ( ph -> [ x / x ] ps ) <-> ( ph -> ps ) )
21.26.2  Greater than, greater than or equal to. As a stylistic issue, set.mm prefers 'less than' instead of 'greater than' to reduce the number of conversion steps. Here we formally define the widely-used relations 'greater than' and 'greater than or equal to', so that we have formal definitions of them, as well as a few related theorems.
Syntax	cge-real 32596	Extend wff notation to include the 'greater than or equal to' relation, see df-gte 32598.
class >_
Syntax	cgt 32597	Extend wff notation to include the 'greater than' relation, see df-gt 32599.
class >
Definition	df-gte 32598	Define the 'greater than or equal' predicate over the reals. Defined in ISO 80000-2:2009(E) operation 2-7.10. It is used as a primitive in the "NIST Digital Library of Mathematical Functions" , front introduction, "Common Notations and Definitions" section at http://dlmf.nist.gov/front/introduction#Sx4. This relation is merely the converse of the 'less than or equal to' relation defined by df-le 9646. We do not write this as ( x >_ y <-> y <_ x ), and similarly we do not write ` > ` as ( x > y <-> y < x ), because these are not definitional axioms as understood by mmj2 (those definitions will be flagged as being "potentially non-conservative"). We could write them this way: |- > = { <. x , y >. | ( ( x e. RR* /\ y e. RR* ) /\ y < x ) } and |- >_ = { <. x , y >. | ( ( x e. RR* /\ y e. RR* ) /\ y <_ x ) } but these are very complicated. This definition of >_, and the similar one for > (df-gt 32599), are a bit strange when you see them for the first time, but these definitions are much simpler for us to process and are clearly conservative definitions. (My thanks to Mario Carneiro for pointing out this simpler approach.) See gte-lte 32600 for a more conventional expression of the relationship between < and >. As a stylistic issue, set.mm prefers 'less than' instead of 'greater than' to reduce the number of conversion steps. Thus, we discourage its use, but include its definition so that there is a formal definition of this symbol. (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.)
|- >_ = `' <_
Definition	df-gt 32599	The 'greater than' relation is merely the converse of the 'less than or equal to' relation defined by df-lt 9517. Defined in ISO 80000-2:2009(E) operation 2-7.12. See df-gte 32598 for a discussion on why this approach is used for the definition. See gt-lt 32601 and gt-lth 32603 for more conventional expression of the relationship between < and >. As a stylistic issue, set.mm prefers 'less than or equal' instead of 'greater than or equal' to reduce the number of conversion steps. Thus, we discourage its use, but include its definition so that there is a formal definition of this symbol. (Contributed by David A. Wheeler, 19-Apr-2015.) (New usage is discouraged.)
|- > = `' <
Theorem	gte-lte 32600	Simple relationship between <_ and >_. (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.)
|- ( ( A e. _V /\ B e. _V ) -> ( A >_ B <-> B <_ A ) )