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