Theorem ltrncnvleN

Description: Less-than or equal property of lattice translation converse. (Contributed by NM, 10-May-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ltrnle.b	|- B = ( Base ` K )
	ltrnle.l	|- .<_ = ( le ` K )
	ltrnle.h	|- H = ( LHyp ` K )
	ltrnle.t	|- T = ( ( LTrn ` K ) ` W )
Assertion	ltrncnvleN	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> ( X .<_ Y <-> ( `' F ` X ) .<_ ( `' F ` Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		ltrnle.b	|- B = ( Base ` K )
2		ltrnle.l	|- .<_ = ( le ` K )
3		ltrnle.h	|- H = ( LHyp ` K )
4		ltrnle.t	|- T = ( ( LTrn ` K ) ` W )
5		simp1l	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> K e. V )
6		eqid	|- ( LAut ` K ) = ( LAut ` K )
7	3 6 4	ltrnlaut	|- ( ( ( K e. V /\ W e. H ) /\ F e. T ) -> F e. ( LAut ` K ) )
8	7	3adant3	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> F e. ( LAut ` K ) )
9		simp3	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> ( X e. B /\ Y e. B ) )
10	1 2 6	lautcnvle	|- ( ( ( K e. V /\ F e. ( LAut ` K ) ) /\ ( X e. B /\ Y e. B ) ) -> ( X .<_ Y <-> ( `' F ` X ) .<_ ( `' F ` Y ) ) )
11	5 8 9 10	syl21anc	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> ( X .<_ Y <-> ( `' F ` X ) .<_ ( `' F ` Y ) ) )