Theorem cdleme16g

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph on p. 114, Eq. (1). F and G represent f(s) and f(t) respectively. We show, in their notation, (s \/ t) /\ w=(f(s) \/ f(t)) /\ w. (Contributed by NM, 11-Oct-2012)

	Ref	Expression
Hypotheses	cdleme12.l	|- .<_ = ( le ` K )
	cdleme12.j	|- .\/ = ( join ` K )
	cdleme12.m	|- ./\ = ( meet ` K )
	cdleme12.a	|- A = ( Atoms ` K )
	cdleme12.h	|- H = ( LHyp ` K )
	cdleme12.u	|- U = ( ( P .\/ Q ) ./\ W )
	cdleme12.f	|- F = ( ( S .\/ U ) ./\ ( Q .\/ ( ( P .\/ S ) ./\ W ) ) )
	cdleme12.g	|- G = ( ( T .\/ U ) ./\ ( Q .\/ ( ( P .\/ T ) ./\ W ) ) )
Assertion	cdleme16g	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( P =/= Q /\ S =/= T ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ -. U .<_ ( S .\/ T ) ) ) -> ( ( S .\/ T ) ./\ W ) = ( ( F .\/ G ) ./\ W ) )

Proof

Step	Hyp	Ref	Expression
1		cdleme12.l	|- .<_ = ( le ` K )
2		cdleme12.j	|- .\/ = ( join ` K )
3		cdleme12.m	|- ./\ = ( meet ` K )
4		cdleme12.a	|- A = ( Atoms ` K )
5		cdleme12.h	|- H = ( LHyp ` K )
6		cdleme12.u	|- U = ( ( P .\/ Q ) ./\ W )
7		cdleme12.f	|- F = ( ( S .\/ U ) ./\ ( Q .\/ ( ( P .\/ S ) ./\ W ) ) )
8		cdleme12.g	|- G = ( ( T .\/ U ) ./\ ( Q .\/ ( ( P .\/ T ) ./\ W ) ) )
9	1 2 3 4 5 6 7 8	cdleme16e	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( P =/= Q /\ S =/= T ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ -. U .<_ ( S .\/ T ) ) ) -> ( ( S .\/ T ) ./\ ( F .\/ G ) ) = ( ( S .\/ T ) ./\ W ) )
10	1 2 3 4 5 6 7 8	cdleme16f	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( P =/= Q /\ S =/= T ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ -. U .<_ ( S .\/ T ) ) ) -> ( ( S .\/ T ) ./\ ( F .\/ G ) ) = ( ( F .\/ G ) ./\ W ) )
11	9 10	eqtr3d	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( P =/= Q /\ S =/= T ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ -. U .<_ ( S .\/ T ) ) ) -> ( ( S .\/ T ) ./\ W ) = ( ( F .\/ G ) ./\ W ) )