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⁡Wjoin⁡KF⁡oc⁡K⁡Wmeet⁡KW
12 8 11 mpd3an3 ⊢K∈HL∧W∈H∧F∈T→R⁡F=oc⁡K⁡Wjoin⁡KF⁡oc⁡K⁡Wmeet⁡KW
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 ⊢BaseK=BaseK
18 17 2 lhpbase ⊢W∈H→W∈BaseK
19 18 ad2antlr ⊢K∈HL∧W∈H∧F∈T→W∈BaseK
20 17 5 opoccl ⊢K∈OP∧W∈BaseK→oc⁡K⁡W∈BaseK
21 16 19 20 syl2anc ⊢K∈HL∧W∈H∧F∈T→oc⁡K⁡W∈BaseK
22 17 2 3 ltrncl ⊢K∈HL∧W∈H∧F∈T∧oc⁡K⁡W∈BaseK→F⁡oc⁡K⁡W∈BaseK
23 21 22 mpd3an3 ⊢K∈HL∧W∈H∧F∈T→F⁡oc⁡K⁡W∈BaseK
24 17 9 latjcl ⊢K∈Lat∧oc⁡K⁡W∈BaseK∧F⁡oc⁡K⁡W∈BaseK→oc⁡K⁡Wjoin⁡KF⁡oc⁡K⁡W∈BaseK
25 14 21 23 24 syl3anc ⊢K∈HL∧W∈H∧F∈T→oc⁡K⁡Wjoin⁡KF⁡oc⁡K⁡W∈BaseK
26 17 1 10 latmle2 ⊢K∈Lat∧oc⁡K⁡Wjoin⁡KF⁡oc⁡K⁡W∈BaseK∧W∈BaseK→oc⁡K⁡Wjoin⁡KF⁡oc⁡K⁡Wmeet⁡KW≤˙W
27 14 25 19 26 syl3anc ⊢K∈HL∧W∈H∧F∈T→oc⁡K⁡Wjoin⁡KF⁡oc⁡K⁡Wmeet⁡KW≤˙W
28 12 27 eqbrtrd ⊢K∈HL∧W∈H∧F∈T→R⁡F≤˙W