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