ldepslinc

Description: For (left) vector spaces, isldepslvec2 provides an alternative definition of being a linearly dependent subset, whereas ldepsnlinc indicates that there is not an analogous alternative definition for arbitrary (left) modules. (Contributed by AV, 25-May-2019) (Revised by AV, 30-Jul-2019)

		Ref	Expression
	Assertion	ldepslinc	$⊢ (\forall m \in LVec \forall s \in 𝒫 {Base}_{m} (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \land \neg \forall m \in LMod \forall s \in 𝒫 {Base}_{m} (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)))$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{m} = {Base}_{m}$
2		eqid	$⊢ 0_{m} = 0_{m}$
3		eqid	$⊢ Scalar (m) = Scalar (m)$
4		eqid	$⊢ {Base}_{Scalar (m)} = {Base}_{Scalar (m)}$
5		eqid	$⊢ 0_{Scalar (m)} = 0_{Scalar (m)}$
6	1 2 3 4 5	isldepslvec2	$⊢ (m \in LVec \land s \in 𝒫 {Base}_{m}) \to (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \leftrightarrow s linDepS m)$
7	6	bicomd	$⊢ (m \in LVec \land s \in 𝒫 {Base}_{m}) \to (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v))$
8	7	rgen2	$⊢ \forall m \in LVec \forall s \in 𝒫 {Base}_{m} (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v))$
9		ldepsnlinc	$⊢ \exists m \in LMod \exists s \in 𝒫 {Base}_{m} (s linDepS m \land \forall v \in s \forall f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \to f linC (m) (s ∖ \{v\}) \neq v))$
10		df-ne	$⊢ f linC (m) (s ∖ \{v\}) \neq v \leftrightarrow \neg f linC (m) (s ∖ \{v\}) = v$
11	10	imbi2i	$⊢ ({finSupp}_{0_{Scalar (m)}} (f) \to f linC (m) (s ∖ \{v\}) \neq v) \leftrightarrow ({finSupp}_{0_{Scalar (m)}} (f) \to \neg f linC (m) (s ∖ \{v\}) = v)$
12		imnan	$⊢ ({finSupp}_{0_{Scalar (m)}} (f) \to \neg f linC (m) (s ∖ \{v\}) = v) \leftrightarrow \neg ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)$
13	11 12	bitri	$⊢ ({finSupp}_{0_{Scalar (m)}} (f) \to f linC (m) (s ∖ \{v\}) \neq v) \leftrightarrow \neg ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)$
14	13	ralbii	$⊢ \forall f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \to f linC (m) (s ∖ \{v\}) \neq v) \leftrightarrow \forall f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) \neg ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)$
15		ralnex	$⊢ \forall f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) \neg ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \leftrightarrow \neg \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)$
16	14 15	bitri	$⊢ \forall f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \to f linC (m) (s ∖ \{v\}) \neq v) \leftrightarrow \neg \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)$
17	16	ralbii	$⊢ \forall v \in s \forall f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \to f linC (m) (s ∖ \{v\}) \neq v) \leftrightarrow \forall v \in s \neg \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)$
18		ralnex	$⊢ \forall v \in s \neg \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \leftrightarrow \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)$
19	17 18	bitri	$⊢ \forall v \in s \forall f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \to f linC (m) (s ∖ \{v\}) \neq v) \leftrightarrow \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)$
20	19	anbi2i	$⊢ (s linDepS m \land \forall v \in s \forall f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \to f linC (m) (s ∖ \{v\}) \neq v)) \leftrightarrow (s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v))$
21	20	2rexbii	$⊢ \exists m \in LMod \exists s \in 𝒫 {Base}_{m} (s linDepS m \land \forall v \in s \forall f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \to f linC (m) (s ∖ \{v\}) \neq v)) \leftrightarrow \exists m \in LMod \exists s \in 𝒫 {Base}_{m} (s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v))$
22	9 21	mpbi	$⊢ \exists m \in LMod \exists s \in 𝒫 {Base}_{m} (s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v))$
23	22	orci	$⊢ (\exists m \in LMod \exists s \in 𝒫 {Base}_{m} (s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \lor \exists m \in LMod \exists s \in 𝒫 {Base}_{m} (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \land \neg s linDepS m))$
24		r19.43	$⊢ \exists m \in LMod (\exists s \in 𝒫 {Base}_{m} (s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \lor \exists s \in 𝒫 {Base}_{m} (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \land \neg s linDepS m)) \leftrightarrow (\exists m \in LMod \exists s \in 𝒫 {Base}_{m} (s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \lor \exists m \in LMod \exists s \in 𝒫 {Base}_{m} (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \land \neg s linDepS m))$
25	23 24	mpbir	$⊢ \exists m \in LMod (\exists s \in 𝒫 {Base}_{m} (s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \lor \exists s \in 𝒫 {Base}_{m} (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \land \neg s linDepS m))$
26		r19.43	$⊢ \exists s \in 𝒫 {Base}_{m} ((s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \lor (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \land \neg s linDepS m)) \leftrightarrow (\exists s \in 𝒫 {Base}_{m} (s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \lor \exists s \in 𝒫 {Base}_{m} (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \land \neg s linDepS m))$
27	26	rexbii	$⊢ \exists m \in LMod \exists s \in 𝒫 {Base}_{m} ((s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \lor (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \land \neg s linDepS m)) \leftrightarrow \exists m \in LMod (\exists s \in 𝒫 {Base}_{m} (s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \lor \exists s \in 𝒫 {Base}_{m} (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \land \neg s linDepS m))$
28	25 27	mpbir	$⊢ \exists m \in LMod \exists s \in 𝒫 {Base}_{m} ((s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \lor (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \land \neg s linDepS m))$
29		xor	$⊢ \neg (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \leftrightarrow ((s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \lor (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \land \neg s linDepS m))$
30	29	bicomi	$⊢ ((s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \lor (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \land \neg s linDepS m)) \leftrightarrow \neg (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v))$
31	30	rexbii	$⊢ \exists s \in 𝒫 {Base}_{m} ((s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \lor (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \land \neg s linDepS m)) \leftrightarrow \exists s \in 𝒫 {Base}_{m} \neg (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v))$
32		rexnal	$⊢ \exists s \in 𝒫 {Base}_{m} \neg (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \leftrightarrow \neg \forall s \in 𝒫 {Base}_{m} (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v))$
33	31 32	bitri	$⊢ \exists s \in 𝒫 {Base}_{m} ((s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \lor (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \land \neg s linDepS m)) \leftrightarrow \neg \forall s \in 𝒫 {Base}_{m} (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v))$
34	33	rexbii	$⊢ \exists m \in LMod \exists s \in 𝒫 {Base}_{m} ((s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \lor (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \land \neg s linDepS m)) \leftrightarrow \exists m \in LMod \neg \forall s \in 𝒫 {Base}_{m} (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v))$
35		rexnal	$⊢ \exists m \in LMod \neg \forall s \in 𝒫 {Base}_{m} (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \leftrightarrow \neg \forall m \in LMod \forall s \in 𝒫 {Base}_{m} (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v))$
36	34 35	bitri	$⊢ \exists m \in LMod \exists s \in 𝒫 {Base}_{m} ((s linDepS m \land \neg \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \lor (\exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v) \land \neg s linDepS m)) \leftrightarrow \neg \forall m \in LMod \forall s \in 𝒫 {Base}_{m} (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v))$
37	28 36	mpbi	$⊢ \neg \forall m \in LMod \forall s \in 𝒫 {Base}_{m} (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v))$
38	8 37	pm3.2i	$⊢ (\forall m \in LVec \forall s \in 𝒫 {Base}_{m} (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)) \land \neg \forall m \in LMod \forall s \in 𝒫 {Base}_{m} (s linDepS m \leftrightarrow \exists v \in s \exists f \in ({Base}_{Scalar (m)}^{(s ∖ \{v\})}) ({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) (s ∖ \{v\}) = v)))$

Metamath Proof Explorer

Theorem ldepslinc

Proof