Theorem lplnnlt

Description: Two lattice planes cannot satisfy the less than relation. (Contributed by NM, 7-Jul-2012)

	Ref	Expression
Hypotheses	lplnnlt.s	|- .< = ( lt ` K )
	lplnnlt.p	|- P = ( LPlanes ` K )
Assertion	lplnnlt	|- ( ( K e. HL /\ X e. P /\ Y e. P ) -> -. X .< Y )

Proof

Step	Hyp	Ref	Expression
1		lplnnlt.s	|- .< = ( lt ` K )
2		lplnnlt.p	|- P = ( LPlanes ` K )
3	1	pltirr	|- ( ( K e. HL /\ X e. P ) -> -. X .< X )
4	3	3adant3	|- ( ( K e. HL /\ X e. P /\ Y e. P ) -> -. X .< X )
5		breq2	|- ( X = Y -> ( X .< X <-> X .< Y ) )
6	5	notbid	|- ( X = Y -> ( -. X .< X <-> -. X .< Y ) )
7	4 6	syl5ibcom	|- ( ( K e. HL /\ X e. P /\ Y e. P ) -> ( X = Y -> -. X .< Y ) )
8		eqid	|- ( le ` K ) = ( le ` K )
9	8 1	pltle	|- ( ( K e. HL /\ X e. P /\ Y e. P ) -> ( X .< Y -> X ( le ` K ) Y ) )
10	8 2	lplncmp	|- ( ( K e. HL /\ X e. P /\ Y e. P ) -> ( X ( le ` K ) Y <-> X = Y ) )
11	9 10	sylibd	|- ( ( K e. HL /\ X e. P /\ Y e. P ) -> ( X .< Y -> X = Y ) )
12	11	necon3ad	|- ( ( K e. HL /\ X e. P /\ Y e. P ) -> ( X =/= Y -> -. X .< Y ) )
13	7 12	pm2.61dne	|- ( ( K e. HL /\ X e. P /\ Y e. P ) -> -. X .< Y )