Metamath Proof Explorer

Theorem lindepsnlininds

Description: A linearly dependent subset is not a linearly independent subset. (Contributed by AV, 26-Apr-2019)

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

Proof

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 df-lindeps 
 |-  linDepS = { <. s , m >. | -. s linIndS m }
4 2 3 brabga 
 |-  ( ( S e. V /\ M e. W ) -> ( S linDepS M <-> -. S linIndS M ) )