Metamath Proof Explorer


Theorem 4noncolr1

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

Ref Expression
Hypotheses 3noncol.l ˙ = K
3noncol.j ˙ = join K
3noncol.a A = Atoms K
Assertion 4noncolr1 K HL P A Q A R A S A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R S P ¬ Q ˙ S ˙ P ¬ R ˙ S ˙ P ˙ Q

Proof

Step Hyp Ref Expression
1 3noncol.l ˙ = K
2 3noncol.j ˙ = join K
3 3noncol.a A = Atoms K
4 simp11 K HL P A Q A R A S A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R K HL
5 simp13 K HL P A Q A R A S A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q A
6 simp2l K HL P A Q A R A S A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R R A
7 simp2r K HL P A Q A R A S A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R S A
8 simp12 K HL P A Q A R A S A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R P A
9 1 2 3 4noncolr3 K HL P A Q A R A S A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q R ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S
10 1 2 3 4noncolr2 K HL Q A R A S A P A Q R ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S S P ¬ Q ˙ S ˙ P ¬ R ˙ S ˙ P ˙ Q
11 4 5 6 7 8 9 10 syl321anc K HL P A Q A R A S A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R S P ¬ Q ˙ S ˙ P ¬ R ˙ S ˙ P ˙ Q