3dimlem4

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

Proof

Step	Hyp	Ref	Expression
1		3dim0.j	$⊢ \underset{˙}{\lor} = join (K)$
2		3dim0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		3dim0.a	$⊢ A = Atoms (K)$
4		simp2l	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \to P \neq Q$
5		simp2r	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \to \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
6		simp11	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to K \in HL$
7		simp2l	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to R \in A$
8		simp12	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to P \in A$
9		simp13	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to Q \in A$
10		simp3l	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to Q \neq R$
11	10	necomd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to R \neq Q$
12	2 1 3	hlatexch2	$⊢ (K \in HL \land (R \in A \land P \in A \land Q \in A) \land R \neq Q) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to P \underset{˙}{\leq} (R \underset{˙}{\lor} Q))$
13	6 7 8 9 11 12	syl131anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to P \underset{˙}{\leq} (R \underset{˙}{\lor} Q))$
14	1 3	hlatjcom	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\lor} R = R \underset{˙}{\lor} Q$
15	6 9 7 14	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to Q \underset{˙}{\lor} R = R \underset{˙}{\lor} Q$
16	15	breq2d	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow P \underset{˙}{\leq} (R \underset{˙}{\lor} Q))$
17	13 16	sylibrd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
18	17	3ad2ant1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
19	5 18	mtod	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
20		simp11	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \to (K \in HL \land P \in A \land Q \in A)$
21		simp12	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \to (R \in A \land S \in A)$
22		simp13r	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \to \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
23		simp3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \to \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)$
24	1 2 3	3dimlem4a	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (\neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
25	20 21 22 5 23 24	syl113anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \to \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
26	4 19 25	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \to (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$

Metamath Proof Explorer

Theorem 3dimlem4

Proof