Metamath Proof Explorer


Theorem lbspss

Description: No proper subset of a basis spans the space. (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses lbsind2.j J=LBasisW
lbsind2.n N=LSpanW
lbsind2.f F=ScalarW
lbsind2.o 1˙=1F
lbsind2.z 0˙=0F
lbspss.v V=BaseW
Assertion lbspss WLMod1˙0˙BJCBNCV

Proof

Step Hyp Ref Expression
1 lbsind2.j J=LBasisW
2 lbsind2.n N=LSpanW
3 lbsind2.f F=ScalarW
4 lbsind2.o 1˙=1F
5 lbsind2.z 0˙=0F
6 lbspss.v V=BaseW
7 pssnel CBxxB¬xC
8 7 3ad2ant3 WLMod1˙0˙BJCBxxB¬xC
9 simpl2 WLMod1˙0˙BJCBxB¬xCBJ
10 6 1 lbsss BJBV
11 9 10 syl WLMod1˙0˙BJCBxB¬xCBV
12 simprl WLMod1˙0˙BJCBxB¬xCxB
13 11 12 sseldd WLMod1˙0˙BJCBxB¬xCxV
14 simpl1l WLMod1˙0˙BJCBxB¬xCWLMod
15 11 ssdifssd WLMod1˙0˙BJCBxB¬xCBxV
16 simpl3 WLMod1˙0˙BJCBxB¬xCCB
17 16 pssssd WLMod1˙0˙BJCBxB¬xCCB
18 17 sseld WLMod1˙0˙BJCBxB¬xCyCyB
19 simprr WLMod1˙0˙BJCBxB¬xC¬xC
20 eleq1w y=xyCxC
21 20 notbid y=x¬yC¬xC
22 19 21 syl5ibrcom WLMod1˙0˙BJCBxB¬xCy=x¬yC
23 22 necon2ad WLMod1˙0˙BJCBxB¬xCyCyx
24 18 23 jcad WLMod1˙0˙BJCBxB¬xCyCyByx
25 eldifsn yBxyByx
26 24 25 syl6ibr WLMod1˙0˙BJCBxB¬xCyCyBx
27 26 ssrdv WLMod1˙0˙BJCBxB¬xCCBx
28 6 2 lspss WLModBxVCBxNCNBx
29 14 15 27 28 syl3anc WLMod1˙0˙BJCBxB¬xCNCNBx
30 simpl1r WLMod1˙0˙BJCBxB¬xC1˙0˙
31 1 2 3 4 5 lbsind2 WLMod1˙0˙BJxB¬xNBx
32 14 30 9 12 31 syl211anc WLMod1˙0˙BJCBxB¬xC¬xNBx
33 29 32 ssneldd WLMod1˙0˙BJCBxB¬xC¬xNC
34 nelne1 xV¬xNCVNC
35 13 33 34 syl2anc WLMod1˙0˙BJCBxB¬xCVNC
36 35 necomd WLMod1˙0˙BJCBxB¬xCNCV
37 8 36 exlimddv WLMod1˙0˙BJCBNCV