4noncolr3

Description: A way to express 4 non-colinear atoms (rotated right 3 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	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))$

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	4	hllatd	$⊢ ((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 Lat$
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		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
9	6 8	syl	$⊢ ((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 {Base}_{K}$
10		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$
11	7 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
12	10 11	syl	$⊢ ((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 {Base}_{K}$
13		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$
14	7 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
15	13 14	syl	$⊢ ((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 {Base}_{K}$
16		simp32	$⊢ ((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 \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
17	7 1 2	latnlej1r	$⊢ (K \in Lat \land (R \in {Base}_{K} \land P \in {Base}_{K} \land Q \in {Base}_{K}) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \neq Q$
18	5 9 12 15 16 17	syl131anc	$⊢ ((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 Q$
19	18	necomd	$⊢ ((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$
20		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$
21	7 3	atbase	$⊢ S \in A \to S \in {Base}_{K}$
22	20 21	syl	$⊢ ((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 {Base}_{K}$
23	7 2	latjcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land R \in {Base}_{K}) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
24	5 15 9 23	syl3anc	$⊢ ((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 \underset{˙}{\lor} R \in {Base}_{K}$
25		simp33	$⊢ ((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 \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
26	2 3	hlatjass	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = P \underset{˙}{\lor} (Q \underset{˙}{\lor} R)$
27	4 10 13 6 26	syl13anc	$⊢ ((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 \underset{˙}{\lor} Q) \underset{˙}{\lor} R = P \underset{˙}{\lor} (Q \underset{˙}{\lor} R)$
28	27	breq2d	$⊢ ((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 \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leftrightarrow S \underset{˙}{\leq} (P \underset{˙}{\lor} (Q \underset{˙}{\lor} R)))$
29	25 28	mtbid	$⊢ ((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 \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} (Q \underset{˙}{\lor} R))$
30	7 1 2	latnlej2r	$⊢ (K \in Lat \land (S \in {Base}_{K} \land P \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K}) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} (Q \underset{˙}{\lor} R))) \to \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
31	5 22 12 24 29 30	syl131anc	$⊢ ((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 \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
32		simp31	$⊢ ((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 \neq Q$
33	1 2 3	hlatexch1	$⊢ (K \in HL \land (P \in A \land R \in A \land Q \in A) \land P \neq Q) \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \to R \underset{˙}{\leq} (Q \underset{˙}{\lor} P))$
34	4 10 6 13 32 33	syl131anc	$⊢ ((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 \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \to R \underset{˙}{\leq} (Q \underset{˙}{\lor} P))$
35	7 2	latjcom	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
36	5 12 15 35	syl3anc	$⊢ ((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 \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
37	36	breq2d	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow R \underset{˙}{\leq} (Q \underset{˙}{\lor} P))$
38	34 37	sylibrd	$⊢ ((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 \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
39	16 38	mtod	$⊢ ((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 \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
40	7 1 2 3	hlexch1	$⊢ (K \in HL \land (P \in A \land S \in A \land Q \underset{˙}{\lor} R \in {Base}_{K}) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to (P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S) \to S \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} P))$
41	4 10 20 24 39 40	syl131anc	$⊢ ((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 \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S) \to S \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} P))$
42	7 2	latjcom	$⊢ (K \in Lat \land Q \in {Base}_{K} \land R \in {Base}_{K}) \to Q \underset{˙}{\lor} R = R \underset{˙}{\lor} Q$
43	5 15 9 42	syl3anc	$⊢ ((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 \underset{˙}{\lor} R = R \underset{˙}{\lor} Q$
44	43	oveq1d	$⊢ ((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 \underset{˙}{\lor} R) \underset{˙}{\lor} P = (R \underset{˙}{\lor} Q) \underset{˙}{\lor} P$
45	7 2	latj31	$⊢ (K \in Lat \land (R \in {Base}_{K} \land Q \in {Base}_{K} \land P \in {Base}_{K})) \to (R \underset{˙}{\lor} Q) \underset{˙}{\lor} P = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
46	5 9 15 12 45	syl13anc	$⊢ ((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 \underset{˙}{\lor} Q) \underset{˙}{\lor} P = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
47	44 46	eqtrd	$⊢ ((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 \underset{˙}{\lor} R) \underset{˙}{\lor} P = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
48	47	breq2d	$⊢ ((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 \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} P) \leftrightarrow S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
49	41 48	sylibd	$⊢ ((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 \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S) \to S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
50	25 49	mtod	$⊢ ((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 \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)$
51	19 31 50	3jca	$⊢ ((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))$

Metamath Proof Explorer

Theorem 4noncolr3

Proof