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

Metamath Proof Explorer

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