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 = ( LSubSp ` W )
lssat.a 
|- A = ( LSAtoms ` W )
Assertion lssat 
|- ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ U C. V ) -> E. p e. A ( p C_ V /\ -. p C_ U ) )

Proof

Step Hyp Ref Expression
1 lssat.s 
 |-  S = ( LSubSp ` W )
2 lssat.a 
 |-  A = ( LSAtoms ` W )
3 dfpss3 
 |-  ( U C. V <-> ( U C_ V /\ -. V C_ U ) )
4 3 simprbi 
 |-  ( U C. V -> -. V C_ U )
5 ss2rab 
 |-  ( { p e. A | p C_ V } C_ { p e. A | p C_ U } <-> A. p e. A ( p C_ V -> p C_ U ) )
6 iman 
 |-  ( ( p C_ V -> p C_ U ) <-> -. ( p C_ V /\ -. p C_ U ) )
7 6 ralbii 
 |-  ( A. p e. A ( p C_ V -> p C_ U ) <-> A. p e. A -. ( p C_ V /\ -. p C_ U ) )
8 5 7 bitr2i 
 |-  ( A. p e. A -. ( p C_ V /\ -. p C_ U ) <-> { p e. A | p C_ V } C_ { p e. A | p C_ U } )
9 simpl1 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ { p e. A | p C_ V } C_ { p e. A | p C_ U } ) -> W e. LMod )
10 1 2 lsatlss 
 |-  ( W e. LMod -> A C_ S )
11 rabss2 
 |-  ( A C_ S -> { p e. A | p C_ U } C_ { p e. S | p C_ U } )
12 uniss 
 |-  ( { p e. A | p C_ U } C_ { p e. S | p C_ U } -> U. { p e. A | p C_ U } C_ U. { p e. S | p C_ U } )
13 9 10 11 12 4syl 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ { p e. A | p C_ V } C_ { p e. A | p C_ U } ) -> U. { p e. A | p C_ U } C_ U. { p e. S | p C_ U } )
14 simpl2 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ { p e. A | p C_ V } C_ { p e. A | p C_ U } ) -> U e. S )
15 unimax 
 |-  ( U e. S -> U. { p e. S | p C_ U } = U )
16 14 15 syl 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ { p e. A | p C_ V } C_ { p e. A | p C_ U } ) -> U. { p e. S | p C_ U } = U )
17 eqid 
 |-  ( Base ` W ) = ( Base ` W )
18 17 1 lssss 
 |-  ( U e. S -> U C_ ( Base ` W ) )
19 14 18 syl 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ { p e. A | p C_ V } C_ { p e. A | p C_ U } ) -> U C_ ( Base ` W ) )
20 16 19 eqsstrd 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ { p e. A | p C_ V } C_ { p e. A | p C_ U } ) -> U. { p e. S | p C_ U } C_ ( Base ` W ) )
21 13 20 sstrd 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ { p e. A | p C_ V } C_ { p e. A | p C_ U } ) -> U. { p e. A | p C_ U } C_ ( Base ` W ) )
22 uniss 
 |-  ( { p e. A | p C_ V } C_ { p e. A | p C_ U } -> U. { p e. A | p C_ V } C_ U. { p e. A | p C_ U } )
23 22 adantl 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ { p e. A | p C_ V } C_ { p e. A | p C_ U } ) -> U. { p e. A | p C_ V } C_ U. { p e. A | p C_ U } )
24 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
25 17 24 lspss 
 |-  ( ( W e. LMod /\ U. { p e. A | p C_ U } C_ ( Base ` W ) /\ U. { p e. A | p C_ V } C_ U. { p e. A | p C_ U } ) -> ( ( LSpan ` W ) ` U. { p e. A | p C_ V } ) C_ ( ( LSpan ` W ) ` U. { p e. A | p C_ U } ) )
26 9 21 23 25 syl3anc 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ { p e. A | p C_ V } C_ { p e. A | p C_ U } ) -> ( ( LSpan ` W ) ` U. { p e. A | p C_ V } ) C_ ( ( LSpan ` W ) ` U. { p e. A | p C_ U } ) )
27 simpl3 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ { p e. A | p C_ V } C_ { p e. A | p C_ U } ) -> V e. S )
28 1 24 2 lssats 
 |-  ( ( W e. LMod /\ V e. S ) -> V = ( ( LSpan ` W ) ` U. { p e. A | p C_ V } ) )
29 9 27 28 syl2anc 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ { p e. A | p C_ V } C_ { p e. A | p C_ U } ) -> V = ( ( LSpan ` W ) ` U. { p e. A | p C_ V } ) )
30 1 24 2 lssats 
 |-  ( ( W e. LMod /\ U e. S ) -> U = ( ( LSpan ` W ) ` U. { p e. A | p C_ U } ) )
31 9 14 30 syl2anc 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ { p e. A | p C_ V } C_ { p e. A | p C_ U } ) -> U = ( ( LSpan ` W ) ` U. { p e. A | p C_ U } ) )
32 26 29 31 3sstr4d 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ { p e. A | p C_ V } C_ { p e. A | p C_ U } ) -> V C_ U )
33 32 ex 
 |-  ( ( W e. LMod /\ U e. S /\ V e. S ) -> ( { p e. A | p C_ V } C_ { p e. A | p C_ U } -> V C_ U ) )
34 8 33 syl5bi 
 |-  ( ( W e. LMod /\ U e. S /\ V e. S ) -> ( A. p e. A -. ( p C_ V /\ -. p C_ U ) -> V C_ U ) )
35 34 con3dimp 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ -. V C_ U ) -> -. A. p e. A -. ( p C_ V /\ -. p C_ U ) )
36 dfrex2 
 |-  ( E. p e. A ( p C_ V /\ -. p C_ U ) <-> -. A. p e. A -. ( p C_ V /\ -. p C_ U ) )
37 35 36 sylibr 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ -. V C_ U ) -> E. p e. A ( p C_ V /\ -. p C_ U ) )
38 4 37 sylan2 
 |-  ( ( ( W e. LMod /\ U e. S /\ V e. S ) /\ U C. V ) -> E. p e. A ( p C_ V /\ -. p C_ U ) )