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
|- .<_ = ( le ` K )
trlle.h
|- H = ( LHyp ` K )
trlle.t
|- T = ( ( LTrn ` K ) ` W )
trlle.r
|- R = ( ( trL ` K ) ` W )
Assertion trlle
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) .<_ W )

Proof

Step Hyp Ref Expression
1 trlle.l
 |-  .<_ = ( le ` 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 e. HL /\ W e. H ) -> ( ( ( oc ` K ) ` W ) e. ( Atoms ` K ) /\ -. ( ( oc ` K ) ` W ) .<_ W ) )
8 7 adantr
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( ( oc ` K ) ` W ) e. ( 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 e. HL /\ W e. H ) /\ F e. T /\ ( ( ( oc ` K ) ` W ) e. ( 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 e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( F ` ( ( oc ` K ) ` W ) ) ) ( meet ` K ) W ) )
13 hllat
 |-  ( K e. HL -> K e. Lat )
14 13 ad2antrr
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> K e. Lat )
15 hlop
 |-  ( K e. HL -> K e. OP )
16 15 ad2antrr
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> K e. OP )
17 eqid
 |-  ( Base ` K ) = ( Base ` K )
18 17 2 lhpbase
 |-  ( W e. H -> W e. ( Base ` K ) )
19 18 ad2antlr
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> W e. ( Base ` K ) )
20 17 5 opoccl
 |-  ( ( K e. OP /\ W e. ( Base ` K ) ) -> ( ( oc ` K ) ` W ) e. ( Base ` K ) )
21 16 19 20 syl2anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( oc ` K ) ` W ) e. ( Base ` K ) )
22 17 2 3 ltrncl
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( ( oc ` K ) ` W ) e. ( Base ` K ) ) -> ( F ` ( ( oc ` K ) ` W ) ) e. ( Base ` K ) )
23 21 22 mpd3an3
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( F ` ( ( oc ` K ) ` W ) ) e. ( Base ` K ) )
24 17 9 latjcl
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` W ) e. ( Base ` K ) /\ ( F ` ( ( oc ` K ) ` W ) ) e. ( Base ` K ) ) -> ( ( ( oc ` K ) ` W ) ( join ` K ) ( F ` ( ( oc ` K ) ` W ) ) ) e. ( Base ` K ) )
25 14 21 23 24 syl3anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( ( oc ` K ) ` W ) ( join ` K ) ( F ` ( ( oc ` K ) ` W ) ) ) e. ( Base ` K ) )
26 17 1 10 latmle2
 |-  ( ( K e. Lat /\ ( ( ( oc ` K ) ` W ) ( join ` K ) ( F ` ( ( oc ` K ) ` W ) ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( F ` ( ( oc ` K ) ` W ) ) ) ( meet ` K ) W ) .<_ W )
27 14 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 ) .<_ W )
28 12 27 eqbrtrd
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) .<_ W )