Metamath Proof Explorer

Theorem 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∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→SlinDepSM

Proof

Step Hyp Ref Expression
1 eqid ⊢BaseM=BaseM
2 eqid ⊢Scalar⁡M=Scalar⁡M
3 eqid ⊢0Scalar⁡M=0Scalar⁡M
4 eqid ⊢1Scalar⁡M=1Scalar⁡M
5 eqeq1 ⊢s=y→s=0M↔y=0M
6 5 ifbid ⊢s=y→ifs=0M1Scalar⁡M0Scalar⁡M=ify=0M1Scalar⁡M0Scalar⁡M
7 6 cbvmptv ⊢s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M=y∈S⟼ify=0M1Scalar⁡M0Scalar⁡M
8 1 2 3 4 7 mptcfsupp ⊢M∈LMod∧S∈𝒫BaseM∧0M∈S→finSupp0Scalar⁡M⁡s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M
9 8 3adant1r ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→finSupp0Scalar⁡M⁡s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M
10 simp1l ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→M∈LMod
11 simp2 ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→S∈𝒫BaseM
12 eqid ⊢0M=0M
13 eqid ⊢s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M=s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M
14 1 2 3 4 12 13 linc0scn0 ⊢M∈LMod∧S∈𝒫BaseM→s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡MlinC⁡MS=0M
15 10 11 14 syl2anc ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡MlinC⁡MS=0M
16 simp3 ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→0M∈S
17 fveq2 ⊢x=0M→s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M⁡x=s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M⁡0M
18 17 neeq1d ⊢x=0M→s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M⁡x≠0Scalar⁡M↔s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M⁡0M≠0Scalar⁡M
19 18 adantl ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S∧x=0M→s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M⁡x≠0Scalar⁡M↔s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M⁡0M≠0Scalar⁡M
20 iftrue ⊢s=0M→ifs=0M1Scalar⁡M0Scalar⁡M=1Scalar⁡M
21 fvexd ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→1Scalar⁡M∈V
22 13 20 16 21 fvmptd3 ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M⁡0M=1Scalar⁡M
23 2 lmodring ⊢M∈LMod→Scalar⁡M∈Ring
24 23 anim1i ⊢M∈LMod∧1<BaseScalar⁡M→Scalar⁡M∈Ring∧1<BaseScalar⁡M
25 24 3ad2ant1 ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→Scalar⁡M∈Ring∧1<BaseScalar⁡M
26 eqid ⊢BaseScalar⁡M=BaseScalar⁡M
27 26 4 3 ring1ne0 ⊢Scalar⁡M∈Ring∧1<BaseScalar⁡M→1Scalar⁡M≠0Scalar⁡M
28 25 27 syl ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→1Scalar⁡M≠0Scalar⁡M
29 22 28 eqnetrd ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M⁡0M≠0Scalar⁡M
30 16 19 29 rspcedvd ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→∃x∈Ss∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M⁡x≠0Scalar⁡M
31 2 26 4 lmod1cl ⊢M∈LMod→1Scalar⁡M∈BaseScalar⁡M
32 2 26 3 lmod0cl ⊢M∈LMod→0Scalar⁡M∈BaseScalar⁡M
33 31 32 ifcld ⊢M∈LMod→ifs=0M1Scalar⁡M0Scalar⁡M∈BaseScalar⁡M
34 33 adantr ⊢M∈LMod∧1<BaseScalar⁡M→ifs=0M1Scalar⁡M0Scalar⁡M∈BaseScalar⁡M
35 34 3ad2ant1 ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→ifs=0M1Scalar⁡M0Scalar⁡M∈BaseScalar⁡M
36 35 adantr ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S∧s∈S→ifs=0M1Scalar⁡M0Scalar⁡M∈BaseScalar⁡M
37 36 fmpttd ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M:S⟶BaseScalar⁡M
38 fvexd ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→BaseScalar⁡M∈V
39 38 11 elmapd ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M∈BaseScalar⁡MS↔s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M:S⟶BaseScalar⁡M
40 37 39 mpbird ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M∈BaseScalar⁡MS
41 breq1 ⊢f=s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M→finSupp0Scalar⁡M⁡f↔finSupp0Scalar⁡M⁡s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M
42 oveq1 ⊢f=s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M→flinC⁡MS=s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡MlinC⁡MS
43 42 eqeq1d ⊢f=s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M→flinC⁡MS=0M↔s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡MlinC⁡MS=0M
44 fveq1 ⊢f=s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M→f⁡x=s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M⁡x
45 44 neeq1d ⊢f=s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M→f⁡x≠0Scalar⁡M↔s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M⁡x≠0Scalar⁡M
46 45 rexbidv ⊢f=s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M→∃x∈Sf⁡x≠0Scalar⁡M↔∃x∈Ss∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M⁡x≠0Scalar⁡M
47 41 43 46 3anbi123d ⊢f=s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M→finSupp0Scalar⁡M⁡f∧flinC⁡MS=0M∧∃x∈Sf⁡x≠0Scalar⁡M↔finSupp0Scalar⁡M⁡s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M∧s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡MlinC⁡MS=0M∧∃x∈Ss∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M⁡x≠0Scalar⁡M
48 47 adantl ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S∧f=s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M→finSupp0Scalar⁡M⁡f∧flinC⁡MS=0M∧∃x∈Sf⁡x≠0Scalar⁡M↔finSupp0Scalar⁡M⁡s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M∧s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡MlinC⁡MS=0M∧∃x∈Ss∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M⁡x≠0Scalar⁡M
49 40 48 rspcedv ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→finSupp0Scalar⁡M⁡s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M∧s∈S⟼ifs=0M1Scalar⁡M0Scalar⁡MlinC⁡MS=0M∧∃x∈Ss∈S⟼ifs=0M1Scalar⁡M0Scalar⁡M⁡x≠0Scalar⁡M→∃f∈BaseScalar⁡MSfinSupp0Scalar⁡M⁡f∧flinC⁡MS=0M∧∃x∈Sf⁡x≠0Scalar⁡M
50 9 15 30 49 mp3and ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→∃f∈BaseScalar⁡MSfinSupp0Scalar⁡M⁡f∧flinC⁡MS=0M∧∃x∈Sf⁡x≠0Scalar⁡M
51 1 12 2 26 3 islindeps ⊢M∈LMod∧S∈𝒫BaseM→SlinDepSM↔∃f∈BaseScalar⁡MSfinSupp0Scalar⁡M⁡f∧flinC⁡MS=0M∧∃x∈Sf⁡x≠0Scalar⁡M
52 10 11 51 syl2anc ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→SlinDepSM↔∃f∈BaseScalar⁡MSfinSupp0Scalar⁡M⁡f∧flinC⁡MS=0M∧∃x∈Sf⁡x≠0Scalar⁡M
53 50 52 mpbird ⊢M∈LMod∧1<BaseScalar⁡M∧S∈𝒫BaseM∧0M∈S→SlinDepSM