Theorem dihord5a

Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014)

	Ref	Expression
Hypotheses	dihord.b	|- B = ( Base ` K )
	dihord.l	|- .<_ = ( le ` K )
	dihord.h	|- H = ( LHyp ` K )
	dihord.i	|- I = ( ( DIsoH ` K ) ` W )
Assertion	dihord5a	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) ) -> X .<_ Y )

Proof

Step	Hyp	Ref	Expression
1		dihord.b	|- B = ( Base ` K )
2		dihord.l	|- .<_ = ( le ` K )
3		dihord.h	|- H = ( LHyp ` K )
4		dihord.i	|- I = ( ( DIsoH ` K ) ` W )
5		eqid	|- ( join ` K ) = ( join ` K )
6		eqid	|- ( meet ` K ) = ( meet ` K )
7		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
8		eqid	|- ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
9		eqid	|- ( LSSum ` ( ( DVecH ` K ) ` W ) ) = ( LSSum ` ( ( DVecH ` K ) ` W ) )
10	1 2 3 5 6 7 8 9 4	dihord5apre	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) ) -> X .<_ Y )