Metamath Proof Explorer


Theorem lssat

Description: Two subspaces in a proper subset relationship imply the existence of a 1-dim subspace less than or equal to one but not the other. ( chpssati analog.) (Contributed by NM, 9-Apr-2014)

Ref Expression
Hypotheses lssat.s S=LSubSpW
lssat.a A=LSAtomsW
Assertion lssat WLModUSVSUVpApV¬pU

Proof

Step Hyp Ref Expression
1 lssat.s S=LSubSpW
2 lssat.a A=LSAtomsW
3 dfpss3 UVUV¬VU
4 3 simprbi UV¬VU
5 ss2rab pA|pVpA|pUpApVpU
6 iman pVpU¬pV¬pU
7 6 ralbii pApVpUpA¬pV¬pU
8 5 7 bitr2i pA¬pV¬pUpA|pVpA|pU
9 simpl1 WLModUSVSpA|pVpA|pUWLMod
10 1 2 lsatlss WLModAS
11 rabss2 ASpA|pUpS|pU
12 uniss pA|pUpS|pUpA|pUpS|pU
13 9 10 11 12 4syl WLModUSVSpA|pVpA|pUpA|pUpS|pU
14 simpl2 WLModUSVSpA|pVpA|pUUS
15 unimax USpS|pU=U
16 14 15 syl WLModUSVSpA|pVpA|pUpS|pU=U
17 eqid BaseW=BaseW
18 17 1 lssss USUBaseW
19 14 18 syl WLModUSVSpA|pVpA|pUUBaseW
20 16 19 eqsstrd WLModUSVSpA|pVpA|pUpS|pUBaseW
21 13 20 sstrd WLModUSVSpA|pVpA|pUpA|pUBaseW
22 uniss pA|pVpA|pUpA|pVpA|pU
23 22 adantl WLModUSVSpA|pVpA|pUpA|pVpA|pU
24 eqid LSpanW=LSpanW
25 17 24 lspss WLModpA|pUBaseWpA|pVpA|pULSpanWpA|pVLSpanWpA|pU
26 9 21 23 25 syl3anc WLModUSVSpA|pVpA|pULSpanWpA|pVLSpanWpA|pU
27 simpl3 WLModUSVSpA|pVpA|pUVS
28 1 24 2 lssats WLModVSV=LSpanWpA|pV
29 9 27 28 syl2anc WLModUSVSpA|pVpA|pUV=LSpanWpA|pV
30 1 24 2 lssats WLModUSU=LSpanWpA|pU
31 9 14 30 syl2anc WLModUSVSpA|pVpA|pUU=LSpanWpA|pU
32 26 29 31 3sstr4d WLModUSVSpA|pVpA|pUVU
33 32 ex WLModUSVSpA|pVpA|pUVU
34 8 33 syl5bi WLModUSVSpA¬pV¬pUVU
35 34 con3dimp WLModUSVS¬VU¬pA¬pV¬pU
36 dfrex2 pApV¬pU¬pA¬pV¬pU
37 35 36 sylibr WLModUSVS¬VUpApV¬pU
38 4 37 sylan2 WLModUSVSUVpApV¬pU