Theorem cdlemg2fv

Description: Value of a translation in terms of an associated atom. cdleme48fvg with simpler hypotheses. TODO: Use ltrnj to vastly simplify. (Contributed by NM, 23-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.b	|- B = ( Base ` K )
Assertion	cdlemg2fv	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( X e. B /\ -. X .<_ W ) ) /\ ( F e. T /\ ( P .\/ ( X ./\ W ) ) = X ) ) -> ( F ` X ) = ( ( F ` P ) .\/ ( X ./\ W ) ) )

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