Theorem cdlemg2k

Description: cdleme42keg with simpler hypotheses. TODO: FIX COMMENT. TODO: derive from cdlemg3a , cdlemg2fv2 , cdlemg2jOLDN , ltrnel ? (Contributed by NM, 22-Apr-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemg2inv.h	|- H = ( LHyp ` K )
2		cdlemg2inv.t	|- T = ( ( LTrn ` K ) ` W )
3		cdlemg2j.l	|- .<_ = ( le ` K )
4		cdlemg2j.j	|- .\/ = ( join ` K )
5		cdlemg2j.a	|- A = ( Atoms ` K )
6		cdlemg2j.m	|- ./\ = ( meet ` K )
7		cdlemg2j.u	|- U = ( ( P .\/ Q ) ./\ W )
8		eqid	|- ( Base ` K ) = ( Base ` K )
9		eqid	|- ( ( p .\/ q ) ./\ W ) = ( ( p .\/ q ) ./\ W )
10		eqid	|- ( ( t .\/ ( ( p .\/ q ) ./\ W ) ) ./\ ( q .\/ ( ( p .\/ t ) ./\ W ) ) ) = ( ( t .\/ ( ( p .\/ q ) ./\ W ) ) ./\ ( q .\/ ( ( p .\/ t ) ./\ W ) ) )
11		eqid	|- ( ( p .\/ q ) ./\ ( ( ( t .\/ ( ( p .\/ q ) ./\ W ) ) ./\ ( q .\/ ( ( p .\/ t ) ./\ W ) ) ) .\/ ( ( s .\/ t ) ./\ W ) ) ) = ( ( p .\/ q ) ./\ ( ( ( t .\/ ( ( p .\/ q ) ./\ W ) ) ./\ ( q .\/ ( ( p .\/ t ) ./\ W ) ) ) .\/ ( ( s .\/ t ) ./\ W ) ) )
12		eqid	|- ( x e. ( Base ` K ) |-> if ( ( p =/= q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( if ( s .<_ ( p .\/ q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( p .\/ q ) ) -> y = ( ( p .\/ q ) ./\ ( ( ( t .\/ ( ( p .\/ q ) ./\ W ) ) ./\ ( q .\/ ( ( p .\/ t ) ./\ W ) ) ) .\/ ( ( s .\/ t ) ./\ W ) ) ) ) ) , [_ s / t ]_ ( ( t .\/ ( ( p .\/ q ) ./\ W ) ) ./\ ( q .\/ ( ( p .\/ t ) ./\ W ) ) ) ) .\/ ( x ./\ W ) ) ) ) , x ) ) = ( x e. ( Base ` K ) |-> if ( ( p =/= q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( if ( s .<_ ( p .\/ q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( p .\/ q ) ) -> y = ( ( p .\/ q ) ./\ ( ( ( t .\/ ( ( p .\/ q ) ./\ W ) ) ./\ ( q .\/ ( ( p .\/ t ) ./\ W ) ) ) .\/ ( ( s .\/ t ) ./\ W ) ) ) ) ) , [_ s / t ]_ ( ( t .\/ ( ( p .\/ q ) ./\ W ) ) ./\ ( q .\/ ( ( p .\/ t ) ./\ W ) ) ) ) .\/ ( x ./\ W ) ) ) ) , x ) )
13	8 3 4 6 5 1 2 9 10 11 12 7	cdlemg2klem	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ F e. T ) -> ( ( F ` P ) .\/ ( F ` Q ) ) = ( ( F ` P ) .\/ U ) )