dalawlem6

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

Proof