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 3 adantr 
 |-  ( ( ph /\ { q e. A | q C_ U } C_ { q e. A | q C_ T } ) -> W e. LMod )
14 1 2 lsatlss 
 |-  ( W e. LMod -> A C_ S )
15 rabss2 
 |-  ( A C_ S -> { q e. A | q C_ T } C_ { q e. S | q C_ T } )
16 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 } )
17 3 14 15 16 4syl 
 |-  ( ph -> U. { q e. A | q C_ T } C_ U. { q e. S | q C_ T } )
18 unimax 
 |-  ( T e. S -> U. { q e. S | q C_ T } = T )
19 4 18 syl 
 |-  ( ph -> U. { q e. S | q C_ T } = T )
20 eqid 
 |-  ( Base ` W ) = ( Base ` W )
21 20 1 lssss 
 |-  ( T e. S -> T C_ ( Base ` W ) )
22 4 21 syl 
 |-  ( ph -> T C_ ( Base ` W ) )
23 19 22 eqsstrd 
 |-  ( ph -> U. { q e. S | q C_ T } C_ ( Base ` W ) )
24 17 23 sstrd 
 |-  ( ph -> U. { q e. A | q C_ T } C_ ( Base ` W ) )
25 24 adantr 
 |-  ( ( ph /\ { q e. A | q C_ U } C_ { q e. A | q C_ T } ) -> U. { q e. A | q C_ T } C_ ( Base ` W ) )
26 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 } )
27 26 adantl 
 |-  ( ( ph /\ { 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 } )
28 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
29 20 28 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 } ) )
30 13 25 27 29 syl3anc 
 |-  ( ( 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 } ) )
31 1 28 2 lssats 
 |-  ( ( W e. LMod /\ U e. S ) -> U = ( ( LSpan ` W ) ` U. { q e. A | q C_ U } ) )
32 3 5 31 syl2anc 
 |-  ( ph -> U = ( ( LSpan ` W ) ` U. { q e. A | q C_ U } ) )
33 32 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 } ) )
34 1 28 2 lssats 
 |-  ( ( W e. LMod /\ T e. S ) -> T = ( ( LSpan ` W ) ` U. { q e. A | q C_ T } ) )
35 3 4 34 syl2anc 
 |-  ( ph -> T = ( ( LSpan ` W ) ` U. { q e. A | q C_ T } ) )
36 35 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 } ) )
37 30 33 36 3sstr4d 
 |-  ( ( ph /\ { q e. A | q C_ U } C_ { q e. A | q C_ T } ) -> U C_ T )
38 37 ex 
 |-  ( ph -> ( { q e. A | q C_ U } C_ { q e. A | q C_ T } -> U C_ T ) )
39 12 38 syl5bir 
 |-  ( ph -> ( A. q e. A ( q C_ U -> q C_ T ) -> U C_ T ) )
40 11 39 syl5bir 
 |-  ( ph -> ( A. q e. A -. ( q C_ U /\ -. q C_ T ) -> U C_ T ) )
41 9 40 mtod 
 |-  ( ph -> -. A. q e. A -. ( q C_ U /\ -. q C_ T ) )
42 dfrex2 
 |-  ( E. q e. A ( q C_ U /\ -. q C_ T ) <-> -. A. q e. A -. ( q C_ U /\ -. q C_ T ) )
43 41 42 sylibr 
 |-  ( ph -> E. q e. A ( q C_ U /\ -. q C_ T ) )