dalawlem3

Description: Lemma for dalaw . First piece of dalawlem5 . (Contributed by NM, 4-Oct-2012)

	Ref	Expression
Hypotheses	dalawlem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dalawlem.j	$⊢ \underset{˙}{\lor} = join (K)$
	dalawlem.m	$⊢ \underset{˙}{\land} = meet (K)$
	dalawlem.a	$⊢ A = Atoms (K)$
Assertion	dalawlem3	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$

Proof

Step	Hyp	Ref	Expression
1		dalawlem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dalawlem.j	$⊢ \underset{˙}{\lor} = join (K)$
3		dalawlem.m	$⊢ \underset{˙}{\land} = meet (K)$
4		dalawlem.a	$⊢ A = Atoms (K)$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6		simp11	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to K \in HL$
7	6	hllatd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to K \in Lat$
8		simp22	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to Q \in A$
9		simp32	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to T \in A$
10	5 2 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land T \in A) \to Q \underset{˙}{\lor} T \in {Base}_{K}$
11	6 8 9 10	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to Q \underset{˙}{\lor} T \in {Base}_{K}$
12		simp21	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to P \in A$
13	5 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
14	12 13	syl	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to P \in {Base}_{K}$
15	5 2	latjcl	$⊢ (K \in Lat \land Q \underset{˙}{\lor} T \in {Base}_{K} \land P \in {Base}_{K}) \to (Q \underset{˙}{\lor} T) \underset{˙}{\lor} P \in {Base}_{K}$
16	7 11 14 15	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\lor} T) \underset{˙}{\lor} P \in {Base}_{K}$
17		simp31	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to S \in A$
18	5 4	atbase	$⊢ S \in A \to S \in {Base}_{K}$
19	17 18	syl	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to S \in {Base}_{K}$
20	5 3	latmcl	$⊢ (K \in Lat \land (Q \underset{˙}{\lor} T) \underset{˙}{\lor} P \in {Base}_{K} \land S \in {Base}_{K}) \to ((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S \in {Base}_{K}$
21	7 16 19 20	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S \in {Base}_{K}$
22		simp23	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to R \in A$
23	5 2 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
24	6 8 22 23	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
25		simp33	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to U \in A$
26	5 4	atbase	$⊢ U \in A \to U \in {Base}_{K}$
27	25 26	syl	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to U \in {Base}_{K}$
28	5 3	latmcl	$⊢ (K \in Lat \land Q \underset{˙}{\lor} R \in {Base}_{K} \land U \in {Base}_{K}) \to (Q \underset{˙}{\lor} R) \underset{˙}{\land} U \in {Base}_{K}$
29	7 24 27 28	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\land} U \in {Base}_{K}$
30	5 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land P \in A) \to R \underset{˙}{\lor} P \in {Base}_{K}$
31	6 22 12 30	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to R \underset{˙}{\lor} P \in {Base}_{K}$
32	5 2 4	hlatjcl	$⊢ (K \in HL \land U \in A \land S \in A) \to U \underset{˙}{\lor} S \in {Base}_{K}$
33	6 25 17 32	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to U \underset{˙}{\lor} S \in {Base}_{K}$
34	5 3	latmcl	$⊢ (K \in Lat \land R \underset{˙}{\lor} P \in {Base}_{K} \land U \underset{˙}{\lor} S \in {Base}_{K}) \to (R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S) \in {Base}_{K}$
35	7 31 33 34	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S) \in {Base}_{K}$
36	5 2	latjcl	$⊢ (K \in Lat \land (Q \underset{˙}{\lor} R) \underset{˙}{\land} U \in {Base}_{K} \land (R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S) \in {Base}_{K}) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \in {Base}_{K}$
37	7 29 35 36	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \in {Base}_{K}$
38	5 2 4	hlatjcl	$⊢ (K \in HL \land T \in A \land U \in A) \to T \underset{˙}{\lor} U \in {Base}_{K}$
39	6 9 25 38	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to T \underset{˙}{\lor} U \in {Base}_{K}$
40	5 3	latmcl	$⊢ (K \in Lat \land Q \underset{˙}{\lor} R \in {Base}_{K} \land T \underset{˙}{\lor} U \in {Base}_{K}) \to (Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U) \in {Base}_{K}$
41	7 24 39 40	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U) \in {Base}_{K}$
42	5 2	latjcl	$⊢ (K \in Lat \land (Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U) \in {Base}_{K} \land (R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S) \in {Base}_{K}) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \in {Base}_{K}$
43	7 41 35 42	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \in {Base}_{K}$
44	5 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
45	8 44	syl	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to Q \in {Base}_{K}$
46	5 3	latmcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land U \in {Base}_{K}) \to Q \underset{˙}{\land} U \in {Base}_{K}$
47	7 45 27 46	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to Q \underset{˙}{\land} U \in {Base}_{K}$
48	5 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land S \in A) \to P \underset{˙}{\lor} S \in {Base}_{K}$
49	6 12 17 48	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to P \underset{˙}{\lor} S \in {Base}_{K}$
50	5 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} S \in {Base}_{K} \land Q \in {Base}_{K}) \to (P \underset{˙}{\lor} S) \underset{˙}{\land} Q \in {Base}_{K}$
51	7 49 45 50	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (P \underset{˙}{\lor} S) \underset{˙}{\land} Q \in {Base}_{K}$
52	5 2	latjcl	$⊢ (K \in Lat \land Q \underset{˙}{\land} U \in {Base}_{K} \land (P \underset{˙}{\lor} S) \underset{˙}{\land} Q \in {Base}_{K}) \to (Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \in {Base}_{K}$
53	7 47 51 52	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \in {Base}_{K}$
54	5 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land (Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \in {Base}_{K}) \to P \underset{˙}{\lor} ((Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q)) \in {Base}_{K}$
55	7 14 53 54	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to P \underset{˙}{\lor} ((Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q)) \in {Base}_{K}$
56	5 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
57	22 56	syl	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to R \in {Base}_{K}$
58	5 2	latjcl	$⊢ (K \in Lat \land R \in {Base}_{K} \land (Q \underset{˙}{\lor} R) \underset{˙}{\land} U \in {Base}_{K}) \to R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \in {Base}_{K}$
59	7 57 29 58	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \in {Base}_{K}$
60	5 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \in {Base}_{K}) \to P \underset{˙}{\lor} (R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U)) \in {Base}_{K}$
61	7 14 59 60	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to P \underset{˙}{\lor} (R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U)) \in {Base}_{K}$
62	5 2	latjcl	$⊢ (K \in Lat \land Q \underset{˙}{\land} U \in {Base}_{K} \land P \in {Base}_{K}) \to (Q \underset{˙}{\land} U) \underset{˙}{\lor} P \in {Base}_{K}$
63	7 47 14 62	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\land} U) \underset{˙}{\lor} P \in {Base}_{K}$
64	5 1 2 3	latmlej22	$⊢ (K \in Lat \land (S \in {Base}_{K} \land (Q \underset{˙}{\lor} T) \underset{˙}{\lor} P \in {Base}_{K} \land (Q \underset{˙}{\land} U) \underset{˙}{\lor} P \in {Base}_{K})) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (((Q \underset{˙}{\land} U) \underset{˙}{\lor} P) \underset{˙}{\lor} S)$
65	7 19 16 63 64	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (((Q \underset{˙}{\land} U) \underset{˙}{\lor} P) \underset{˙}{\lor} S)$
66	5 2	latjass	$⊢ (K \in Lat \land (Q \underset{˙}{\land} U \in {Base}_{K} \land P \in {Base}_{K} \land S \in {Base}_{K})) \to ((Q \underset{˙}{\land} U) \underset{˙}{\lor} P) \underset{˙}{\lor} S = (Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} S)$
67	7 47 14 19 66	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\land} U) \underset{˙}{\lor} P) \underset{˙}{\lor} S = (Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} S)$
68	65 67	breqtrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} ((Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} S))$
69	5 3	latmcl	$⊢ (K \in Lat \land Q \underset{˙}{\lor} T \in {Base}_{K} \land P \underset{˙}{\lor} S \in {Base}_{K}) \to (Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S) \in {Base}_{K}$
70	7 11 49 69	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S) \in {Base}_{K}$
71	5 2	latjcl	$⊢ (K \in Lat \land (Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S) \in {Base}_{K} \land P \in {Base}_{K}) \to ((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\lor} P \in {Base}_{K}$
72	7 70 14 71	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\lor} P \in {Base}_{K}$
73	5 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
74	6 12 8 73	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
75	1 2 4	hlatlej2	$⊢ (K \in HL \land P \in A \land S \in A) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} S)$
76	6 12 17 75	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} S)$
77	5 1 3	latmlem2	$⊢ (K \in Lat \land (S \in {Base}_{K} \land P \underset{˙}{\lor} S \in {Base}_{K} \land (Q \underset{˙}{\lor} T) \underset{˙}{\lor} P \in {Base}_{K})) \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} (P \underset{˙}{\lor} S)))$
78	7 19 49 16 77	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} (P \underset{˙}{\lor} S)))$
79	76 78	mpd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} (P \underset{˙}{\lor} S))$
80	1 2 4	hlatlej1	$⊢ (K \in HL \land P \in A \land S \in A) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} S)$
81	6 12 17 80	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} S)$
82	5 1 2 3 4	atmod4i1	$⊢ (K \in HL \land (P \in A \land Q \underset{˙}{\lor} T \in {Base}_{K} \land P \underset{˙}{\lor} S \in {Base}_{K}) \land P \underset{˙}{\leq} (P \underset{˙}{\lor} S)) \to ((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\lor} P = ((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} (P \underset{˙}{\lor} S)$
83	6 12 11 49 81 82	syl131anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\lor} P = ((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} (P \underset{˙}{\lor} S)$
84	79 83	breqtrrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\lor} P)$
85	5 3	latmcom	$⊢ (K \in Lat \land Q \underset{˙}{\lor} T \in {Base}_{K} \land P \underset{˙}{\lor} S \in {Base}_{K}) \to (Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S) = (P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)$
86	7 11 49 85	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S) = (P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)$
87		simp12	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
88	86 87	eqbrtrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
89	1 2 4	hlatlej1	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
90	6 12 8 89	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
91	5 1 2	latjle12	$⊢ (K \in Lat \land ((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S) \in {Base}_{K} \land P \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K})) \to ((((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\lor} P) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
92	7 70 14 74 91	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\lor} P) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
93	88 90 92	mpbi2and	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\lor} P) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
94	5 1 7 21 72 74 84 93	lattrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
95	5 2	latjcl	$⊢ (K \in Lat \land Q \underset{˙}{\land} U \in {Base}_{K} \land P \underset{˙}{\lor} S \in {Base}_{K}) \to (Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} S) \in {Base}_{K}$
96	7 47 49 95	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} S) \in {Base}_{K}$
97	5 1 3	latlem12	$⊢ (K \in Lat \land (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S \in {Base}_{K} \land (Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} S) \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K})) \to (((((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} ((Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \land (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (((Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))$
98	7 21 96 74 97	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} ((Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \land (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (((Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))$
99	68 94 98	mpbi2and	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (((Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \underset{˙}{\land} (P \underset{˙}{\lor} Q))$
100	5 1 2 3 4	atmod3i1	$⊢ (K \in HL \land (P \in A \land P \underset{˙}{\lor} S \in {Base}_{K} \land Q \in {Base}_{K}) \land P \underset{˙}{\leq} (P \underset{˙}{\lor} S)) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) = (P \underset{˙}{\lor} S) \underset{˙}{\land} (P \underset{˙}{\lor} Q)$
101	6 12 49 45 81 100	syl131anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) = (P \underset{˙}{\lor} S) \underset{˙}{\land} (P \underset{˙}{\lor} Q)$
102	101	oveq2d	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q)) = (Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} (P \underset{˙}{\lor} Q))$
103	5 2	latj12	$⊢ (K \in Lat \land (Q \underset{˙}{\land} U \in {Base}_{K} \land P \in {Base}_{K} \land (P \underset{˙}{\lor} S) \underset{˙}{\land} Q \in {Base}_{K})) \to (Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q)) = P \underset{˙}{\lor} ((Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q))$
104	7 47 14 51 103	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q)) = P \underset{˙}{\lor} ((Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q))$
105	5 1 2 3	latmlej12	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land U \in {Base}_{K} \land P \in {Base}_{K})) \to (Q \underset{˙}{\land} U) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
106	7 45 27 14 105	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\land} U) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
107	5 1 2 3 4	atmod1i1m	$⊢ ((K \in HL \land U \in A) \land (Q \in {Base}_{K} \land P \underset{˙}{\lor} S \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K}) \land (Q \underset{˙}{\land} U) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} (P \underset{˙}{\lor} Q)) = ((Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \underset{˙}{\land} (P \underset{˙}{\lor} Q)$
108	6 25 45 49 74 106 107	syl231anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} (P \underset{˙}{\lor} Q)) = ((Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \underset{˙}{\land} (P \underset{˙}{\lor} Q)$
109	102 104 108	3eqtr3rd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\land} U) \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \underset{˙}{\land} (P \underset{˙}{\lor} Q) = P \underset{˙}{\lor} ((Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q))$
110	99 109	breqtrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (P \underset{˙}{\lor} ((Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q)))$
111	1 2 4	hlatlej1	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
112	6 8 22 111	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
113	1 2 4	hlatlej2	$⊢ (K \in HL \land R \in A \land U \in A) \to U \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
114	6 22 25 113	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to U \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
115	5 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} S \in {Base}_{K} \land Q \underset{˙}{\lor} T \in {Base}_{K}) \to (P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T) \in {Base}_{K}$
116	7 49 11 115	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T) \in {Base}_{K}$
117	5 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land U \in A) \to R \underset{˙}{\lor} U \in {Base}_{K}$
118	6 22 25 117	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to R \underset{˙}{\lor} U \in {Base}_{K}$
119	1 2 4	hlatlej1	$⊢ (K \in HL \land Q \in A \land T \in A) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} T)$
120	6 8 9 119	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} T)$
121	5 1 3	latmlem2	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land Q \underset{˙}{\lor} T \in {Base}_{K} \land P \underset{˙}{\lor} S \in {Base}_{K})) \to (Q \underset{˙}{\leq} (Q \underset{˙}{\lor} T) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)))$
122	7 45 11 49 121	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\leq} (Q \underset{˙}{\lor} T) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)))$
123	120 122	mpd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T))$
124		simp13	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
125	5 1 7 51 116 118 123 124	lattrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
126	5 1 2	latjle12	$⊢ (K \in Lat \land (U \in {Base}_{K} \land (P \underset{˙}{\lor} S) \underset{˙}{\land} Q \in {Base}_{K} \land R \underset{˙}{\lor} U \in {Base}_{K})) \to ((U \underset{˙}{\leq} (R \underset{˙}{\lor} U) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \leftrightarrow (U \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q)) \underset{˙}{\leq} (R \underset{˙}{\lor} U))$
127	7 27 51 118 126	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((U \underset{˙}{\leq} (R \underset{˙}{\lor} U) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \leftrightarrow (U \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q)) \underset{˙}{\leq} (R \underset{˙}{\lor} U))$
128	114 125 127	mpbi2and	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (U \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
129	5 2	latjcl	$⊢ (K \in Lat \land U \in {Base}_{K} \land (P \underset{˙}{\lor} S) \underset{˙}{\land} Q \in {Base}_{K}) \to U \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \in {Base}_{K}$
130	7 27 51 129	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to U \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \in {Base}_{K}$
131	5 1 3	latmlem12	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K}) \land (U \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \in {Base}_{K} \land R \underset{˙}{\lor} U \in {Base}_{K})) \to ((Q \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land (U \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \to (Q \underset{˙}{\land} (U \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q))) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (R \underset{˙}{\lor} U)))$
132	7 45 24 130 118 131	syl122anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land (U \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \to (Q \underset{˙}{\land} (U \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q))) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (R \underset{˙}{\lor} U)))$
133	112 128 132	mp2and	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\land} (U \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q))) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (R \underset{˙}{\lor} U))$
134	5 1 3	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} S \in {Base}_{K} \land Q \in {Base}_{K}) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \underset{˙}{\leq} Q$
135	7 49 45 134	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \underset{˙}{\leq} Q$
136	5 1 2 3 4	atmod2i2	$⊢ (K \in HL \land (U \in A \land Q \in {Base}_{K} \land (P \underset{˙}{\lor} S) \underset{˙}{\land} Q \in {Base}_{K}) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \underset{˙}{\leq} Q) \to (Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) = Q \underset{˙}{\land} (U \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q))$
137	6 25 45 51 135 136	syl131anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) = Q \underset{˙}{\land} (U \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q))$
138	1 2 4	hlatlej2	$⊢ (K \in HL \land Q \in A \land R \in A) \to R \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
139	6 8 22 138	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to R \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
140	5 1 2 3 4	atmod3i2	$⊢ (K \in HL \land (U \in A \land R \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K}) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) = (Q \underset{˙}{\lor} R) \underset{˙}{\land} (R \underset{˙}{\lor} U)$
141	6 25 57 24 139 140	syl131anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) = (Q \underset{˙}{\lor} R) \underset{˙}{\land} (R \underset{˙}{\lor} U)$
142	133 137 141	3brtr4d	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q)) \underset{˙}{\leq} (R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U))$
143	5 1 2	latjlej2	$⊢ (K \in Lat \land ((Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q) \in {Base}_{K} \land R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \in {Base}_{K} \land P \in {Base}_{K})) \to (((Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q)) \underset{˙}{\leq} (R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U)) \to (P \underset{˙}{\lor} ((Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q))) \underset{˙}{\leq} (P \underset{˙}{\lor} (R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U))))$
144	7 53 59 14 143	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q)) \underset{˙}{\leq} (R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U)) \to (P \underset{˙}{\lor} ((Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q))) \underset{˙}{\leq} (P \underset{˙}{\lor} (R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U))))$
145	142 144	mpd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (P \underset{˙}{\lor} ((Q \underset{˙}{\land} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} Q))) \underset{˙}{\leq} (P \underset{˙}{\lor} (R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U)))$
146	5 1 7 21 55 61 110 145	lattrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (P \underset{˙}{\lor} (R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U)))$
147	5 2	latj13	$⊢ (K \in Lat \land (P \in {Base}_{K} \land R \in {Base}_{K} \land (Q \underset{˙}{\lor} R) \underset{˙}{\land} U \in {Base}_{K})) \to P \underset{˙}{\lor} (R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U)) = ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} (R \underset{˙}{\lor} P)$
148	7 14 57 29 147	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to P \underset{˙}{\lor} (R \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U)) = ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} (R \underset{˙}{\lor} P)$
149	146 148	breqtrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} (R \underset{˙}{\lor} P))$
150	5 1 2 3	latmlej22	$⊢ (K \in Lat \land (S \in {Base}_{K} \land (Q \underset{˙}{\lor} T) \underset{˙}{\lor} P \in {Base}_{K} \land U \in {Base}_{K})) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (U \underset{˙}{\lor} S)$
151	7 19 16 27 150	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (U \underset{˙}{\lor} S)$
152	5 2	latjcl	$⊢ (K \in Lat \land (Q \underset{˙}{\lor} R) \underset{˙}{\land} U \in {Base}_{K} \land R \underset{˙}{\lor} P \in {Base}_{K}) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} (R \underset{˙}{\lor} P) \in {Base}_{K}$
153	7 29 31 152	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} (R \underset{˙}{\lor} P) \in {Base}_{K}$
154	5 1 3	latlem12	$⊢ (K \in Lat \land (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S \in {Base}_{K} \land ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} (R \underset{˙}{\lor} P) \in {Base}_{K} \land U \underset{˙}{\lor} S \in {Base}_{K})) \to (((((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} (R \underset{˙}{\lor} P)) \land (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (U \underset{˙}{\lor} S)) \leftrightarrow (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} ((((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} (R \underset{˙}{\lor} P)) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$
155	7 21 153 33 154	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} (R \underset{˙}{\lor} P)) \land (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (U \underset{˙}{\lor} S)) \leftrightarrow (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} ((((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} (R \underset{˙}{\lor} P)) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$
156	149 151 155	mpbi2and	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} ((((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} (R \underset{˙}{\lor} P)) \underset{˙}{\land} (U \underset{˙}{\lor} S))$
157	5 1 2 3	latmlej21	$⊢ (K \in Lat \land (U \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K} \land S \in {Base}_{K})) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\leq} (U \underset{˙}{\lor} S)$
158	7 27 24 19 157	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\leq} (U \underset{˙}{\lor} S)$
159	5 1 2 3 4	atmod1i1m	$⊢ ((K \in HL \land U \in A) \land (Q \underset{˙}{\lor} R \in {Base}_{K} \land R \underset{˙}{\lor} P \in {Base}_{K} \land U \underset{˙}{\lor} S \in {Base}_{K}) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\leq} (U \underset{˙}{\lor} S)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) = (((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} (R \underset{˙}{\lor} P)) \underset{˙}{\land} (U \underset{˙}{\lor} S)$
160	6 25 24 31 33 158 159	syl231anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) = (((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} (R \underset{˙}{\lor} P)) \underset{˙}{\land} (U \underset{˙}{\lor} S)$
161	156 160	breqtrrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$
162	1 2 4	hlatlej2	$⊢ (K \in HL \land T \in A \land U \in A) \to U \underset{˙}{\leq} (T \underset{˙}{\lor} U)$
163	6 9 25 162	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to U \underset{˙}{\leq} (T \underset{˙}{\lor} U)$
164	5 1 3	latmlem2	$⊢ (K \in Lat \land (U \in {Base}_{K} \land T \underset{˙}{\lor} U \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K})) \to (U \underset{˙}{\leq} (T \underset{˙}{\lor} U) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)))$
165	7 27 39 24 164	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (U \underset{˙}{\leq} (T \underset{˙}{\lor} U) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)))$
166	163 165	mpd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U))$
167	5 1 2	latjlej1	$⊢ (K \in Lat \land ((Q \underset{˙}{\lor} R) \underset{˙}{\land} U \in {Base}_{K} \land (Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U) \in {Base}_{K} \land (R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S) \in {Base}_{K})) \to (((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \to (((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))))$
168	7 29 41 35 167	syl13anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \to (((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))))$
169	166 168	mpd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} R) \underset{˙}{\land} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$
170	5 1 7 21 37 43 161 169	lattrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\lor} P) \underset{˙}{\land} S) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$

Metamath Proof Explorer

Theorem dalawlem3

Proof