dalawlem12

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

Proof