3atlem3

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

Proof

Step	Hyp	Ref	Expression
1		3at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		3at.j	$⊢ \underset{˙}{\lor} = join (K)$
3		3at.a	$⊢ A = Atoms (K)$
4		simpl1	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land P \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A))$
5		simpl21	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land P \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
6		simpl22	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land P \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to P \neq U$
7		simpr	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land P \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to P \underset{˙}{\leq} (T \underset{˙}{\lor} U)$
8	6 7	jca	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land P \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to (P \neq U \land P \underset{˙}{\leq} (T \underset{˙}{\lor} U))$
9		simpl23	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land P \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
10		simpl3	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land P \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)$
11	1 2 3	3atlem2	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (P \neq U \land P \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
12	4 5 8 9 10 11	syl131anc	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land P \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
13		simpl1	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land \neg P \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A))$
14		simpl21	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land \neg P \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
15		simpr	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land \neg P \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to \neg P \underset{˙}{\leq} (T \underset{˙}{\lor} U)$
16		simpl23	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land \neg P \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
17		simpl3	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land \neg P \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)$
18	1 2 3	3atlem1	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg P \underset{˙}{\leq} (T \underset{˙}{\lor} U) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
19	13 14 15 16 17 18	syl131anc	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land \neg P \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
20	12 19	pm2.61dan	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$

Metamath Proof Explorer

Theorem 3atlem3

Proof