Theorem cdlemg8d

Description: TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013)

	Ref	Expression
Hypotheses	cdlemg8.l	|- .<_ = ( le ` K )
	cdlemg8.j	|- .\/ = ( join ` K )
	cdlemg8.m	|- ./\ = ( meet ` K )
	cdlemg8.a	|- A = ( Atoms ` K )
	cdlemg8.h	|- H = ( LHyp ` K )
	cdlemg8.t	|- T = ( ( LTrn ` K ) ` W )
Assertion	cdlemg8d	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ F e. T ) /\ ( G e. T /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) = ( P .\/ Q ) /\ ( F ` ( G ` P ) ) =/= P ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) ./\ W ) = ( ( Q .\/ ( F ` ( G ` Q ) ) ) ./\ W ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemg8.l	|- .<_ = ( le ` K )
2		cdlemg8.j	|- .\/ = ( join ` K )
3		cdlemg8.m	|- ./\ = ( meet ` K )
4		cdlemg8.a	|- A = ( Atoms ` K )
5		cdlemg8.h	|- H = ( LHyp ` K )
6		cdlemg8.t	|- T = ( ( LTrn ` K ) ` W )
7	1 2 3 4 5 6	cdlemg8b	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ F e. T ) /\ ( G e. T /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) = ( P .\/ Q ) /\ ( F ` ( G ` P ) ) =/= P ) ) -> ( P .\/ ( F ` ( G ` P ) ) ) = ( P .\/ Q ) )
8	1 2 3 4 5 6	cdlemg8c	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ F e. T ) /\ ( G e. T /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) = ( P .\/ Q ) /\ ( F ` ( G ` P ) ) =/= P ) ) -> ( Q .\/ ( F ` ( G ` Q ) ) ) = ( P .\/ Q ) )
9	7 8	eqtr4d	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ F e. T ) /\ ( G e. T /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) = ( P .\/ Q ) /\ ( F ` ( G ` P ) ) =/= P ) ) -> ( P .\/ ( F ` ( G ` P ) ) ) = ( Q .\/ ( F ` ( G ` Q ) ) ) )
10	9	oveq1d	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ F e. T ) /\ ( G e. T /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) = ( P .\/ Q ) /\ ( F ` ( G ` P ) ) =/= P ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) ./\ W ) = ( ( Q .\/ ( F ` ( G ` Q ) ) ) ./\ W ) )