3atlem6

	Ref	Expression
Hypotheses	3at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	3at.j	$⊢ \underset{˙}{\lor} = join (K)$
	3at.a	$⊢ A = Atoms (K)$
Assertion	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$

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 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 K \in HL$
5		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 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 \in A$
6		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 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 Q \in A$
7		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 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 R \in A$
8	2 3	hlatj32	$⊢ (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} R) \underset{˙}{\lor} Q$
9	4 5 6 7 8	syl13anc	$⊢ ((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 = (P \underset{˙}{\lor} R) \underset{˙}{\lor} Q$
10	5 7 6	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 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 \in A \land R \in A \land Q \in A)$
11		simp13	$⊢ ((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 (S \in A \land T \in A \land U \in A)$
12		simp21	$⊢ ((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 \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
13		simp22	$⊢ ((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 \neq Q$
14	13	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 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 Q \neq P$
15	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))$
16	4 6 7 5 14 15	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 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 (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
17	12 16	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 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 \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
18	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 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 K \in Lat$
19		eqid	$⊢ {Base}_{K} = {Base}_{K}$
20	19 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
21	7 20	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 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 R \in {Base}_{K}$
22	19 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
23	5 22	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 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 \in {Base}_{K}$
24	19 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
25	6 24	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 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 Q \in {Base}_{K}$
26	19 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$
27	26	necomd	$⊢ (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 P \neq R$
28	18 21 23 25 12 27	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 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 \neq R$
29		simp23	$⊢ ((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
30		simp133	$⊢ ((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 U \in A$
31	1 2 3	hlatexchb1	$⊢ (K \in HL \land (Q \in A \land U \in A \land P \in A) \land Q \neq P) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} U) \leftrightarrow P \underset{˙}{\lor} Q = P \underset{˙}{\lor} U)$
32	4 6 30 5 14 31	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 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 (Q \underset{˙}{\leq} (P \underset{˙}{\lor} U) \leftrightarrow P \underset{˙}{\lor} Q = P \underset{˙}{\lor} U)$
33	29 32	mpbid	$⊢ ((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 = P \underset{˙}{\lor} U$
34	33	breq2d	$⊢ ((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 (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow R \underset{˙}{\leq} (P \underset{˙}{\lor} U))$
35	12 34	mtbid	$⊢ ((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 \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
36		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 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) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)$
37	9 36	eqbrtrrd	$⊢ ((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} R) \underset{˙}{\lor} Q) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)$
38	1 2 3	3atlem5	$⊢ ((K \in HL \land (P \in A \land R \in A \land Q \in A) \land (S \in A \land T \in A \land U \in A)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land P \neq R \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} R) \underset{˙}{\lor} Q) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \to (P \underset{˙}{\lor} R) \underset{˙}{\lor} Q = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
39	4 10 11 17 28 35 37 38	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 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} R) \underset{˙}{\lor} Q = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
40	9 39	eqtrd	$⊢ ((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$

Metamath Proof Explorer

Theorem 3atlem6

Proof