Metamath Proof Explorer


Theorem ldepsnlinc

Description: The reverse implication of islindeps2 does not hold for arbitrary (left) modules, see note in Roman p. 112: "... if a nontrivial linear combination of the elements ... in an R-module M is 0, ... where not all of the coefficients are 0, then we cannot conclude ... that one of the elements ... is a linear combination of the others." This means that there is at least one left module having a linearly dependent subset in which there is at least one element which is not a linear combinantion of the other elements of this subset. Such a left module can be constructed by using zlmodzxzequa and zlmodzxznm . (Contributed by AV, 25-May-2019) (Revised by AV, 30-Jul-2019)

Ref Expression
Assertion ldepsnlinc mLMods𝒫BasemslinDepSmvsfBaseScalarmsvfinSupp0ScalarmfflinCmsvv

Proof

Step Hyp Ref Expression
1 eqid ringfreeLMod01=ringfreeLMod01
2 1 zlmodzxzlmod ringfreeLMod01LModring=ScalarringfreeLMod01
3 2 simpli ringfreeLMod01LMod
4 3z 3
5 6nn 6
6 5 nnzi 6
7 1 zlmodzxzel 360316BaseringfreeLMod01
8 4 6 7 mp2an 0316BaseringfreeLMod01
9 2z 2
10 4z 4
11 1 zlmodzxzel 240214BaseringfreeLMod01
12 9 10 11 mp2an 0214BaseringfreeLMod01
13 prelpwi 0316BaseringfreeLMod010214BaseringfreeLMod0103160214𝒫BaseringfreeLMod01
14 8 12 13 mp2an 03160214𝒫BaseringfreeLMod01
15 eqid 0316=0316
16 eqid 0214=0214
17 1 15 16 zlmodzxzldep 03160214linDepSringfreeLMod01
18 1 15 16 ldepsnlinclem1 fBasering0214flinCringfreeLMod0102140316
19 simpr ringfreeLMod01LModring=ScalarringfreeLMod01ring=ScalarringfreeLMod01
20 19 eqcomd ringfreeLMod01LModring=ScalarringfreeLMod01ScalarringfreeLMod01=ring
21 2 20 ax-mp ScalarringfreeLMod01=ring
22 21 fveq2i BaseScalarringfreeLMod01=Basering
23 22 oveq1i BaseScalarringfreeLMod010214=Basering0214
24 18 23 eleq2s fBaseScalarringfreeLMod010214flinCringfreeLMod0102140316
25 24 a1d fBaseScalarringfreeLMod010214finSupp0ScalarringfreeLMod01fflinCringfreeLMod0102140316
26 25 rgen fBaseScalarringfreeLMod010214finSupp0ScalarringfreeLMod01fflinCringfreeLMod0102140316
27 1 15 16 ldepsnlinclem2 fBasering0316flinCringfreeLMod0103160214
28 22 oveq1i BaseScalarringfreeLMod010316=Basering0316
29 27 28 eleq2s fBaseScalarringfreeLMod010316flinCringfreeLMod0103160214
30 29 a1d fBaseScalarringfreeLMod010316finSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214
31 30 rgen fBaseScalarringfreeLMod010316finSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214
32 prex 0316V
33 prex 0214V
34 sneq v=0316v=0316
35 34 difeq2d v=031603160214v=031602140316
36 1 15 16 zlmodzxzldeplem 03160214
37 difprsn1 03160214031602140316=0214
38 36 37 ax-mp 031602140316=0214
39 35 38 eqtrdi v=031603160214v=0214
40 39 oveq2d v=0316BaseScalarringfreeLMod0103160214v=BaseScalarringfreeLMod010214
41 39 oveq2d v=0316flinCringfreeLMod0103160214v=flinCringfreeLMod010214
42 id v=0316v=0316
43 41 42 neeq12d v=0316flinCringfreeLMod0103160214vvflinCringfreeLMod0102140316
44 43 imbi2d v=0316finSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214vvfinSupp0ScalarringfreeLMod01fflinCringfreeLMod0102140316
45 40 44 raleqbidv v=0316fBaseScalarringfreeLMod0103160214vfinSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214vvfBaseScalarringfreeLMod010214finSupp0ScalarringfreeLMod01fflinCringfreeLMod0102140316
46 sneq v=0214v=0214
47 46 difeq2d v=021403160214v=031602140214
48 difprsn2 03160214031602140214=0316
49 36 48 ax-mp 031602140214=0316
50 47 49 eqtrdi v=021403160214v=0316
51 50 oveq2d v=0214BaseScalarringfreeLMod0103160214v=BaseScalarringfreeLMod010316
52 50 oveq2d v=0214flinCringfreeLMod0103160214v=flinCringfreeLMod010316
53 id v=0214v=0214
54 52 53 neeq12d v=0214flinCringfreeLMod0103160214vvflinCringfreeLMod0103160214
55 54 imbi2d v=0214finSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214vvfinSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214
56 51 55 raleqbidv v=0214fBaseScalarringfreeLMod0103160214vfinSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214vvfBaseScalarringfreeLMod010316finSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214
57 32 33 45 56 ralpr v03160214fBaseScalarringfreeLMod0103160214vfinSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214vvfBaseScalarringfreeLMod010214finSupp0ScalarringfreeLMod01fflinCringfreeLMod0102140316fBaseScalarringfreeLMod010316finSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214
58 26 31 57 mpbir2an v03160214fBaseScalarringfreeLMod0103160214vfinSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214vv
59 17 58 pm3.2i 03160214linDepSringfreeLMod01v03160214fBaseScalarringfreeLMod0103160214vfinSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214vv
60 breq1 s=03160214slinDepSringfreeLMod0103160214linDepSringfreeLMod01
61 id s=03160214s=03160214
62 difeq1 s=03160214sv=03160214v
63 62 oveq2d s=03160214BaseScalarringfreeLMod01sv=BaseScalarringfreeLMod0103160214v
64 62 oveq2d s=03160214flinCringfreeLMod01sv=flinCringfreeLMod0103160214v
65 64 neeq1d s=03160214flinCringfreeLMod01svvflinCringfreeLMod0103160214vv
66 65 imbi2d s=03160214finSupp0ScalarringfreeLMod01fflinCringfreeLMod01svvfinSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214vv
67 63 66 raleqbidv s=03160214fBaseScalarringfreeLMod01svfinSupp0ScalarringfreeLMod01fflinCringfreeLMod01svvfBaseScalarringfreeLMod0103160214vfinSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214vv
68 61 67 raleqbidv s=03160214vsfBaseScalarringfreeLMod01svfinSupp0ScalarringfreeLMod01fflinCringfreeLMod01svvv03160214fBaseScalarringfreeLMod0103160214vfinSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214vv
69 60 68 anbi12d s=03160214slinDepSringfreeLMod01vsfBaseScalarringfreeLMod01svfinSupp0ScalarringfreeLMod01fflinCringfreeLMod01svv03160214linDepSringfreeLMod01v03160214fBaseScalarringfreeLMod0103160214vfinSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214vv
70 69 rspcev 03160214𝒫BaseringfreeLMod0103160214linDepSringfreeLMod01v03160214fBaseScalarringfreeLMod0103160214vfinSupp0ScalarringfreeLMod01fflinCringfreeLMod0103160214vvs𝒫BaseringfreeLMod01slinDepSringfreeLMod01vsfBaseScalarringfreeLMod01svfinSupp0ScalarringfreeLMod01fflinCringfreeLMod01svv
71 14 59 70 mp2an s𝒫BaseringfreeLMod01slinDepSringfreeLMod01vsfBaseScalarringfreeLMod01svfinSupp0ScalarringfreeLMod01fflinCringfreeLMod01svv
72 fveq2 m=ringfreeLMod01Basem=BaseringfreeLMod01
73 72 pweqd m=ringfreeLMod01𝒫Basem=𝒫BaseringfreeLMod01
74 breq2 m=ringfreeLMod01slinDepSmslinDepSringfreeLMod01
75 2fveq3 m=ringfreeLMod01BaseScalarm=BaseScalarringfreeLMod01
76 75 oveq1d m=ringfreeLMod01BaseScalarmsv=BaseScalarringfreeLMod01sv
77 2fveq3 m=ringfreeLMod010Scalarm=0ScalarringfreeLMod01
78 77 breq2d m=ringfreeLMod01finSupp0ScalarmffinSupp0ScalarringfreeLMod01f
79 fveq2 m=ringfreeLMod01linCm=linCringfreeLMod01
80 79 oveqd m=ringfreeLMod01flinCmsv=flinCringfreeLMod01sv
81 80 neeq1d m=ringfreeLMod01flinCmsvvflinCringfreeLMod01svv
82 78 81 imbi12d m=ringfreeLMod01finSupp0ScalarmfflinCmsvvfinSupp0ScalarringfreeLMod01fflinCringfreeLMod01svv
83 76 82 raleqbidv m=ringfreeLMod01fBaseScalarmsvfinSupp0ScalarmfflinCmsvvfBaseScalarringfreeLMod01svfinSupp0ScalarringfreeLMod01fflinCringfreeLMod01svv
84 83 ralbidv m=ringfreeLMod01vsfBaseScalarmsvfinSupp0ScalarmfflinCmsvvvsfBaseScalarringfreeLMod01svfinSupp0ScalarringfreeLMod01fflinCringfreeLMod01svv
85 74 84 anbi12d m=ringfreeLMod01slinDepSmvsfBaseScalarmsvfinSupp0ScalarmfflinCmsvvslinDepSringfreeLMod01vsfBaseScalarringfreeLMod01svfinSupp0ScalarringfreeLMod01fflinCringfreeLMod01svv
86 73 85 rexeqbidv m=ringfreeLMod01s𝒫BasemslinDepSmvsfBaseScalarmsvfinSupp0ScalarmfflinCmsvvs𝒫BaseringfreeLMod01slinDepSringfreeLMod01vsfBaseScalarringfreeLMod01svfinSupp0ScalarringfreeLMod01fflinCringfreeLMod01svv
87 86 rspcev ringfreeLMod01LMods𝒫BaseringfreeLMod01slinDepSringfreeLMod01vsfBaseScalarringfreeLMod01svfinSupp0ScalarringfreeLMod01fflinCringfreeLMod01svvmLMods𝒫BasemslinDepSmvsfBaseScalarmsvfinSupp0ScalarmfflinCmsvv
88 3 71 87 mp2an mLMods𝒫BasemslinDepSmvsfBaseScalarmsvfinSupp0ScalarmfflinCmsvv