Description: A linearly dependent subset is not a linearly independent subset. (Contributed by AV, 26Apr2019)
Ref  Expression  

Assertion  lindepsnlininds   ( ( S e. V /\ M e. W ) > ( S linDepS M <> . S linIndS M ) ) 
Step  Hyp  Ref  Expression 

1  breq12   ( ( s = S /\ m = M ) > ( s linIndS m <> S linIndS M ) ) 

2  1  notbid   ( ( s = S /\ m = M ) > ( . s linIndS m <> . S linIndS M ) ) 
3  dflindeps   linDepS = { <. s , m >.  . s linIndS m } 

4  2 3  brabga   ( ( S e. V /\ M e. W ) > ( S linDepS M <> . S linIndS M ) ) 