3atlem4

	Ref	Expression
Hypotheses	3at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	3at.j	$⊢ \underset{˙}{\lor} = join (K)$
	3at.a	$⊢ A = Atoms (K)$
Assertion	3atlem4	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} R$

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		simp11	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to K \in HL$
5		simp12	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to (P \in A \land Q \in A \land R \in A)$
6		simp13l	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to S \in A$
7		simp13r	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to T \in A$
8		simp123	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to R \in A$
9	6 7 8	3jca	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to (S \in A \land T \in A \land R \in A)$
10		simp2l	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
11	4	hllatd	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to K \in Lat$
12		eqid	$⊢ {Base}_{K} = {Base}_{K}$
13	12 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
14	8 13	syl	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to R \in {Base}_{K}$
15		simp121	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to P \in A$
16	12 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
17	15 16	syl	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to P \in {Base}_{K}$
18		simp122	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to Q \in A$
19	12 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
20	18 19	syl	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to Q \in {Base}_{K}$
21	12 1 2	latnlej1l	$⊢ (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 P$
22	11 14 17 20 10 21	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 (\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} R)) \to R \neq P$
23	22	necomd	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to P \neq R$
24		simp2r	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to P \neq Q$
25	24	necomd	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to Q \neq P$
26	1 2 3	hlatexch1	$⊢ (K \in HL \land (Q \in A \land R \in A \land P \in A) \land Q \neq P) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
27	4 18 8 15 25 26	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 (\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} R)) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
28	10 27	mtod	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
29		simp3	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} R)$
30	1 2 3	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 R \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq R \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} R)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} R)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} R$
31	4 5 9 10 23 28 29 30	syl331anc	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \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} R)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} R$

Metamath Proof Explorer

Theorem 3atlem4

Proof