Theorem trlcoabs

Description: Absorption into a composition by joining with trace. (Contributed by NM, 22-Jul-2013)

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

Proof

Step	Hyp	Ref	Expression
1		trlcoabs.l	|- .<_ = ( le ` K )
2		trlcoabs.j	|- .\/ = ( join ` K )
3		trlcoabs.a	|- A = ( Atoms ` K )
4		trlcoabs.h	|- H = ( LHyp ` K )
5		trlcoabs.t	|- T = ( ( LTrn ` K ) ` W )
6		trlcoabs.r	|- R = ( ( trL ` K ) ` W )
7	1 3 4 5	ltrncoval	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ P e. A ) -> ( ( F o. G ) ` P ) = ( F ` ( G ` P ) ) )
8	7	3adant3r	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F o. G ) ` P ) = ( F ` ( G ` P ) ) )
9	8	oveq1d	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( F o. G ) ` P ) .\/ ( R ` F ) ) = ( ( F ` ( G ` P ) ) .\/ ( R ` F ) ) )
10		simp1	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( K e. HL /\ W e. H ) )
11		simp2l	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> F e. T )
12	1 3 4 5	ltrnel	|- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) )
13	12	3adant2l	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) )
14	1 2 3 4 5 6	trljat3	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) ) -> ( ( G ` P ) .\/ ( R ` F ) ) = ( ( F ` ( G ` P ) ) .\/ ( R ` F ) ) )
15	10 11 13 14	syl3anc	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G ` P ) .\/ ( R ` F ) ) = ( ( F ` ( G ` P ) ) .\/ ( R ` F ) ) )
16	9 15	eqtr4d	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( F o. G ) ` P ) .\/ ( R ` F ) ) = ( ( G ` P ) .\/ ( R ` F ) ) )