Theorem 3noncolr1N

Description: Two ways to express 3 non-colinear atoms (rotated right 1 place). (Contributed by NM, 12-Jul-2012) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		3noncol.l	|- .<_ = ( le ` K )
2		3noncol.j	|- .\/ = ( join ` K )
3		3noncol.a	|- A = ( Atoms ` K )
4		simp1	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> K e. HL )
5		simp22	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> Q e. A )
6		simp23	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> R e. A )
7		simp21	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> P e. A )
8	1 2 3	3noncolr2	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( Q =/= R /\ -. P .<_ ( Q .\/ R ) ) )
9	1 2 3	3noncolr2	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ P e. A ) /\ ( Q =/= R /\ -. P .<_ ( Q .\/ R ) ) ) -> ( R =/= P /\ -. Q .<_ ( R .\/ P ) ) )
10	4 5 6 7 8 9	syl131anc	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( R =/= P /\ -. Q .<_ ( R .\/ P ) ) )