3atlem2

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

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		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 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) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)$
5		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 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 K \in HL$
6	5	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 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 K \in Lat$
7		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 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 \in A$
8		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 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 Q \in A$
9		eqid	$⊢ {Base}_{K} = {Base}_{K}$
10	9 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
11	5 7 8 10	syl3anc	$⊢ ((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 \in {Base}_{K}$
12		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 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 R \in A$
13	9 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
14	12 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 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 R \in {Base}_{K}$
15		simp131	$⊢ ((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 S \in A$
16		simp132	$⊢ ((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 T \in A$
17	9 2 3	hlatjcl	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\lor} T \in {Base}_{K}$
18	5 15 16 17	syl3anc	$⊢ ((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 S \underset{˙}{\lor} T \in {Base}_{K}$
19		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 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 U \in A$
20	9 3	atbase	$⊢ U \in A \to U \in {Base}_{K}$
21	19 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 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 U \in {Base}_{K}$
22	9 2	latjcl	$⊢ (K \in Lat \land S \underset{˙}{\lor} T \in {Base}_{K} \land U \in {Base}_{K}) \to (S \underset{˙}{\lor} T) \underset{˙}{\lor} U \in {Base}_{K}$
23	6 18 21 22	syl3anc	$⊢ ((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 (S \underset{˙}{\lor} T) \underset{˙}{\lor} U \in {Base}_{K}$
24	9 1 2	latjle12	$⊢ (K \in Lat \land (P \underset{˙}{\lor} Q \in {Base}_{K} \land R \in {Base}_{K} \land (S \underset{˙}{\lor} T) \underset{˙}{\lor} U \in {Base}_{K})) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U) \land R \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U))$
25	6 11 14 23 24	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 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{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U) \land R \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U))$
26	4 25	mpbird	$⊢ ((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{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U) \land R \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U))$
27	26	simprd	$⊢ ((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 R \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)$
28	2 3	hlatjass	$⊢ (K \in HL \land (S \in A \land T \in A \land U \in A)) \to (S \underset{˙}{\lor} T) \underset{˙}{\lor} U = S \underset{˙}{\lor} (T \underset{˙}{\lor} U)$
29	5 15 16 19 28	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 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 (S \underset{˙}{\lor} T) \underset{˙}{\lor} U = S \underset{˙}{\lor} (T \underset{˙}{\lor} U)$
30		simp22r	$⊢ ((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{˙}{\leq} (T \underset{˙}{\lor} U)$
31		simp22l	$⊢ ((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 \neq U$
32	1 2 3	hlatexchb2	$⊢ (K \in HL \land (P \in A \land T \in A \land U \in A) \land P \neq U) \to (P \underset{˙}{\leq} (T \underset{˙}{\lor} U) \leftrightarrow P \underset{˙}{\lor} U = T \underset{˙}{\lor} U)$
33	5 7 16 19 31 32	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 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{˙}{\leq} (T \underset{˙}{\lor} U) \leftrightarrow P \underset{˙}{\lor} U = T \underset{˙}{\lor} U)$
34	30 33	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 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} U = T \underset{˙}{\lor} U$
35	34	oveq2d	$⊢ ((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 S \underset{˙}{\lor} (P \underset{˙}{\lor} U) = S \underset{˙}{\lor} (T \underset{˙}{\lor} U)$
36	29 35	eqtr4d	$⊢ ((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 (S \underset{˙}{\lor} T) \underset{˙}{\lor} U = S \underset{˙}{\lor} (P \underset{˙}{\lor} U)$
37	2 3	hlatjass	$⊢ (K \in HL \land (P \in A \land Q \in A \land U \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} U = P \underset{˙}{\lor} (Q \underset{˙}{\lor} U)$
38	5 7 8 19 37	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 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} U = P \underset{˙}{\lor} (Q \underset{˙}{\lor} U)$
39	2 3	hlatj12	$⊢ (K \in HL \land (P \in A \land Q \in A \land U \in A)) \to P \underset{˙}{\lor} (Q \underset{˙}{\lor} U) = Q \underset{˙}{\lor} (P \underset{˙}{\lor} U)$
40	5 7 8 19 39	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 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} U) = Q \underset{˙}{\lor} (P \underset{˙}{\lor} U)$
41	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$
42	5 7 8 12 41	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 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 = (P \underset{˙}{\lor} R) \underset{˙}{\lor} Q$
43	4 42 29	3brtr3d	$⊢ ((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} R) \underset{˙}{\lor} Q) \underset{˙}{\leq} (S \underset{˙}{\lor} (T \underset{˙}{\lor} U))$
44	9 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land R \in A) \to P \underset{˙}{\lor} R \in {Base}_{K}$
45	5 7 12 44	syl3anc	$⊢ ((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} R \in {Base}_{K}$
46	9 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
47	8 46	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 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 Q \in {Base}_{K}$
48	9 3	atbase	$⊢ S \in A \to S \in {Base}_{K}$
49	15 48	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 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 S \in {Base}_{K}$
50	9 2 3	hlatjcl	$⊢ (K \in HL \land T \in A \land U \in A) \to T \underset{˙}{\lor} U \in {Base}_{K}$
51	5 16 19 50	syl3anc	$⊢ ((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 T \underset{˙}{\lor} U \in {Base}_{K}$
52	9 2	latjcl	$⊢ (K \in Lat \land S \in {Base}_{K} \land T \underset{˙}{\lor} U \in {Base}_{K}) \to S \underset{˙}{\lor} (T \underset{˙}{\lor} U) \in {Base}_{K}$
53	6 49 51 52	syl3anc	$⊢ ((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 S \underset{˙}{\lor} (T \underset{˙}{\lor} U) \in {Base}_{K}$
54	9 1 2	latjle12	$⊢ (K \in Lat \land (P \underset{˙}{\lor} R \in {Base}_{K} \land Q \in {Base}_{K} \land S \underset{˙}{\lor} (T \underset{˙}{\lor} U) \in {Base}_{K})) \to (((P \underset{˙}{\lor} R) \underset{˙}{\leq} (S \underset{˙}{\lor} (T \underset{˙}{\lor} U)) \land Q \underset{˙}{\leq} (S \underset{˙}{\lor} (T \underset{˙}{\lor} U))) \leftrightarrow ((P \underset{˙}{\lor} R) \underset{˙}{\lor} Q) \underset{˙}{\leq} (S \underset{˙}{\lor} (T \underset{˙}{\lor} U)))$
55	6 45 47 53 54	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 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} R) \underset{˙}{\leq} (S \underset{˙}{\lor} (T \underset{˙}{\lor} U)) \land Q \underset{˙}{\leq} (S \underset{˙}{\lor} (T \underset{˙}{\lor} U))) \leftrightarrow ((P \underset{˙}{\lor} R) \underset{˙}{\lor} Q) \underset{˙}{\leq} (S \underset{˙}{\lor} (T \underset{˙}{\lor} U)))$
56	43 55	mpbird	$⊢ ((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} R) \underset{˙}{\leq} (S \underset{˙}{\lor} (T \underset{˙}{\lor} U)) \land Q \underset{˙}{\leq} (S \underset{˙}{\lor} (T \underset{˙}{\lor} U)))$
57	56	simprd	$⊢ ((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 Q \underset{˙}{\leq} (S \underset{˙}{\lor} (T \underset{˙}{\lor} U))$
58	57 35	breqtrrd	$⊢ ((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 Q \underset{˙}{\leq} (S \underset{˙}{\lor} (P \underset{˙}{\lor} U))$
59	9 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land U \in A) \to P \underset{˙}{\lor} U \in {Base}_{K}$
60	5 7 19 59	syl3anc	$⊢ ((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} U \in {Base}_{K}$
61		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 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 \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
62	9 1 2 3	hlexchb2	$⊢ (K \in HL \land (Q \in A \land S \in A \land P \underset{˙}{\lor} U \in {Base}_{K}) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \to (Q \underset{˙}{\leq} (S \underset{˙}{\lor} (P \underset{˙}{\lor} U)) \leftrightarrow Q \underset{˙}{\lor} (P \underset{˙}{\lor} U) = S \underset{˙}{\lor} (P \underset{˙}{\lor} U))$
63	5 8 15 60 61 62	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 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 (Q \underset{˙}{\leq} (S \underset{˙}{\lor} (P \underset{˙}{\lor} U)) \leftrightarrow Q \underset{˙}{\lor} (P \underset{˙}{\lor} U) = S \underset{˙}{\lor} (P \underset{˙}{\lor} U))$
64	58 63	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 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 Q \underset{˙}{\lor} (P \underset{˙}{\lor} U) = S \underset{˙}{\lor} (P \underset{˙}{\lor} U)$
65	38 40 64	3eqtrd	$⊢ ((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} U = S \underset{˙}{\lor} (P \underset{˙}{\lor} U)$
66	36 65	eqtr4d	$⊢ ((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 (S \underset{˙}{\lor} T) \underset{˙}{\lor} U = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} U$
67	27 66	breqtrd	$⊢ ((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 R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} U)$
68		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 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 \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
69	9 1 2 3	hlexchb1	$⊢ (K \in HL \land (R \in A \land U \in A \land P \underset{˙}{\lor} Q \in {Base}_{K}) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} U) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} U)$
70	5 12 19 11 68 69	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 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 (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} U) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} U)$
71	67 70	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 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 = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} U$
72	71 66	eqtr4d	$⊢ ((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$

Metamath Proof Explorer

Theorem 3atlem2

Proof