Description: Alternative definition of being a linearly dependent subset of a (left) vector space. In this case, the reverse implication of islindeps2 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)
Ref | Expression | ||
---|---|---|---|
Hypotheses | islindeps2.b | |
|
islindeps2.z | |
||
islindeps2.r | |
||
islindeps2.e | |
||
islindeps2.0 | |
||
Assertion | isldepslvec2 | |