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	$⊢ \underset{˙}{\leq} = \leq_{K}$
	3noncol.j	$⊢ \underset{˙}{\lor} = join (K)$
	3noncol.a	$⊢ A = Atoms (K)$
Assertion	3noncolr1N	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \neq P \land \neg Q \underset{˙}{\leq} (R \underset{˙}{\lor} P))$

Step	Hyp	Ref	Expression
1		3noncol.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		3noncol.j	$⊢ \underset{˙}{\lor} = join (K)$
3		3noncol.a	$⊢ A = Atoms (K)$
4		simp1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in HL$
5		simp22	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in A$
6		simp23	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \in A$
7		simp21	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \in A$
8	1 2 3	3noncolr2	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (Q \neq R \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
9	1 2 3	3noncolr2	$⊢ (K \in HL \land (Q \in A \land R \in A \land P \in A) \land (Q \neq R \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to (R \neq P \land \neg Q \underset{˙}{\leq} (R \underset{˙}{\lor} P))$
10	4 5 6 7 8 9	syl131anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \neq P \land \neg Q \underset{˙}{\leq} (R \underset{˙}{\lor} P))$

Metamath Proof Explorer