el0ldep

Description: A set containing the zero element of a module is always linearly dependent, if the underlying ring has at least two elements. (Contributed by AV, 13-Apr-2019) (Revised by AV, 27-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

		Ref	Expression
	Assertion	el0ldep	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to S linDepS M$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{M} = {Base}_{M}$
2		eqid	$⊢ Scalar (M) = Scalar (M)$
3		eqid	$⊢ 0_{Scalar (M)} = 0_{Scalar (M)}$
4		eqid	$⊢ 1_{Scalar (M)} = 1_{Scalar (M)}$
5		eqeq1	$⊢ s = y \to (s = 0_{M} \leftrightarrow y = 0_{M})$
6	5	ifbid	$⊢ s = y \to if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)}) = if (y = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})$
7	6	cbvmptv	$⊢ (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) = (y \in S ⟼ if (y = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)}))$
8	1 2 3 4 7	mptcfsupp	$⊢ (M \in LMod \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to {finSupp}_{0_{Scalar (M)}} ((s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})))$
9	8	3adant1r	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to {finSupp}_{0_{Scalar (M)}} ((s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})))$
10		simp1l	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to M \in LMod$
11		simp2	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to S \in 𝒫 {Base}_{M}$
12		eqid	$⊢ 0_{M} = 0_{M}$
13		eqid	$⊢ (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) = (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)}))$
14	1 2 3 4 12 13	linc0scn0	$⊢ (M \in LMod \land S \in 𝒫 {Base}_{M}) \to (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) linC (M) S = 0_{M}$
15	10 11 14	syl2anc	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) linC (M) S = 0_{M}$
16		simp3	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to 0_{M} \in S$
17		fveq2	$⊢ x = 0_{M} \to (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) (x) = (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) (0_{M})$
18	17	neeq1d	$⊢ x = 0_{M} \to ((s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) (x) \neq 0_{Scalar (M)} \leftrightarrow (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) (0_{M}) \neq 0_{Scalar (M)})$
19	18	adantl	$⊢ (((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \land x = 0_{M}) \to ((s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) (x) \neq 0_{Scalar (M)} \leftrightarrow (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) (0_{M}) \neq 0_{Scalar (M)})$
20		iftrue	$⊢ s = 0_{M} \to if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)}) = 1_{Scalar (M)}$
21		fvexd	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to 1_{Scalar (M)} \in V$
22	13 20 16 21	fvmptd3	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) (0_{M}) = 1_{Scalar (M)}$
23	2	lmodring	$⊢ M \in LMod \to Scalar (M) \in Ring$
24	23	anim1i	$⊢ (M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \to (Scalar (M) \in Ring \land 1 < \|{Base}_{Scalar (M)}\|)$
25	24	3ad2ant1	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to (Scalar (M) \in Ring \land 1 < \|{Base}_{Scalar (M)}\|)$
26		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
27	26 4 3	ring1ne0	$⊢ (Scalar (M) \in Ring \land 1 < \|{Base}_{Scalar (M)}\|) \to 1_{Scalar (M)} \neq 0_{Scalar (M)}$
28	25 27	syl	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to 1_{Scalar (M)} \neq 0_{Scalar (M)}$
29	22 28	eqnetrd	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) (0_{M}) \neq 0_{Scalar (M)}$
30	16 19 29	rspcedvd	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to \exists x \in S (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) (x) \neq 0_{Scalar (M)}$
31	2 26 4	lmod1cl	$⊢ M \in LMod \to 1_{Scalar (M)} \in {Base}_{Scalar (M)}$
32	2 26 3	lmod0cl	$⊢ M \in LMod \to 0_{Scalar (M)} \in {Base}_{Scalar (M)}$
33	31 32	ifcld	$⊢ M \in LMod \to if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)}) \in {Base}_{Scalar (M)}$
34	33	adantr	$⊢ (M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \to if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)}) \in {Base}_{Scalar (M)}$
35	34	3ad2ant1	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)}) \in {Base}_{Scalar (M)}$
36	35	adantr	$⊢ (((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \land s \in S) \to if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)}) \in {Base}_{Scalar (M)}$
37	36	fmpttd	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) : S ⟶ {Base}_{Scalar (M)}$
38		fvexd	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to {Base}_{Scalar (M)} \in V$
39	38 11	elmapd	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to ((s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) \in ({Base}_{Scalar (M)}^{S}) \leftrightarrow (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) : S ⟶ {Base}_{Scalar (M)})$
40	37 39	mpbird	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) \in ({Base}_{Scalar (M)}^{S})$
41		breq1	$⊢ f = (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) \to ({finSupp}_{0_{Scalar (M)}} (f) \leftrightarrow {finSupp}_{0_{Scalar (M)}} ((s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)}))))$
42		oveq1	$⊢ f = (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) \to f linC (M) S = (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) linC (M) S$
43	42	eqeq1d	$⊢ f = (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) \to (f linC (M) S = 0_{M} \leftrightarrow (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) linC (M) S = 0_{M})$
44		fveq1	$⊢ f = (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) \to f (x) = (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) (x)$
45	44	neeq1d	$⊢ f = (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) \to (f (x) \neq 0_{Scalar (M)} \leftrightarrow (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) (x) \neq 0_{Scalar (M)})$
46	45	rexbidv	$⊢ f = (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) \to (\exists x \in S f (x) \neq 0_{Scalar (M)} \leftrightarrow \exists x \in S (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) (x) \neq 0_{Scalar (M)})$
47	41 43 46	3anbi123d	$⊢ f = (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) \to (({finSupp}_{0_{Scalar (M)}} (f) \land f linC (M) S = 0_{M} \land \exists x \in S f (x) \neq 0_{Scalar (M)}) \leftrightarrow ({finSupp}_{0_{Scalar (M)}} ((s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)}))) \land (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) linC (M) S = 0_{M} \land \exists x \in S (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) (x) \neq 0_{Scalar (M)}))$
48	47	adantl	$⊢ (((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \land f = (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)}))) \to (({finSupp}_{0_{Scalar (M)}} (f) \land f linC (M) S = 0_{M} \land \exists x \in S f (x) \neq 0_{Scalar (M)}) \leftrightarrow ({finSupp}_{0_{Scalar (M)}} ((s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)}))) \land (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) linC (M) S = 0_{M} \land \exists x \in S (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) (x) \neq 0_{Scalar (M)}))$
49	40 48	rspcedv	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to (({finSupp}_{0_{Scalar (M)}} ((s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)}))) \land (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) linC (M) S = 0_{M} \land \exists x \in S (s \in S ⟼ if (s = 0_{M}, 1_{Scalar (M)}, 0_{Scalar (M)})) (x) \neq 0_{Scalar (M)}) \to \exists f \in ({Base}_{Scalar (M)}^{S}) ({finSupp}_{0_{Scalar (M)}} (f) \land f linC (M) S = 0_{M} \land \exists x \in S f (x) \neq 0_{Scalar (M)}))$
50	9 15 30 49	mp3and	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to \exists f \in ({Base}_{Scalar (M)}^{S}) ({finSupp}_{0_{Scalar (M)}} (f) \land f linC (M) S = 0_{M} \land \exists x \in S f (x) \neq 0_{Scalar (M)})$
51	1 12 2 26 3	islindeps	$⊢ (M \in LMod \land S \in 𝒫 {Base}_{M}) \to (S linDepS M \leftrightarrow \exists f \in ({Base}_{Scalar (M)}^{S}) ({finSupp}_{0_{Scalar (M)}} (f) \land f linC (M) S = 0_{M} \land \exists x \in S f (x) \neq 0_{Scalar (M)}))$
52	10 11 51	syl2anc	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to (S linDepS M \leftrightarrow \exists f \in ({Base}_{Scalar (M)}^{S}) ({finSupp}_{0_{Scalar (M)}} (f) \land f linC (M) S = 0_{M} \land \exists x \in S f (x) \neq 0_{Scalar (M)}))$
53	50 52	mpbird	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to S linDepS M$

Metamath Proof Explorer

Theorem el0ldep

Proof