Metamath Proof Explorer

Theorem lssatle

Description: The ordering of two subspaces is determined by the atoms under them. ( chrelat3 analog.) (Contributed by NM, 29-Oct-2014)

Ref Expression
Hypotheses lssatle.s 
|- S = ( LSubSp ` W )
lssatle.a 
|- A = ( LSAtoms ` W )
lssatle.w 
|- ( ph -> W e. LMod )
lssatle.t 
|- ( ph -> T e. S )
lssatle.u 
|- ( ph -> U e. S )
Assertion lssatle 
|- ( ph -> ( T C_ U <-> A. p e. A ( p C_ T -> p C_ U ) ) )

Proof

Step Hyp Ref Expression
1 lssatle.s 
 |-  S = ( LSubSp ` W )
2 lssatle.a 
 |-  A = ( LSAtoms ` W )
3 lssatle.w 
 |-  ( ph -> W e. LMod )
4 lssatle.t 
 |-  ( ph -> T e. S )
5 lssatle.u 
 |-  ( ph -> U e. S )
6 sstr 
 |-  ( ( p C_ T /\ T C_ U ) -> p C_ U )
7 6 expcom 
 |-  ( T C_ U -> ( p C_ T -> p C_ U ) )
8 7 ralrimivw 
 |-  ( T C_ U -> A. p e. A ( p C_ T -> p C_ U ) )
9 ss2rab 
 |-  ( { p e. A | p C_ T } C_ { p e. A | p C_ U } <-> A. p e. A ( p C_ T -> p C_ U ) )
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 3 10 11 12 4syl 
 |-  ( ph -> U. { p e. A | p C_ U } C_ U. { p e. S | p C_ U } )
14 unimax 
 |-  ( U e. S -> U. { p e. S | p C_ U } = U )
15 5 14 syl 
 |-  ( ph -> U. { p e. S | p C_ U } = U )
16 eqid 
 |-  ( Base ` W ) = ( Base ` W )
17 16 1 lssss 
 |-  ( U e. S -> U C_ ( Base ` W ) )
18 5 17 syl 
 |-  ( ph -> U C_ ( Base ` W ) )
19 15 18 eqsstrd 
 |-  ( ph -> U. { p e. S | p C_ U } C_ ( Base ` W ) )
20 13 19 sstrd 
 |-  ( ph -> U. { p e. A | p C_ U } C_ ( Base ` W ) )
21 uniss 
 |-  ( { p e. A | p C_ T } C_ { p e. A | p C_ U } -> U. { p e. A | p C_ T } C_ U. { p e. A | p C_ U } )
22 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
23 16 22 lspss 
 |-  ( ( W e. LMod /\ U. { p e. A | p C_ U } C_ ( Base ` W ) /\ U. { p e. A | p C_ T } C_ U. { p e. A | p C_ U } ) -> ( ( LSpan ` W ) ` U. { p e. A | p C_ T } ) C_ ( ( LSpan ` W ) ` U. { p e. A | p C_ U } ) )
24 3 20 21 23 syl2an3an 
 |-  ( ( ph /\ { p e. A | p C_ T } C_ { p e. A | p C_ U } ) -> ( ( LSpan ` W ) ` U. { p e. A | p C_ T } ) C_ ( ( LSpan ` W ) ` U. { p e. A | p C_ U } ) )
25 24 ex 
 |-  ( ph -> ( { p e. A | p C_ T } C_ { p e. A | p C_ U } -> ( ( LSpan ` W ) ` U. { p e. A | p C_ T } ) C_ ( ( LSpan ` W ) ` U. { p e. A | p C_ U } ) ) )
26 1 22 2 lssats 
 |-  ( ( W e. LMod /\ T e. S ) -> T = ( ( LSpan ` W ) ` U. { p e. A | p C_ T } ) )
27 3 4 26 syl2anc 
 |-  ( ph -> T = ( ( LSpan ` W ) ` U. { p e. A | p C_ T } ) )
28 1 22 2 lssats 
 |-  ( ( W e. LMod /\ U e. S ) -> U = ( ( LSpan ` W ) ` U. { p e. A | p C_ U } ) )
29 3 5 28 syl2anc 
 |-  ( ph -> U = ( ( LSpan ` W ) ` U. { p e. A | p C_ U } ) )
30 27 29 sseq12d 
 |-  ( ph -> ( T C_ U <-> ( ( LSpan ` W ) ` U. { p e. A | p C_ T } ) C_ ( ( LSpan ` W ) ` U. { p e. A | p C_ U } ) ) )
31 25 30 sylibrd 
 |-  ( ph -> ( { p e. A | p C_ T } C_ { p e. A | p C_ U } -> T C_ U ) )
32 9 31 biimtrrid 
 |-  ( ph -> ( A. p e. A ( p C_ T -> p C_ U ) -> T C_ U ) )
33 8 32 impbid2 
 |-  ( ph -> ( T C_ U <-> A. p e. A ( p C_ T -> p C_ U ) ) )