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 φ W LMod
lssatle.t φ T S
lssatle.u φ U S
Assertion lssatle φ T U p A p T p U

Proof

Step Hyp Ref Expression
1 lssatle.s S = LSubSp W
2 lssatle.a A = LSAtoms W
3 lssatle.w φ W LMod
4 lssatle.t φ T S
5 lssatle.u φ U S
6 sstr p T T U p U
7 6 expcom T U p T p U
8 7 ralrimivw T U p A p T p U
9 ss2rab p A | p T p A | p U p A p T p U
10 3 adantr φ p A | p T p A | p U W LMod
11 1 2 lsatlss W LMod A S
12 rabss2 A S p A | p U p S | p U
13 uniss p A | p U p S | p U p A | p U p S | p U
14 3 11 12 13 4syl φ p A | p U p S | p U
15 unimax U S p S | p U = U
16 5 15 syl φ p S | p U = U
17 eqid Base W = Base W
18 17 1 lssss U S U Base W
19 5 18 syl φ U Base W
20 16 19 eqsstrd φ p S | p U Base W
21 14 20 sstrd φ p A | p U Base W
22 21 adantr φ p A | p T p A | p U p A | p U Base W
23 uniss p A | p T p A | p U p A | p T p A | p U
24 23 adantl φ p A | p T p A | p U p A | p T p A | p U
25 eqid LSpan W = LSpan W
26 17 25 lspss W LMod p A | p U Base W p A | p T p A | p U LSpan W p A | p T LSpan W p A | p U
27 10 22 24 26 syl3anc φ p A | p T p A | p U LSpan W p A | p T LSpan W p A | p U
28 27 ex φ p A | p T p A | p U LSpan W p A | p T LSpan W p A | p U
29 1 25 2 lssats W LMod T S T = LSpan W p A | p T
30 3 4 29 syl2anc φ T = LSpan W p A | p T
31 1 25 2 lssats W LMod U S U = LSpan W p A | p U
32 3 5 31 syl2anc φ U = LSpan W p A | p U
33 30 32 sseq12d φ T U LSpan W p A | p T LSpan W p A | p U
34 28 33 sylibrd φ p A | p T p A | p U T U
35 9 34 syl5bir φ p A p T p U T U
36 8 35 impbid2 φ T U p A p T p U