Metamath Proof Explorer

Theorem 3atlem7

Description: Lemma for 3at . (Contributed by NM, 23-Jun-2012)

		Ref	Expression
	Hypotheses	3at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		3at.j	$⊢ \underset{˙}{\lor} = join (K)$
		3at.a	$⊢ A = Atoms (K)$
	Assertion	3atlem7	$⊢ ((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 Q) \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 Q) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land Q \underset{˙}{\leq} (P \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		simpl2l	$⊢ (((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 Q) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
6		simpl2r	$⊢ (((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 Q) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \to P \neq Q$
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 Q) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
8		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 Q) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)$
9	1 2 3	3atlem6	$⊢ ((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 Q \land 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$
10	4 5 6 7 8 9	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 Q) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
11		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 Q) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land \neg Q \underset{˙}{\leq} (P \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))$
12		simpl2l	$⊢ (((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 Q) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
13		simpl2r	$⊢ (((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 Q) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \to P \neq Q$
14		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 Q) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
15		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 Q) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)$
16	1 2 3	3atlem5	$⊢ ((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 Q \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$
17	11 12 13 14 15 16	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 Q) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
18	10 17	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 Q) \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$