Metamath Proof Explorer

Theorem lpssat

Description: Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. ( chpssati analog.) (Contributed by NM, 11-Jan-2015)

Ref Expression
Hypotheses lpssat.s 
|- S = ( LSubSp ` W )
lpssat.a 
|- A = ( LSAtoms ` W )
lpssat.w 
|- ( ph -> W e. LMod )
lpssat.t 
|- ( ph -> T e. S )
lpssat.u 
|- ( ph -> U e. S )
lpssat.l 
|- ( ph -> T C. U )
Assertion lpssat 
|- ( ph -> E. q e. A ( q C_ U /\ -. q C_ T ) )

Proof

Step Hyp Ref Expression
1 lpssat.s 
 |-  S = ( LSubSp ` W )
2 lpssat.a 
 |-  A = ( LSAtoms ` W )
3 lpssat.w 
 |-  ( ph -> W e. LMod )
4 lpssat.t 
 |-  ( ph -> T e. S )
5 lpssat.u 
 |-  ( ph -> U e. S )
6 lpssat.l 
 |-  ( ph -> T C. U )
7 dfpss3 
 |-  ( T C. U <-> ( T C_ U /\ -. U C_ T ) )
8 7 simprbi 
 |-  ( T C. U -> -. U C_ T )
9 6 8 syl 
 |-  ( ph -> -. U C_ T )
10 iman 
 |-  ( ( q C_ U -> q C_ T ) <-> -. ( q C_ U /\ -. q C_ T ) )
11 10 ralbii 
 |-  ( A. q e. A ( q C_ U -> q C_ T ) <-> A. q e. A -. ( q C_ U /\ -. q C_ T ) )
12 ss2rab 
 |-  ( { q e. A | q C_ U } C_ { q e. A | q C_ T } <-> A. q e. A ( q C_ U -> q C_ T ) )
13 1 2 lsatlss 
 |-  ( W e. LMod -> A C_ S )
14 rabss2 
 |-  ( A C_ S -> { q e. A | q C_ T } C_ { q e. S | q C_ T } )
15 uniss 
 |-  ( { q e. A | q C_ T } C_ { q e. S | q C_ T } -> U. { q e. A | q C_ T } C_ U. { q e. S | q C_ T } )
16 3 13 14 15 4syl 
 |-  ( ph -> U. { q e. A | q C_ T } C_ U. { q e. S | q C_ T } )
17 unimax 
 |-  ( T e. S -> U. { q e. S | q C_ T } = T )
18 4 17 syl 
 |-  ( ph -> U. { q e. S | q C_ T } = T )
19 eqid 
 |-  ( Base ` W ) = ( Base ` W )
20 19 1 lssss 
 |-  ( T e. S -> T C_ ( Base ` W ) )
21 4 20 syl 
 |-  ( ph -> T C_ ( Base ` W ) )
22 18 21 eqsstrd 
 |-  ( ph -> U. { q e. S | q C_ T } C_ ( Base ` W ) )
23 16 22 sstrd 
 |-  ( ph -> U. { q e. A | q C_ T } C_ ( Base ` W ) )
24 uniss 
 |-  ( { q e. A | q C_ U } C_ { q e. A | q C_ T } -> U. { q e. A | q C_ U } C_ U. { q e. A | q C_ T } )
25 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
26 19 25 lspss 
 |-  ( ( W e. LMod /\ U. { q e. A | q C_ T } C_ ( Base ` W ) /\ U. { q e. A | q C_ U } C_ U. { q e. A | q C_ T } ) -> ( ( LSpan ` W ) ` U. { q e. A | q C_ U } ) C_ ( ( LSpan ` W ) ` U. { q e. A | q C_ T } ) )
27 3 23 24 26 syl2an3an 
 |-  ( ( ph /\ { q e. A | q C_ U } C_ { q e. A | q C_ T } ) -> ( ( LSpan ` W ) ` U. { q e. A | q C_ U } ) C_ ( ( LSpan ` W ) ` U. { q e. A | q C_ T } ) )
28 1 25 2 lssats 
 |-  ( ( W e. LMod /\ U e. S ) -> U = ( ( LSpan ` W ) ` U. { q e. A | q C_ U } ) )
29 3 5 28 syl2anc 
 |-  ( ph -> U = ( ( LSpan ` W ) ` U. { q e. A | q C_ U } ) )
30 29 adantr 
 |-  ( ( ph /\ { q e. A | q C_ U } C_ { q e. A | q C_ T } ) -> U = ( ( LSpan ` W ) ` U. { q e. A | q C_ U } ) )
31 1 25 2 lssats 
 |-  ( ( W e. LMod /\ T e. S ) -> T = ( ( LSpan ` W ) ` U. { q e. A | q C_ T } ) )
32 3 4 31 syl2anc 
 |-  ( ph -> T = ( ( LSpan ` W ) ` U. { q e. A | q C_ T } ) )
33 32 adantr 
 |-  ( ( ph /\ { q e. A | q C_ U } C_ { q e. A | q C_ T } ) -> T = ( ( LSpan ` W ) ` U. { q e. A | q C_ T } ) )
34 27 30 33 3sstr4d 
 |-  ( ( ph /\ { q e. A | q C_ U } C_ { q e. A | q C_ T } ) -> U C_ T )
35 34 ex 
 |-  ( ph -> ( { q e. A | q C_ U } C_ { q e. A | q C_ T } -> U C_ T ) )
36 12 35 biimtrrid 
 |-  ( ph -> ( A. q e. A ( q C_ U -> q C_ T ) -> U C_ T ) )
37 11 36 biimtrrid 
 |-  ( ph -> ( A. q e. A -. ( q C_ U /\ -. q C_ T ) -> U C_ T ) )
38 9 37 mtod 
 |-  ( ph -> -. A. q e. A -. ( q C_ U /\ -. q C_ T ) )
39 dfrex2 
 |-  ( E. q e. A ( q C_ U /\ -. q C_ T ) <-> -. A. q e. A -. ( q C_ U /\ -. q C_ T ) )
40 38 39 sylibr 
 |-  ( ph -> E. q e. A ( q C_ U /\ -. q C_ T ) )