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 e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) e. 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 
 |-  ( le ` K ) = ( le ` K )
6 eqid 
 |-  ( oc ` K ) = ( oc ` K )
7 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
8 5 6 7 2 lhpocnel 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( oc ` K ) ` W ) e. ( Atoms ` K ) /\ -. ( ( oc ` K ) ` W ) ( le ` K ) W ) )
9 8 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( ( oc ` K ) ` W ) e. ( Atoms ` K ) /\ -. ( ( oc ` K ) ` W ) ( le ` K ) W ) )
10 eqid 
 |-  ( join ` K ) = ( join ` K )
11 eqid 
 |-  ( meet ` K ) = ( meet ` K )
12 5 10 11 7 2 3 4 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( ( ( oc ` K ) ` W ) e. ( Atoms ` K ) /\ -. ( ( oc ` K ) ` W ) ( le ` K ) W ) ) -> ( R ` F ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( F ` ( ( oc ` K ) ` W ) ) ) ( meet ` K ) W ) )
13 9 12 mpd3an3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( F ` ( ( oc ` K ) ` W ) ) ) ( meet ` K ) W ) )
14 hllat 
 |-  ( K e. HL -> K e. Lat )
15 14 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> K e. Lat )
16 hlop 
 |-  ( K e. HL -> K e. OP )
17 16 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> K e. OP )
18 1 2 lhpbase 
 |-  ( W e. H -> W e. B )
19 18 ad2antlr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> W e. B )
20 1 6 opoccl 
 |-  ( ( K e. OP /\ W e. B ) -> ( ( oc ` K ) ` W ) e. B )
21 17 19 20 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( oc ` K ) ` W ) e. B )
22 1 2 3 ltrncl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( ( oc ` K ) ` W ) e. B ) -> ( F ` ( ( oc ` K ) ` W ) ) e. B )
23 21 22 mpd3an3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( F ` ( ( oc ` K ) ` W ) ) e. B )
24 1 10 latjcl 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` W ) e. B /\ ( F ` ( ( oc ` K ) ` W ) ) e. B ) -> ( ( ( oc ` K ) ` W ) ( join ` K ) ( F ` ( ( oc ` K ) ` W ) ) ) e. B )
25 15 21 23 24 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( ( oc ` K ) ` W ) ( join ` K ) ( F ` ( ( oc ` K ) ` W ) ) ) e. B )
26 1 11 latmcl 
 |-  ( ( K e. Lat /\ ( ( ( oc ` K ) ` W ) ( join ` K ) ( F ` ( ( oc ` K ) ` W ) ) ) e. B /\ W e. B ) -> ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( F ` ( ( oc ` K ) ` W ) ) ) ( meet ` K ) W ) e. B )
27 15 25 19 26 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( F ` ( ( oc ` K ) ` W ) ) ) ( meet ` K ) W ) e. B )
28 13 27 eqeltrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) e. B )