This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 4noncolr2

Description: A way to express 4 non-colinear atoms (rotated right 2 places). (Contributed by NM, 11-Jul-2012)

		Ref	Expression
	Hypotheses	3noncol.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		3noncol.j	$⊢ \underset{˙}{\lor} = join (K)$
		3noncol.a	$⊢ A = Atoms (K)$
	Assertion	4noncolr2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (R \neq S \land \neg P \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land \neg Q \underset{˙}{\leq} ((R \underset{˙}{\lor} S) \underset{˙}{\lor} P))$

Proof

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		simp11	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to K \in HL$
5		simp13	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to Q \in A$
6		simp2l	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to R \in A$
7		simp2r	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to S \in A$
8		simp12	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to P \in A$
9	1 2 3	4noncolr3	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))$
10	1 2 3	4noncolr3	$⊢ ((K \in HL \land Q \in A \land R \in A) \land (S \in A \land P \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to (R \neq S \land \neg P \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land \neg Q \underset{˙}{\leq} ((R \underset{˙}{\lor} S) \underset{˙}{\lor} P))$
11	4 5 6 7 8 9 10	syl321anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (R \neq S \land \neg P \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land \neg Q \underset{˙}{\leq} ((R \underset{˙}{\lor} S) \underset{˙}{\lor} P))$