Metamath Proof Explorer


Theorem trlle

Description: The trace of a lattice translation is less than the fiducial co-atom W . (Contributed by NM, 25-May-2012)

Ref Expression
Hypotheses trlle.l ˙ = K
trlle.h H = LHyp K
trlle.t T = LTrn K W
trlle.r R = trL K W
Assertion trlle K HL W H F T R F ˙ W

Proof

Step Hyp Ref Expression
1 trlle.l ˙ = K
2 trlle.h H = LHyp K
3 trlle.t T = LTrn K W
4 trlle.r R = trL K W
5 eqid oc K = oc K
6 eqid Atoms K = Atoms K
7 1 5 6 2 lhpocnel K HL W H oc K W Atoms K ¬ oc K W ˙ W
8 7 adantr K HL W H F T oc K W Atoms K ¬ oc K W ˙ W
9 eqid join K = join K
10 eqid meet K = meet K
11 1 9 10 6 2 3 4 trlval2 K HL W H F T oc K W Atoms K ¬ oc K W ˙ W R F = oc K W join K F oc K W meet K W
12 8 11 mpd3an3 K HL W H F T R F = oc K W join K F oc K W meet K W
13 hllat K HL K Lat
14 13 ad2antrr K HL W H F T K Lat
15 hlop K HL K OP
16 15 ad2antrr K HL W H F T K OP
17 eqid Base K = Base K
18 17 2 lhpbase W H W Base K
19 18 ad2antlr K HL W H F T W Base K
20 17 5 opoccl K OP W Base K oc K W Base K
21 16 19 20 syl2anc K HL W H F T oc K W Base K
22 17 2 3 ltrncl K HL W H F T oc K W Base K F oc K W Base K
23 21 22 mpd3an3 K HL W H F T F oc K W Base K
24 17 9 latjcl K Lat oc K W Base K F oc K W Base K oc K W join K F oc K W Base K
25 14 21 23 24 syl3anc K HL W H F T oc K W join K F oc K W Base K
26 17 1 10 latmle2 K Lat oc K W join K F oc K W Base K W Base K oc K W join K F oc K W meet K W ˙ W
27 14 25 19 26 syl3anc K HL W H F T oc K W join K F oc K W meet K W ˙ W
28 12 27 eqbrtrd K HL W H F T R F ˙ W