Metamath Proof Explorer

Theorem trlcl

Description: Closure of the trace of a lattice translation. (Contributed by NM, 22-May-2012)

Ref Expression
Hypotheses trlcl.b ⊢ B = Base K
trlcl.h ⊢ H = LHyp ⁡ K
trlcl.t ⊢ T = LTrn ⁡ K ⁡ W
trlcl.r ⊢ R = trL ⁡ K ⁡ W
Assertion trlcl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → R ⁡ F ∈ B

Proof

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