Theorem cdlemg2jOLDN

Description: TODO: Replace this with ltrnj . (Contributed by NM, 22-Apr-2013) (New usage is discouraged.)

	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 )
Assertion	cdlemg2jOLDN	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ F e. T ) -> ( F ` ( P .\/ Q ) ) = ( ( F ` P ) .\/ ( F ` Q ) ) )

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		eqid	|- ( Base ` K ) = ( Base ` K )
7		eqid	|- ( meet ` K ) = ( meet ` K )
8		eqid	|- ( ( p .\/ q ) ( meet ` K ) W ) = ( ( p .\/ q ) ( meet ` K ) W )
9		eqid	|- ( ( t .\/ ( ( p .\/ q ) ( meet ` K ) W ) ) ( meet ` K ) ( q .\/ ( ( p .\/ t ) ( meet ` K ) W ) ) ) = ( ( t .\/ ( ( p .\/ q ) ( meet ` K ) W ) ) ( meet ` K ) ( q .\/ ( ( p .\/ t ) ( meet ` K ) W ) ) )
10		eqid	|- ( ( p .\/ q ) ( meet ` K ) ( ( ( t .\/ ( ( p .\/ q ) ( meet ` K ) W ) ) ( meet ` K ) ( q .\/ ( ( p .\/ t ) ( meet ` K ) W ) ) ) .\/ ( ( s .\/ t ) ( meet ` K ) W ) ) ) = ( ( p .\/ q ) ( meet ` K ) ( ( ( t .\/ ( ( p .\/ q ) ( meet ` K ) W ) ) ( meet ` K ) ( q .\/ ( ( p .\/ t ) ( meet ` K ) W ) ) ) .\/ ( ( s .\/ t ) ( meet ` K ) W ) ) )
11		eqid	|- ( x e. ( Base ` K ) |-> if ( ( p =/= q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( p .\/ q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( p .\/ q ) ) -> y = ( ( p .\/ q ) ( meet ` K ) ( ( ( t .\/ ( ( p .\/ q ) ( meet ` K ) W ) ) ( meet ` K ) ( q .\/ ( ( p .\/ t ) ( meet ` K ) W ) ) ) .\/ ( ( s .\/ t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t .\/ ( ( p .\/ q ) ( meet ` K ) W ) ) ( meet ` K ) ( q .\/ ( ( p .\/ t ) ( meet ` K ) W ) ) ) ) .\/ ( x ( meet ` K ) W ) ) ) ) , x ) ) = ( x e. ( Base ` K ) |-> if ( ( p =/= q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( p .\/ q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( p .\/ q ) ) -> y = ( ( p .\/ q ) ( meet ` K ) ( ( ( t .\/ ( ( p .\/ q ) ( meet ` K ) W ) ) ( meet ` K ) ( q .\/ ( ( p .\/ t ) ( meet ` K ) W ) ) ) .\/ ( ( s .\/ t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t .\/ ( ( p .\/ q ) ( meet ` K ) W ) ) ( meet ` K ) ( q .\/ ( ( p .\/ t ) ( meet ` K ) W ) ) ) ) .\/ ( x ( meet ` K ) W ) ) ) ) , x ) )
12	6 3 4 7 5 1 2 8 9 10 11	cdlemg2jlemOLDN	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ F e. T ) -> ( F ` ( P .\/ Q ) ) = ( ( F ` P ) .\/ ( F ` Q ) ) )