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 3 adantr 
 |-  ( ( ph /\ { p e. A | p C_ T } C_ { p e. A | p C_ U } ) -> W e. LMod )
11 1 2 lsatlss 
 |-  ( W e. LMod -> A C_ S )
12 rabss2 
 |-  ( A C_ S -> { p e. A | p C_ U } C_ { p e. S | p C_ U } )
13 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 } )
14 3 11 12 13 4syl 
 |-  ( ph -> U. { p e. A | p C_ U } C_ U. { p e. S | p C_ U } )
15 unimax 
 |-  ( U e. S -> U. { p e. S | p C_ U } = U )
16 5 15 syl 
 |-  ( ph -> 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 5 18 syl 
 |-  ( ph -> U C_ ( Base ` W ) )
20 16 19 eqsstrd 
 |-  ( ph -> U. { p e. S | p C_ U } C_ ( Base ` W ) )
21 14 20 sstrd 
 |-  ( ph -> U. { p e. A | p C_ U } C_ ( Base ` W ) )
22 21 adantr 
 |-  ( ( ph /\ { p e. A | p C_ T } C_ { p e. A | p C_ U } ) -> U. { p e. A | p C_ U } C_ ( Base ` W ) )
23 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 } )
24 23 adantl 
 |-  ( ( ph /\ { 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 } )
25 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
26 17 25 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 } ) )
27 10 22 24 26 syl3anc 
 |-  ( ( 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 } ) )
28 27 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 } ) ) )
29 1 25 2 lssats 
 |-  ( ( W e. LMod /\ T e. S ) -> T = ( ( LSpan ` W ) ` U. { p e. A | p C_ T } ) )
30 3 4 29 syl2anc 
 |-  ( ph -> T = ( ( LSpan ` W ) ` U. { p e. A | p C_ T } ) )
31 1 25 2 lssats 
 |-  ( ( W e. LMod /\ U e. S ) -> U = ( ( LSpan ` W ) ` U. { p e. A | p C_ U } ) )
32 3 5 31 syl2anc 
 |-  ( ph -> U = ( ( LSpan ` W ) ` U. { p e. A | p C_ U } ) )
33 30 32 sseq12d 
 |-  ( ph -> ( T C_ U <-> ( ( LSpan ` W ) ` U. { p e. A | p C_ T } ) C_ ( ( LSpan ` W ) ` U. { p e. A | p C_ U } ) ) )
34 28 33 sylibrd 
 |-  ( ph -> ( { p e. A | p C_ T } C_ { p e. A | p C_ U } -> T C_ U ) )
35 9 34 syl5bir 
 |-  ( ph -> ( A. p e. A ( p C_ T -> p C_ U ) -> T C_ U ) )
36 8 35 impbid2 
 |-  ( ph -> ( T C_ U <-> A. p e. A ( p C_ T -> p C_ U ) ) )