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=BaseK
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=BaseK
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≤KW
9 8 adantr ⊢K∈HL∧W∈H∧F∈T→oc⁡K⁡W∈Atoms⁡K∧¬oc⁡K⁡W≤KW
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≤KW→R⁡F=oc⁡K⁡Wjoin⁡KF⁡oc⁡K⁡Wmeet⁡KW
13 9 12 mpd3an3 ⊢K∈HL∧W∈H∧F∈T→R⁡F=oc⁡K⁡Wjoin⁡KF⁡oc⁡K⁡Wmeet⁡KW
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⁡Wjoin⁡KF⁡oc⁡K⁡W∈B
25 15 21 23 24 syl3anc ⊢K∈HL∧W∈H∧F∈T→oc⁡K⁡Wjoin⁡KF⁡oc⁡K⁡W∈B
26 1 11 latmcl ⊢K∈Lat∧oc⁡K⁡Wjoin⁡KF⁡oc⁡K⁡W∈B∧W∈B→oc⁡K⁡Wjoin⁡KF⁡oc⁡K⁡Wmeet⁡KW∈B
27 15 25 19 26 syl3anc ⊢K∈HL∧W∈H∧F∈T→oc⁡K⁡Wjoin⁡KF⁡oc⁡K⁡Wmeet⁡KW∈B
28 13 27 eqeltrd ⊢K∈HL∧W∈H∧F∈T→R⁡F∈B