This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )