Metamath Proof Explorer


Theorem isldepslvec2

Description: Alternative definition of being a linearly dependent subset of a (left) vector space. In this case, the reverse implication of islindeps2 holds, so that both definitions are equivalent (see theorem 1.6 in Roman p. 46 and the note in Roman p. 112: if a nontrivial linear combination of elements (where not all of the coefficients are 0) in an R-vector space is 0, then and only then each of the elements is a linear combination of the others. (Contributed by AV, 30-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Hypotheses islindeps2.b B=BaseM
islindeps2.z Z=0M
islindeps2.r R=ScalarM
islindeps2.e E=BaseR
islindeps2.0 0˙=0R
Assertion isldepslvec2 MLVecS𝒫BsSfESsfinSupp0˙fflinCMSs=sSlinDepSM

Proof

Step Hyp Ref Expression
1 islindeps2.b B=BaseM
2 islindeps2.z Z=0M
3 islindeps2.r R=ScalarM
4 islindeps2.e E=BaseR
5 islindeps2.0 0˙=0R
6 lveclmod MLVecMLMod
7 6 adantr MLVecS𝒫BMLMod
8 simpr MLVecS𝒫BS𝒫B
9 3 lvecdrng MLVecRDivRing
10 drngnzr RDivRingRNzRing
11 9 10 syl MLVecRNzRing
12 11 adantr MLVecS𝒫BRNzRing
13 1 2 3 4 5 islindeps2 MLModS𝒫BRNzRingsSfESsfinSupp0˙fflinCMSs=sSlinDepSM
14 7 8 12 13 syl3anc MLVecS𝒫BsSfESsfinSupp0˙fflinCMSs=sSlinDepSM
15 1 2 3 4 5 islindeps MLVecS𝒫BSlinDepSMgESfinSupp0˙gglinCMS=ZsSgs0˙
16 df-3an finSupp0˙gglinCMS=ZsSgs0˙finSupp0˙gglinCMS=ZsSgs0˙
17 r19.42v sSfinSupp0˙gglinCMS=Zgs0˙finSupp0˙gglinCMS=ZsSgs0˙
18 16 17 bitr4i finSupp0˙gglinCMS=ZsSgs0˙sSfinSupp0˙gglinCMS=Zgs0˙
19 18 rexbii gESfinSupp0˙gglinCMS=ZsSgs0˙gESsSfinSupp0˙gglinCMS=Zgs0˙
20 rexcom gESsSfinSupp0˙gglinCMS=Zgs0˙sSgESfinSupp0˙gglinCMS=Zgs0˙
21 19 20 bitri gESfinSupp0˙gglinCMS=ZsSgs0˙sSgESfinSupp0˙gglinCMS=Zgs0˙
22 simplr MLVecS𝒫BsSS𝒫B
23 6 ad2antrr MLVecS𝒫BsSMLMod
24 simpr MLVecS𝒫BsSsS
25 22 23 24 3jca MLVecS𝒫BsSS𝒫BMLModsS
26 25 ad2antrr MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙S𝒫BMLModsS
27 simplr MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙gES
28 elmapi gESg:SE
29 ffvelcdm g:SEsSgsE
30 28 24 29 syl2anr MLVecS𝒫BsSgESgsE
31 simpr finSupp0˙gglinCMS=Zgs0˙gs0˙
32 30 31 anim12i MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙gsEgs0˙
33 9 ad2antrr MLVecS𝒫BsSRDivRing
34 33 ad2antrr MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙RDivRing
35 eqid UnitR=UnitR
36 4 35 5 drngunit RDivRinggsUnitRgsEgs0˙
37 34 36 syl MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙gsUnitRgsEgs0˙
38 32 37 mpbird MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙gsUnitR
39 simpll finSupp0˙gglinCMS=Zgs0˙finSupp0˙g
40 39 adantl MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙finSupp0˙g
41 eqid invgR=invgR
42 eqid invrR=invrR
43 eqid R=R
44 eqid zSsinvrRinvgRgsRgz=zSsinvrRinvgRgsRgz
45 1 3 4 35 5 2 41 42 43 44 lincresunit2 S𝒫BMLModsSgESgsUnitRfinSupp0˙gfinSupp0˙zSsinvrRinvgRgsRgz
46 26 27 38 40 45 syl13anc MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙finSupp0˙zSsinvrRinvgRgsRgz
47 simpll MLVecS𝒫BsSMLVec
48 22 47 24 3jca MLVecS𝒫BsSS𝒫BMLVecsS
49 48 ad2antrr MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙S𝒫BMLVecsS
50 simprr MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙gs0˙
51 simplr finSupp0˙gglinCMS=Zgs0˙glinCMS=Z
52 51 adantl MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙glinCMS=Z
53 fveq2 z=ygz=gy
54 53 oveq2d z=yinvrRinvgRgsRgz=invrRinvgRgsRgy
55 54 cbvmptv zSsinvrRinvgRgsRgz=ySsinvrRinvgRgsRgy
56 1 3 4 35 5 2 41 42 43 55 lincreslvec3 S𝒫BMLVecsSgESgs0˙finSupp0˙gglinCMS=ZzSsinvrRinvgRgsRgzlinCMSs=s
57 49 27 50 40 52 56 syl131anc MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙zSsinvrRinvgRgsRgzlinCMSs=s
58 1 3 4 35 5 2 41 42 43 44 lincresunit1 S𝒫BMLModsSgESgsUnitRzSsinvrRinvgRgsRgzESs
59 26 27 38 58 syl12anc MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙zSsinvrRinvgRgsRgzESs
60 breq1 f=zSsinvrRinvgRgsRgzfinSupp0˙ffinSupp0˙zSsinvrRinvgRgsRgz
61 oveq1 f=zSsinvrRinvgRgsRgzflinCMSs=zSsinvrRinvgRgsRgzlinCMSs
62 61 eqeq1d f=zSsinvrRinvgRgsRgzflinCMSs=szSsinvrRinvgRgsRgzlinCMSs=s
63 60 62 anbi12d f=zSsinvrRinvgRgsRgzfinSupp0˙fflinCMSs=sfinSupp0˙zSsinvrRinvgRgsRgzzSsinvrRinvgRgsRgzlinCMSs=s
64 63 adantl MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙f=zSsinvrRinvgRgsRgzfinSupp0˙fflinCMSs=sfinSupp0˙zSsinvrRinvgRgsRgzzSsinvrRinvgRgsRgzlinCMSs=s
65 59 64 rspcedv MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙finSupp0˙zSsinvrRinvgRgsRgzzSsinvrRinvgRgsRgzlinCMSs=sfESsfinSupp0˙fflinCMSs=s
66 46 57 65 mp2and MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙fESsfinSupp0˙fflinCMSs=s
67 66 rexlimdva2 MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙fESsfinSupp0˙fflinCMSs=s
68 67 reximdva MLVecS𝒫BsSgESfinSupp0˙gglinCMS=Zgs0˙sSfESsfinSupp0˙fflinCMSs=s
69 21 68 biimtrid MLVecS𝒫BgESfinSupp0˙gglinCMS=ZsSgs0˙sSfESsfinSupp0˙fflinCMSs=s
70 15 69 sylbid MLVecS𝒫BSlinDepSMsSfESsfinSupp0˙fflinCMSs=s
71 14 70 impbid MLVecS𝒫BsSfESsfinSupp0˙fflinCMSs=sSlinDepSM