Metamath Proof Explorer


Theorem trlco

Description: The trace of a composition of translations is less than or equal to the join of their traces. Part of proof of Lemma G of Crawley p. 116, second paragraph on p. 117. (Contributed by NM, 2-Jun-2013)

Ref Expression
Hypotheses trlco.l
|- .<_ = ( le ` K )
trlco.j
|- .\/ = ( join ` K )
trlco.h
|- H = ( LHyp ` K )
trlco.t
|- T = ( ( LTrn ` K ) ` W )
trlco.r
|- R = ( ( trL ` K ) ` W )
Assertion trlco
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( R ` ( F o. G ) ) .<_ ( ( R ` F ) .\/ ( R ` G ) ) )

Proof

Step Hyp Ref Expression
1 trlco.l
 |-  .<_ = ( le ` K )
2 trlco.j
 |-  .\/ = ( join ` K )
3 trlco.h
 |-  H = ( LHyp ` K )
4 trlco.t
 |-  T = ( ( LTrn ` K ) ` W )
5 trlco.r
 |-  R = ( ( trL ` K ) ` W )
6 eqid
 |-  ( Atoms ` K ) = ( Atoms ` K )
7 1 6 3 lhpexnle
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. ( Atoms ` K ) -. p .<_ W )
8 7 3ad2ant1
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> E. p e. ( Atoms ` K ) -. p .<_ W )
9 simpl1
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( p e. ( Atoms ` K ) /\ -. p .<_ W ) ) -> ( K e. HL /\ W e. H ) )
10 simpl2
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( p e. ( Atoms ` K ) /\ -. p .<_ W ) ) -> F e. T )
11 simpl3
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( p e. ( Atoms ` K ) /\ -. p .<_ W ) ) -> G e. T )
12 simpr
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( p e. ( Atoms ` K ) /\ -. p .<_ W ) ) -> ( p e. ( Atoms ` K ) /\ -. p .<_ W ) )
13 eqid
 |-  ( meet ` K ) = ( meet ` K )
14 1 2 3 4 5 13 6 trlcolem
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( p e. ( Atoms ` K ) /\ -. p .<_ W ) ) -> ( R ` ( F o. G ) ) .<_ ( ( R ` F ) .\/ ( R ` G ) ) )
15 9 10 11 12 14 syl121anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( p e. ( Atoms ` K ) /\ -. p .<_ W ) ) -> ( R ` ( F o. G ) ) .<_ ( ( R ` F ) .\/ ( R ` G ) ) )
16 8 15 rexlimddv
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( R ` ( F o. G ) ) .<_ ( ( R ` F ) .\/ ( R ` G ) ) )