Theorem ltrnj

Description: Lattice translation of a meet. TODO: change antecedent to K e. HL (Contributed by NM, 25-May-2012)

	Ref	Expression
Hypotheses	ltrnj.b	|- B = ( Base ` K )
	ltrnj.j	|- .\/ = ( join ` K )
	ltrnj.h	|- H = ( LHyp ` K )
	ltrnj.t	|- T = ( ( LTrn ` K ) ` W )
Assertion	ltrnj	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .\/ ( F ` Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		ltrnj.b	|- B = ( Base ` K )
2		ltrnj.j	|- .\/ = ( join ` K )
3		ltrnj.h	|- H = ( LHyp ` K )
4		ltrnj.t	|- T = ( ( LTrn ` K ) ` W )
5		simp1l	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> K e. HL )
6	5	hllatd	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> K e. Lat )
7		eqid	|- ( LAut ` K ) = ( LAut ` K )
8	3 7 4	ltrnlaut	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F e. ( LAut ` K ) )
9	8	3adant3	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> F e. ( LAut ` K ) )
10		simp3l	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> X e. B )
11		simp3r	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> Y e. B )
12	1 2 7	lautj	|- ( ( K e. Lat /\ ( F e. ( LAut ` K ) /\ X e. B /\ Y e. B ) ) -> ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .\/ ( F ` Y ) ) )
13	6 9 10 11 12	syl13anc	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .\/ ( F ` Y ) ) )