Metamath Proof Explorer


Theorem lindslinindsimp2

Description: Implication 2 for lindslininds . (Contributed by AV, 26-Apr-2019) (Revised by AV, 30-Jul-2019)

Ref Expression
Hypotheses lindslinind.r R=ScalarM
lindslinind.b B=BaseR
lindslinind.0 0˙=0R
lindslinind.z Z=0M
Assertion lindslinindsimp2 SVMLModSBaseMsSyB0˙¬yMsLSpanMSsS𝒫BaseMfBSfinSupp0˙fflinCMS=ZxSfx=0˙

Proof

Step Hyp Ref Expression
1 lindslinind.r R=ScalarM
2 lindslinind.b B=BaseR
3 lindslinind.0 0˙=0R
4 lindslinind.z Z=0M
5 simprl SVMLModSBaseMsSyB0˙¬yMsLSpanMSsSBaseM
6 elpwg SVS𝒫BaseMSBaseM
7 6 ad2antrr SVMLModSBaseMsSyB0˙¬yMsLSpanMSsS𝒫BaseMSBaseM
8 5 7 mpbird SVMLModSBaseMsSyB0˙¬yMsLSpanMSsS𝒫BaseM
9 simplr SVMLModSBaseMMLMod
10 ssdifss SBaseMSsBaseM
11 10 adantl SVMLModSBaseMSsBaseM
12 difexg SVSsV
13 12 ad2antrr SVMLModSBaseMSsV
14 elpwg SsVSs𝒫BaseMSsBaseM
15 13 14 syl SVMLModSBaseMSs𝒫BaseMSsBaseM
16 11 15 mpbird SVMLModSBaseMSs𝒫BaseM
17 eqid BaseM=BaseM
18 17 lspeqlco MLModSs𝒫BaseMMLinCoSs=LSpanMSs
19 18 eleq2d MLModSs𝒫BaseMyMsMLinCoSsyMsLSpanMSs
20 19 bicomd MLModSs𝒫BaseMyMsLSpanMSsyMsMLinCoSs
21 9 16 20 syl2anc SVMLModSBaseMyMsLSpanMSsyMsMLinCoSs
22 21 notbid SVMLModSBaseM¬yMsLSpanMSs¬yMsMLinCoSs
23 17 1 2 lcoval MLModSs𝒫BaseMyMsMLinCoSsyMsBaseMgBSsfinSupp0RgyMs=glinCMSs
24 3 eqcomi 0R=0˙
25 24 breq2i finSupp0RgfinSupp0˙g
26 25 anbi1i finSupp0RgyMs=glinCMSsfinSupp0˙gyMs=glinCMSs
27 26 rexbii gBSsfinSupp0RgyMs=glinCMSsgBSsfinSupp0˙gyMs=glinCMSs
28 27 anbi2i yMsBaseMgBSsfinSupp0RgyMs=glinCMSsyMsBaseMgBSsfinSupp0˙gyMs=glinCMSs
29 23 28 bitrdi MLModSs𝒫BaseMyMsMLinCoSsyMsBaseMgBSsfinSupp0˙gyMs=glinCMSs
30 9 16 29 syl2anc SVMLModSBaseMyMsMLinCoSsyMsBaseMgBSsfinSupp0˙gyMs=glinCMSs
31 30 notbid SVMLModSBaseM¬yMsMLinCoSs¬yMsBaseMgBSsfinSupp0˙gyMs=glinCMSs
32 ianor ¬yMsBaseMgBSsfinSupp0˙gyMs=glinCMSs¬yMsBaseM¬gBSsfinSupp0˙gyMs=glinCMSs
33 ralnex gBSs¬finSupp0˙gyMs=glinCMSs¬gBSsfinSupp0˙gyMs=glinCMSs
34 ianor ¬finSupp0˙gyMs=glinCMSs¬finSupp0˙g¬yMs=glinCMSs
35 34 ralbii gBSs¬finSupp0˙gyMs=glinCMSsgBSs¬finSupp0˙g¬yMs=glinCMSs
36 33 35 bitr3i ¬gBSsfinSupp0˙gyMs=glinCMSsgBSs¬finSupp0˙g¬yMs=glinCMSs
37 36 orbi2i ¬yMsBaseM¬gBSsfinSupp0˙gyMs=glinCMSs¬yMsBaseMgBSs¬finSupp0˙g¬yMs=glinCMSs
38 32 37 bitri ¬yMsBaseMgBSsfinSupp0˙gyMs=glinCMSs¬yMsBaseMgBSs¬finSupp0˙g¬yMs=glinCMSs
39 31 38 bitrdi SVMLModSBaseM¬yMsMLinCoSs¬yMsBaseMgBSs¬finSupp0˙g¬yMs=glinCMSs
40 22 39 bitrd SVMLModSBaseM¬yMsLSpanMSs¬yMsBaseMgBSs¬finSupp0˙g¬yMs=glinCMSs
41 40 2ralbidv SVMLModSBaseMsSyB0˙¬yMsLSpanMSssSyB0˙¬yMsBaseMgBSs¬finSupp0˙g¬yMs=glinCMSs
42 simpllr SVMLModSBaseMsSyB0˙MLMod
43 eldifi yB0˙yB
44 43 adantl sSyB0˙yB
45 44 adantl SVMLModSBaseMsSyB0˙yB
46 ssel2 SBaseMsSsBaseM
47 46 ad2ant2lr SVMLModSBaseMsSyB0˙sBaseM
48 eqid M=M
49 17 1 48 2 lmodvscl MLModyBsBaseMyMsBaseM
50 42 45 47 49 syl3anc SVMLModSBaseMsSyB0˙yMsBaseM
51 50 notnotd SVMLModSBaseMsSyB0˙¬¬yMsBaseM
52 nbfal ¬¬yMsBaseM¬yMsBaseM
53 51 52 sylib SVMLModSBaseMsSyB0˙¬yMsBaseM
54 53 orbi1d SVMLModSBaseMsSyB0˙¬yMsBaseMgBSs¬finSupp0˙g¬yMs=glinCMSsgBSs¬finSupp0˙g¬yMs=glinCMSs
55 54 2ralbidva SVMLModSBaseMsSyB0˙¬yMsBaseMgBSs¬finSupp0˙g¬yMs=glinCMSssSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSs
56 r19.32v yB0˙gBSs¬finSupp0˙g¬yMs=glinCMSsyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSs
57 56 ralbii sSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSssSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSs
58 r19.32v sSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSssSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSs
59 57 58 bitri sSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSssSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSs
60 falim SVMLModSBaseMfBSfinSupp0˙fflinCMS=ZxSfx=0˙
61 sneq s=xs=x
62 61 difeq2d s=xSs=Sx
63 62 oveq2d s=xBSs=BSx
64 oveq2 s=xyMs=yMx
65 62 oveq2d s=xglinCMSs=glinCMSx
66 64 65 eqeq12d s=xyMs=glinCMSsyMx=glinCMSx
67 66 notbid s=x¬yMs=glinCMSs¬yMx=glinCMSx
68 67 orbi2d s=x¬finSupp0˙g¬yMs=glinCMSs¬finSupp0˙g¬yMx=glinCMSx
69 63 68 raleqbidv s=xgBSs¬finSupp0˙g¬yMs=glinCMSsgBSx¬finSupp0˙g¬yMx=glinCMSx
70 69 ralbidv s=xyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSsyB0˙gBSx¬finSupp0˙g¬yMx=glinCMSx
71 70 rspcva xSsSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSsyB0˙gBSx¬finSupp0˙g¬yMx=glinCMSx
72 1 2 3 4 lindslinindsimp2lem5 SVMLModSBaseMxSfBSfinSupp0˙fflinCMS=ZyB0˙gBSx¬finSupp0˙g¬yMx=glinCMSxfx=0˙
73 72 expr SVMLModSBaseMxSfBSfinSupp0˙fflinCMS=ZyB0˙gBSx¬finSupp0˙g¬yMx=glinCMSxfx=0˙
74 73 com14 yB0˙gBSx¬finSupp0˙g¬yMx=glinCMSxxSfBSfinSupp0˙fflinCMS=ZSVMLModSBaseMfx=0˙
75 71 74 syl xSsSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSsxSfBSfinSupp0˙fflinCMS=ZSVMLModSBaseMfx=0˙
76 75 ex xSsSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSsxSfBSfinSupp0˙fflinCMS=ZSVMLModSBaseMfx=0˙
77 76 pm2.43a xSsSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSsfBSfinSupp0˙fflinCMS=ZSVMLModSBaseMfx=0˙
78 77 com14 SVMLModSBaseMsSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSsfBSfinSupp0˙fflinCMS=ZxSfx=0˙
79 78 imp SVMLModSBaseMsSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSsfBSfinSupp0˙fflinCMS=ZxSfx=0˙
80 79 expdimp SVMLModSBaseMsSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSsfBSfinSupp0˙fflinCMS=ZxSfx=0˙
81 80 ralrimdv SVMLModSBaseMsSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSsfBSfinSupp0˙fflinCMS=ZxSfx=0˙
82 81 ralrimiva SVMLModSBaseMsSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSsfBSfinSupp0˙fflinCMS=ZxSfx=0˙
83 82 expcom sSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSsSVMLModSBaseMfBSfinSupp0˙fflinCMS=ZxSfx=0˙
84 60 83 jaoi sSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSsSVMLModSBaseMfBSfinSupp0˙fflinCMS=ZxSfx=0˙
85 84 com12 SVMLModSBaseMsSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSsfBSfinSupp0˙fflinCMS=ZxSfx=0˙
86 59 85 syl5bi SVMLModSBaseMsSyB0˙gBSs¬finSupp0˙g¬yMs=glinCMSsfBSfinSupp0˙fflinCMS=ZxSfx=0˙
87 55 86 sylbid SVMLModSBaseMsSyB0˙¬yMsBaseMgBSs¬finSupp0˙g¬yMs=glinCMSsfBSfinSupp0˙fflinCMS=ZxSfx=0˙
88 41 87 sylbid SVMLModSBaseMsSyB0˙¬yMsLSpanMSsfBSfinSupp0˙fflinCMS=ZxSfx=0˙
89 88 impr SVMLModSBaseMsSyB0˙¬yMsLSpanMSsfBSfinSupp0˙fflinCMS=ZxSfx=0˙
90 8 89 jca SVMLModSBaseMsSyB0˙¬yMsLSpanMSsS𝒫BaseMfBSfinSupp0˙fflinCMS=ZxSfx=0˙
91 90 ex SVMLModSBaseMsSyB0˙¬yMsLSpanMSsS𝒫BaseMfBSfinSupp0˙fflinCMS=ZxSfx=0˙