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 = ( LBasis ` W )
lbsind2.n 
|- N = ( LSpan ` W )
lbsind2.f 
|- F = ( Scalar ` W )
lbsind2.o 
|- .1. = ( 1r ` F )
lbsind2.z 
|- .0. = ( 0g ` F )
lbspss.v 
|- V = ( Base ` W )
Assertion lbspss 
|- ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) -> ( N ` C ) =/= V )

Proof

Step Hyp Ref Expression
1 lbsind2.j 
 |-  J = ( LBasis ` W )
2 lbsind2.n 
 |-  N = ( LSpan ` W )
3 lbsind2.f 
 |-  F = ( Scalar ` W )
4 lbsind2.o 
 |-  .1. = ( 1r ` F )
5 lbsind2.z 
 |-  .0. = ( 0g ` F )
6 lbspss.v 
 |-  V = ( Base ` W )
7 pssnel 
 |-  ( C C. B -> E. x ( x e. B /\ -. x e. C ) )
8 7 3ad2ant3 
 |-  ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) -> E. x ( x e. B /\ -. x e. C ) )
9 simpl2 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> B e. J )
10 6 1 lbsss 
 |-  ( B e. J -> B C_ V )
11 9 10 syl 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> B C_ V )
12 simprl 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> x e. B )
13 11 12 sseldd 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> x e. V )
14 simpl1l 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> W e. LMod )
15 11 ssdifssd 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> ( B \ { x } ) C_ V )
16 simpl3 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> C C. B )
17 16 pssssd 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> C C_ B )
18 17 sseld 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> ( y e. C -> y e. B ) )
19 simprr 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> -. x e. C )
20 eleq1w 
 |-  ( y = x -> ( y e. C <-> x e. C ) )
21 20 notbid 
 |-  ( y = x -> ( -. y e. C <-> -. x e. C ) )
22 19 21 syl5ibrcom 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> ( y = x -> -. y e. C ) )
23 22 necon2ad 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> ( y e. C -> y =/= x ) )
24 18 23 jcad 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> ( y e. C -> ( y e. B /\ y =/= x ) ) )
25 eldifsn 
 |-  ( y e. ( B \ { x } ) <-> ( y e. B /\ y =/= x ) )
26 24 25 syl6ibr 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> ( y e. C -> y e. ( B \ { x } ) ) )
27 26 ssrdv 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> C C_ ( B \ { x } ) )
28 6 2 lspss 
 |-  ( ( W e. LMod /\ ( B \ { x } ) C_ V /\ C C_ ( B \ { x } ) ) -> ( N ` C ) C_ ( N ` ( B \ { x } ) ) )
29 14 15 27 28 syl3anc 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> ( N ` C ) C_ ( N ` ( B \ { x } ) ) )
30 simpl1r 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> .1. =/= .0. )
31 1 2 3 4 5 lbsind2 
 |-  ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ x e. B ) -> -. x e. ( N ` ( B \ { x } ) ) )
32 14 30 9 12 31 syl211anc 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> -. x e. ( N ` ( B \ { x } ) ) )
33 29 32 ssneldd 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> -. x e. ( N ` C ) )
34 nelne1 
 |-  ( ( x e. V /\ -. x e. ( N ` C ) ) -> V =/= ( N ` C ) )
35 13 33 34 syl2anc 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> V =/= ( N ` C ) )
36 35 necomd 
 |-  ( ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) /\ ( x e. B /\ -. x e. C ) ) -> ( N ` C ) =/= V )
37 8 36 exlimddv 
 |-  ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ C C. B ) -> ( N ` C ) =/= V )