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 \in V \land M \in W) \to (S linDepS M \leftrightarrow \neg S linIndS M)$

Step	Hyp	Ref	Expression
1		breq12	$⊢ (s = S \land m = M) \to (s linIndS m \leftrightarrow S linIndS M)$
2	1	notbid	$⊢ (s = S \land m = M) \to (\neg s linIndS m \leftrightarrow \neg S linIndS M)$
3		df-lindeps	$⊢ linDepS = \{⟨s, m⟩ \| \neg s linIndS m\}$
4	2 3	brabga	$⊢ (S \in V \land M \in W) \to (S linDepS M \leftrightarrow \neg S linIndS M)$