Theorem 2llnne2N

Description: Condition implying that two intersecting lines are different. (Contributed by NM, 13-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2lnne.l	|- .<_ = ( le ` K )
	2lnne.j	|- .\/ = ( join ` K )
	2lnne.a	|- A = ( Atoms ` K )
Assertion	2llnne2N	|- ( ( K e. HL /\ ( P e. A /\ R e. A ) /\ -. P .<_ ( R .\/ Q ) ) -> ( R .\/ P ) =/= ( R .\/ Q ) )

Proof

Step	Hyp	Ref	Expression
1		2lnne.l	|- .<_ = ( le ` K )
2		2lnne.j	|- .\/ = ( join ` K )
3		2lnne.a	|- A = ( Atoms ` K )
4		simpl	|- ( ( K e. HL /\ ( P e. A /\ R e. A ) ) -> K e. HL )
5		simprr	|- ( ( K e. HL /\ ( P e. A /\ R e. A ) ) -> R e. A )
6		simprl	|- ( ( K e. HL /\ ( P e. A /\ R e. A ) ) -> P e. A )
7	1 2 3	hlatlej2	|- ( ( K e. HL /\ R e. A /\ P e. A ) -> P .<_ ( R .\/ P ) )
8	4 5 6 7	syl3anc	|- ( ( K e. HL /\ ( P e. A /\ R e. A ) ) -> P .<_ ( R .\/ P ) )
9		breq2	|- ( ( R .\/ P ) = ( R .\/ Q ) -> ( P .<_ ( R .\/ P ) <-> P .<_ ( R .\/ Q ) ) )
10	8 9	syl5ibcom	|- ( ( K e. HL /\ ( P e. A /\ R e. A ) ) -> ( ( R .\/ P ) = ( R .\/ Q ) -> P .<_ ( R .\/ Q ) ) )
11	10	necon3bd	|- ( ( K e. HL /\ ( P e. A /\ R e. A ) ) -> ( -. P .<_ ( R .\/ Q ) -> ( R .\/ P ) =/= ( R .\/ Q ) ) )
12	11	3impia	|- ( ( K e. HL /\ ( P e. A /\ R e. A ) /\ -. P .<_ ( R .\/ Q ) ) -> ( R .\/ P ) =/= ( R .\/ Q ) )