islindeps

Description: The property of being a linearly dependent subset. (Contributed by AV, 26-Apr-2019) (Revised by AV, 30-Jul-2019)

	Ref	Expression
Hypotheses	islindeps.b	$⊢ B = {Base}_{M}$
	islindeps.z	$⊢ Z = 0_{M}$
	islindeps.r	$⊢ R = Scalar (M)$
	islindeps.e	$⊢ E = {Base}_{R}$
	islindeps.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	islindeps	$⊢ (M \in W \land S \in 𝒫 B) \to (S linDepS M \leftrightarrow \exists f \in (E^{S}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z \land \exists x \in S f (x) \neq \underset{˙}{0}))$

Proof

Step	Hyp	Ref	Expression
1		islindeps.b	$⊢ B = {Base}_{M}$
2		islindeps.z	$⊢ Z = 0_{M}$
3		islindeps.r	$⊢ R = Scalar (M)$
4		islindeps.e	$⊢ E = {Base}_{R}$
5		islindeps.0	$⊢ \underset{˙}{0} = 0_{R}$
6		lindepsnlininds	$⊢ (S \in 𝒫 B \land M \in W) \to (S linDepS M \leftrightarrow \neg S linIndS M)$
7	6	ancoms	$⊢ (M \in W \land S \in 𝒫 B) \to (S linDepS M \leftrightarrow \neg S linIndS M)$
8	1 2 3 4 5	islininds	$⊢ (S \in 𝒫 B \land M \in W) \to (S linIndS M \leftrightarrow (S \in 𝒫 B \land \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})))$
9	8	ancoms	$⊢ (M \in W \land S \in 𝒫 B) \to (S linIndS M \leftrightarrow (S \in 𝒫 B \land \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})))$
10		ibar	$⊢ S \in 𝒫 B \to (\forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \leftrightarrow (S \in 𝒫 B \land \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})))$
11	10	bicomd	$⊢ S \in 𝒫 B \to ((S \in 𝒫 B \land \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})) \leftrightarrow \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))$
12	11	adantl	$⊢ (M \in W \land S \in 𝒫 B) \to ((S \in 𝒫 B \land \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})) \leftrightarrow \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))$
13	9 12	bitrd	$⊢ (M \in W \land S \in 𝒫 B) \to (S linIndS M \leftrightarrow \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))$
14	13	notbid	$⊢ (M \in W \land S \in 𝒫 B) \to (\neg S linIndS M \leftrightarrow \neg \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))$
15		rexnal	$⊢ \exists f \in (E^{S}) \neg (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \leftrightarrow \neg \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})$
16		df-ne	$⊢ f (x) \neq \underset{˙}{0} \leftrightarrow \neg f (x) = \underset{˙}{0}$
17	16	rexbii	$⊢ \exists x \in S f (x) \neq \underset{˙}{0} \leftrightarrow \exists x \in S \neg f (x) = \underset{˙}{0}$
18		rexnal	$⊢ \exists x \in S \neg f (x) = \underset{˙}{0} \leftrightarrow \neg \forall x \in S f (x) = \underset{˙}{0}$
19	17 18	bitr2i	$⊢ \neg \forall x \in S f (x) = \underset{˙}{0} \leftrightarrow \exists x \in S f (x) \neq \underset{˙}{0}$
20	19	anbi2i	$⊢ (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \land \neg \forall x \in S f (x) = \underset{˙}{0}) \leftrightarrow (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \land \exists x \in S f (x) \neq \underset{˙}{0})$
21		pm4.61	$⊢ \neg (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \leftrightarrow (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \land \neg \forall x \in S f (x) = \underset{˙}{0})$
22		df-3an	$⊢ ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z \land \exists x \in S f (x) \neq \underset{˙}{0}) \leftrightarrow (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \land \exists x \in S f (x) \neq \underset{˙}{0})$
23	20 21 22	3bitr4i	$⊢ \neg (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \leftrightarrow ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z \land \exists x \in S f (x) \neq \underset{˙}{0})$
24	23	rexbii	$⊢ \exists f \in (E^{S}) \neg (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \leftrightarrow \exists f \in (E^{S}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z \land \exists x \in S f (x) \neq \underset{˙}{0})$
25	15 24	bitr3i	$⊢ \neg \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \leftrightarrow \exists f \in (E^{S}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z \land \exists x \in S f (x) \neq \underset{˙}{0})$
26	25	a1i	$⊢ (M \in W \land S \in 𝒫 B) \to (\neg \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \leftrightarrow \exists f \in (E^{S}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z \land \exists x \in S f (x) \neq \underset{˙}{0}))$
27	7 14 26	3bitrd	$⊢ (M \in W \land S \in 𝒫 B) \to (S linDepS M \leftrightarrow \exists f \in (E^{S}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z \land \exists x \in S f (x) \neq \underset{˙}{0}))$

Metamath Proof Explorer

Theorem islindeps

Proof