dalawlem11

Description: Lemma for dalaw . First part of dalawlem13 . (Contributed by NM, 17-Sep-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	dalawlem11	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (S \underset{˙}{\lor} T)) \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{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\leq} (Q \underset{˙}{\lor} R) \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		simp21	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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$
9		simp22	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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$
10	5 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
11	6 8 9 10	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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}$
12		simp31	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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$
13		simp32	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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$
14	5 2 4	hlatjcl	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\lor} T \in {Base}_{K}$
15	6 12 13 14	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T \in {Base}_{K}$
16	5 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land S \underset{˙}{\lor} T \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T) \in {Base}_{K}$
17	7 11 15 16	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (S \underset{˙}{\lor} T) \in {Base}_{K}$
18		simp23	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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$
19	5 2 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
20	6 9 18 19	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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}$
21	5 1 3	latmle1	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land S \underset{˙}{\lor} T \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
22	7 11 15 21	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
23		simp12	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (Q \underset{˙}{\lor} R)$
24	5 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
25	9 24	syl	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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}$
26	5 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
27	18 26	syl	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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}$
28	5 1 2	latlej1	$⊢ (K \in Lat \land Q \in {Base}_{K} \land R \in {Base}_{K}) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
29	7 25 27 28	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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)$
30	5 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
31	8 30	syl	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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}$
32	5 1 2	latjle12	$⊢ (K \in Lat \land (P \in {Base}_{K} \land Q \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K})) \to ((P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land Q \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
33	7 31 25 20 32	syl13anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (Q \underset{˙}{\lor} R) \land Q \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
34	23 29 33	mpbi2and	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\leq} (Q \underset{˙}{\lor} R)$
35	5 1 7 17 11 20 22 34	lattrd	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
36	5 4	atbase	$⊢ T \in A \to T \in {Base}_{K}$
37	13 36	syl	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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 {Base}_{K}$
38	5 2	latjcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land T \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} T \in {Base}_{K}$
39	7 11 37 38	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T \in {Base}_{K}$
40	5 3	latmcl	$⊢ (K \in Lat \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} T \in {Base}_{K} \land S \underset{˙}{\lor} T \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} (S \underset{˙}{\lor} T) \in {Base}_{K}$
41	7 39 15 40	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T) \underset{˙}{\land} (S \underset{˙}{\lor} T) \in {Base}_{K}$
42	5 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land P \in A) \to R \underset{˙}{\lor} P \in {Base}_{K}$
43	6 18 8 42	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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}$
44		simp33	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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$
45	5 2 4	hlatjcl	$⊢ (K \in HL \land U \in A \land S \in A) \to U \underset{˙}{\lor} S \in {Base}_{K}$
46	6 44 12 45	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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}$
47	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}$
48	7 43 46 47	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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}$
49	5 4	atbase	$⊢ U \in A \to U \in {Base}_{K}$
50	44 49	syl	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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}$
51	5 2	latjcl	$⊢ (K \in Lat \land (R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S) \in {Base}_{K} \land U \in {Base}_{K}) \to ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} U \in {Base}_{K}$
52	7 48 50 51	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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)) \underset{˙}{\lor} U \in {Base}_{K}$
53	5 2	latjcl	$⊢ (K \in Lat \land ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} U \in {Base}_{K} \land T \in {Base}_{K}) \to (((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} U) \underset{˙}{\lor} T \in {Base}_{K}$
54	7 52 37 53	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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)) \underset{˙}{\lor} U) \underset{˙}{\lor} T \in {Base}_{K}$
55	5 1 2	latlej1	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land T \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T)$
56	7 11 37 55	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T)$
57	5 1 3	latmlem1	$⊢ (K \in Lat \land (P \underset{˙}{\lor} Q \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} T \in {Base}_{K} \land S \underset{˙}{\lor} T \in {Base}_{K})) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} (S \underset{˙}{\lor} T)))$
58	7 11 39 15 57	syl13anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} (S \underset{˙}{\lor} T)))$
59	56 58	mpd	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} (S \underset{˙}{\lor} T))$
60	5 1 2	latlej2	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land T \in {Base}_{K}) \to T \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T)$
61	7 11 37 60	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T)$
62	5 1 2 3 4	atmod2i2	$⊢ (K \in HL \land (S \in A \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} T \in {Base}_{K} \land T \in {Base}_{K}) \land T \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} S) \underset{˙}{\lor} T = ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} (S \underset{˙}{\lor} T)$
63	6 12 39 37 61 62	syl131anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T) \underset{˙}{\land} S) \underset{˙}{\lor} T = ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} (S \underset{˙}{\lor} T)$
64	5 2 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land T \in A) \to Q \underset{˙}{\lor} T \in {Base}_{K}$
65	6 9 13 64	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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}$
66	5 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land S \in A) \to P \underset{˙}{\lor} S \in {Base}_{K}$
67	6 8 12 66	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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}$
68	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)$
69	7 65 67 68	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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)$
70		simp13	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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)$
71	69 70	eqbrtrd	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (R \underset{˙}{\lor} U)$
72	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}$
73	7 65 67 72	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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}$
74	5 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land U \in A) \to R \underset{˙}{\lor} U \in {Base}_{K}$
75	6 18 44 74	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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}$
76	5 1 2	latjlej2	$⊢ (K \in Lat \land ((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S) \in {Base}_{K} \land R \underset{˙}{\lor} U \in {Base}_{K} \land P \in {Base}_{K})) \to (((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\leq} (R \underset{˙}{\lor} U) \to (P \underset{˙}{\lor} ((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S))) \underset{˙}{\leq} (P \underset{˙}{\lor} (R \underset{˙}{\lor} U)))$
77	7 73 75 31 76	syl13anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (R \underset{˙}{\lor} U) \to (P \underset{˙}{\lor} ((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S))) \underset{˙}{\leq} (P \underset{˙}{\lor} (R \underset{˙}{\lor} U)))$
78	71 77	mpd	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S))) \underset{˙}{\leq} (P \underset{˙}{\lor} (R \underset{˙}{\lor} U))$
79	5 4	atbase	$⊢ S \in A \to S \in {Base}_{K}$
80	12 79	syl	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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}$
81	5 1 2	latlej1	$⊢ (K \in Lat \land P \in {Base}_{K} \land S \in {Base}_{K}) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} S)$
82	7 31 80 81	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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)$
83	5 1 2 3 4	atmod1i1	$⊢ (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 P \underset{˙}{\lor} ((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) = (P \underset{˙}{\lor} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} (P \underset{˙}{\lor} S)$
84	6 8 65 67 82 83	syl131anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) = (P \underset{˙}{\lor} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} (P \underset{˙}{\lor} S)$
85	2 4	hlatjass	$⊢ (K \in HL \land (P \in A \land R \in A \land U \in A)) \to (P \underset{˙}{\lor} R) \underset{˙}{\lor} U = P \underset{˙}{\lor} (R \underset{˙}{\lor} U)$
86	6 8 18 44 85	syl13anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} U = P \underset{˙}{\lor} (R \underset{˙}{\lor} U)$
87	2 4	hlatjcom	$⊢ (K \in HL \land P \in A \land R \in A) \to P \underset{˙}{\lor} R = R \underset{˙}{\lor} P$
88	6 8 18 87	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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 = R \underset{˙}{\lor} P$
89	88	oveq1d	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} U = (R \underset{˙}{\lor} P) \underset{˙}{\lor} U$
90	86 89	eqtr3d	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} U) = (R \underset{˙}{\lor} P) \underset{˙}{\lor} U$
91	78 84 90	3brtr3d	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T)) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\leq} ((R \underset{˙}{\lor} P) \underset{˙}{\lor} U)$
92	5 1 2	latlej2	$⊢ (K \in Lat \land U \in {Base}_{K} \land S \in {Base}_{K}) \to S \underset{˙}{\leq} (U \underset{˙}{\lor} S)$
93	7 50 80 92	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (U \underset{˙}{\lor} S)$
94	5 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \underset{˙}{\lor} T \in {Base}_{K}) \to P \underset{˙}{\lor} (Q \underset{˙}{\lor} T) \in {Base}_{K}$
95	7 31 65 94	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T) \in {Base}_{K}$
96	5 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} (Q \underset{˙}{\lor} T) \in {Base}_{K} \land P \underset{˙}{\lor} S \in {Base}_{K}) \to (P \underset{˙}{\lor} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} (P \underset{˙}{\lor} S) \in {Base}_{K}$
97	7 95 67 96	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T)) \underset{˙}{\land} (P \underset{˙}{\lor} S) \in {Base}_{K}$
98	5 2	latjcl	$⊢ (K \in Lat \land R \underset{˙}{\lor} P \in {Base}_{K} \land U \in {Base}_{K}) \to (R \underset{˙}{\lor} P) \underset{˙}{\lor} U \in {Base}_{K}$
99	7 43 50 98	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} U \in {Base}_{K}$
100	5 1 3	latmlem12	$⊢ (K \in Lat \land ((P \underset{˙}{\lor} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} (P \underset{˙}{\lor} S) \in {Base}_{K} \land (R \underset{˙}{\lor} P) \underset{˙}{\lor} U \in {Base}_{K}) \land (S \in {Base}_{K} \land U \underset{˙}{\lor} S \in {Base}_{K})) \to ((((P \underset{˙}{\lor} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\leq} ((R \underset{˙}{\lor} P) \underset{˙}{\lor} U) \land S \underset{˙}{\leq} (U \underset{˙}{\lor} S)) \to (((P \underset{˙}{\lor} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\land} S) \underset{˙}{\leq} (((R \underset{˙}{\lor} P) \underset{˙}{\lor} U) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$
101	7 97 99 80 46 100	syl122anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T)) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\leq} ((R \underset{˙}{\lor} P) \underset{˙}{\lor} U) \land S \underset{˙}{\leq} (U \underset{˙}{\lor} S)) \to (((P \underset{˙}{\lor} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\land} S) \underset{˙}{\leq} (((R \underset{˙}{\lor} P) \underset{˙}{\lor} U) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$
102	91 93 101	mp2and	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T)) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\land} S) \underset{˙}{\leq} (((R \underset{˙}{\lor} P) \underset{˙}{\lor} U) \underset{˙}{\land} (U \underset{˙}{\lor} S))$
103		hlol	$⊢ K \in HL \to K \in OL$
104	6 103	syl	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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 OL$
105	5 3	latmassOLD	$⊢ (K \in OL \land (P \underset{˙}{\lor} (Q \underset{˙}{\lor} T) \in {Base}_{K} \land P \underset{˙}{\lor} S \in {Base}_{K} \land S \in {Base}_{K})) \to ((P \underset{˙}{\lor} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\land} S = (P \underset{˙}{\lor} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} ((P \underset{˙}{\lor} S) \underset{˙}{\land} S)$
106	104 95 67 80 105	syl13anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T)) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\land} S = (P \underset{˙}{\lor} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} ((P \underset{˙}{\lor} S) \underset{˙}{\land} S)$
107	2 4	hlatjass	$⊢ (K \in HL \land (P \in A \land Q \in A \land T \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} T = P \underset{˙}{\lor} (Q \underset{˙}{\lor} T)$
108	6 8 9 13 107	syl13anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T = P \underset{˙}{\lor} (Q \underset{˙}{\lor} T)$
109	108	eqcomd	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} T$
110	5 1 2	latlej2	$⊢ (K \in Lat \land P \in {Base}_{K} \land S \in {Base}_{K}) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} S)$
111	7 31 80 110	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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)$
112	5 1 3	latleeqm2	$⊢ (K \in Lat \land S \in {Base}_{K} \land P \underset{˙}{\lor} S \in {Base}_{K}) \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} S) \leftrightarrow (P \underset{˙}{\lor} S) \underset{˙}{\land} S = S)$
113	7 80 67 112	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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) \leftrightarrow (P \underset{˙}{\lor} S) \underset{˙}{\land} S = S)$
114	111 113	mpbid	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} S = S$
115	109 114	oveq12d	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T)) \underset{˙}{\land} ((P \underset{˙}{\lor} S) \underset{˙}{\land} S) = ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} S$
116	106 115	eqtr2d	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T) \underset{˙}{\land} S = ((P \underset{˙}{\lor} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\land} S$
117	5 1 2	latlej1	$⊢ (K \in Lat \land U \in {Base}_{K} \land S \in {Base}_{K}) \to U \underset{˙}{\leq} (U \underset{˙}{\lor} S)$
118	7 50 80 117	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (U \underset{˙}{\lor} S)$
119	5 1 2 3 4	atmod4i1	$⊢ (K \in HL \land (U \in A \land R \underset{˙}{\lor} P \in {Base}_{K} \land U \underset{˙}{\lor} S \in {Base}_{K}) \land U \underset{˙}{\leq} (U \underset{˙}{\lor} S)) \to ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} U = ((R \underset{˙}{\lor} P) \underset{˙}{\lor} U) \underset{˙}{\land} (U \underset{˙}{\lor} S)$
120	6 44 43 46 118 119	syl131anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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)) \underset{˙}{\lor} U = ((R \underset{˙}{\lor} P) \underset{˙}{\lor} U) \underset{˙}{\land} (U \underset{˙}{\lor} S)$
121	102 116 120	3brtr4d	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T) \underset{˙}{\land} S) \underset{˙}{\leq} (((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} U)$
122	5 3	latmcl	$⊢ (K \in Lat \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} T \in {Base}_{K} \land S \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} S \in {Base}_{K}$
123	7 39 80 122	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T) \underset{˙}{\land} S \in {Base}_{K}$
124	5 1 2	latjlej1	$⊢ (K \in Lat \land (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} S \in {Base}_{K} \land ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} U \in {Base}_{K} \land T \in {Base}_{K})) \to ((((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} S) \underset{˙}{\leq} (((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} U) \to ((((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} S) \underset{˙}{\lor} T) \underset{˙}{\leq} ((((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} U) \underset{˙}{\lor} T))$
125	7 123 52 37 124	syl13anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T) \underset{˙}{\land} S) \underset{˙}{\leq} (((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} U) \to ((((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} S) \underset{˙}{\lor} T) \underset{˙}{\leq} ((((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} U) \underset{˙}{\lor} T))$
126	121 125	mpd	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T) \underset{˙}{\land} S) \underset{˙}{\lor} T) \underset{˙}{\leq} ((((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} U) \underset{˙}{\lor} T)$
127	63 126	eqbrtrrd	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\lor} T) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} ((((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} U) \underset{˙}{\lor} T)$
128	5 1 7 17 41 54 59 127	lattrd	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} ((((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} U) \underset{˙}{\lor} T)$
129	5 2	latj31	$⊢ (K \in Lat \land ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S) \in {Base}_{K} \land U \in {Base}_{K} \land T \in {Base}_{K})) \to (((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} U) \underset{˙}{\lor} T = (T \underset{˙}{\lor} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))$
130	7 48 50 37 129	syl13anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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)) \underset{˙}{\lor} U) \underset{˙}{\lor} T = (T \underset{˙}{\lor} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))$
131	128 130	breqtrd	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$
132	5 2 4	hlatjcl	$⊢ (K \in HL \land T \in A \land U \in A) \to T \underset{˙}{\lor} U \in {Base}_{K}$
133	6 13 44 132	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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}$
134	5 2	latjcl	$⊢ (K \in Lat \land T \underset{˙}{\lor} U \in {Base}_{K} \land (R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S) \in {Base}_{K}) \to (T \underset{˙}{\lor} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \in {Base}_{K}$
135	7 133 48 134	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \in {Base}_{K}$
136	5 1 3	latlem12	$⊢ (K \in Lat \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T) \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K} \land (T \underset{˙}{\lor} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \in {Base}_{K})) \to ((((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))))$
137	7 17 20 135 136	syl13anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))))$
138	35 131 137	mpbi2and	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))))$
139	5 1 3	latmle1	$⊢ (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)) \underset{˙}{\leq} (R \underset{˙}{\lor} P)$
140	7 43 46 139	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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)) \underset{˙}{\leq} (R \underset{˙}{\lor} P)$
141	5 1 2	latlej2	$⊢ (K \in Lat \land Q \in {Base}_{K} \land R \in {Base}_{K}) \to R \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
142	7 25 27 141	syl3anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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)$
143	5 1 2	latjle12	$⊢ (K \in Lat \land (R \in {Base}_{K} \land P \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K})) \to ((R \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow (R \underset{˙}{\lor} P) \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
144	7 27 31 20 143	syl13anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow (R \underset{˙}{\lor} P) \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
145	142 23 144	mpbi2and	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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{˙}{\leq} (Q \underset{˙}{\lor} R)$
146	5 1 7 48 43 20 140 145	lattrd	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
147	5 1 2 3 4	llnmod2i2	$⊢ ((K \in HL \land Q \underset{˙}{\lor} R \in {Base}_{K} \land (R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S) \in {Base}_{K}) \land (T \in A \land U \in A) \land ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) = (Q \underset{˙}{\lor} R) \underset{˙}{\land} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$
148	6 20 48 13 44 146 147	syl321anc	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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)) = (Q \underset{˙}{\lor} R) \underset{˙}{\land} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$
149	138 148	breqtrrd	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \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} (S \underset{˙}{\lor} T)) \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 dalawlem11

Proof