dalawlem7

Description: Lemma for dalaw . Second 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	dalawlem7	$⊢ ((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} S) \underset{˙}{\land} T) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$

Proof

Step	Hyp	Ref	Expression
1		dalawlem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dalawlem.j	$⊢ \underset{˙}{\lor} = join (K)$
3		dalawlem.m	$⊢ \underset{˙}{\land} = meet (K)$
4		dalawlem.a	$⊢ A = Atoms (K)$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6		simp11	$⊢ ((K \in HL \land ((P \underset{˙}{\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		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$
13	5 4	atbase	$⊢ S \in A \to S \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 S \in {Base}_{K}$
15	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}$
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} S \in {Base}_{K}$
17		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$
18	5 4	atbase	$⊢ T \in A \to T \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 T \in {Base}_{K}$
20	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}$
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} S) \underset{˙}{\land} T \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 2 4	hlatjcl	$⊢ (K \in HL \land T \in A \land U \in A) \to T \underset{˙}{\lor} U \in {Base}_{K}$
27	6 17 25 26	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}$
28	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}$
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} (T \underset{˙}{\lor} 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 12 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} (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}$
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} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \in {Base}_{K}$
38		hlol	$⊢ K \in HL \to K \in OL$
39	6 38	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$
40	5 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land S \in A) \to P \underset{˙}{\lor} S \in {Base}_{K}$
41	6 8 12 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 P \underset{˙}{\lor} S \in {Base}_{K}$
42	5 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
43	9 42	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 Q \in {Base}_{K}$
44	5 2	latjcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} S \in {Base}_{K} \land Q \in {Base}_{K}) \to (P \underset{˙}{\lor} S) \underset{˙}{\lor} Q \in {Base}_{K}$
45	7 41 43 44	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{˙}{\lor} Q \in {Base}_{K}$
46	5 2 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land T \in A) \to Q \underset{˙}{\lor} T \in {Base}_{K}$
47	6 9 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 Q \underset{˙}{\lor} T \in {Base}_{K}$
48	5 3	latmassOLD	$⊢ (K \in OL \land ((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q \in {Base}_{K} \land Q \underset{˙}{\lor} T \in {Base}_{K} \land T \in {Base}_{K})) \to (((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} T = ((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q) \underset{˙}{\land} ((Q \underset{˙}{\lor} T) \underset{˙}{\land} T)$
49	39 45 47 19 48	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{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} T = ((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q) \underset{˙}{\land} ((Q \underset{˙}{\lor} T) \underset{˙}{\land} T)$
50	2 4	hlatj32	$⊢ (K \in HL \land (P \in A \land S \in A \land Q \in A)) \to (P \underset{˙}{\lor} S) \underset{˙}{\lor} Q = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S$
51	6 8 12 9 50	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{˙}{\lor} Q = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S$
52	1 2 4	hlatlej2	$⊢ (K \in HL \land Q \in A \land T \in A) \to T \underset{˙}{\leq} (Q \underset{˙}{\lor} T)$
53	6 9 17 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 T \underset{˙}{\leq} (Q \underset{˙}{\lor} T)$
54	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)$
55	7 19 47 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 (T \underset{˙}{\leq} (Q \underset{˙}{\lor} T) \leftrightarrow (Q \underset{˙}{\lor} T) \underset{˙}{\land} T = T)$
56	53 55	mpbid	$⊢ ((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} T = T$
57	51 56	oveq12d	$⊢ ((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{˙}{\lor} Q) \underset{˙}{\land} ((Q \underset{˙}{\lor} T) \underset{˙}{\land} T) = ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T$
58	49 57	eqtr2d	$⊢ ((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} S) \underset{˙}{\land} T = (((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} T$
59		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)$
60	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}$
61	7 41 47 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} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T) \in {Base}_{K}$
62	5 1 2	latjlej1	$⊢ (K \in Lat \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T) \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K} \land Q \in {Base}_{K})) \to (((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \to (((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\lor} Q) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} Q))$
63	7 61 24 43 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} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \to (((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\lor} Q) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} Q))$
64	59 63	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} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\lor} Q) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} Q)$
65	1 2 4	hlatlej1	$⊢ (K \in HL \land Q \in A \land T \in A) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} T)$
66	6 9 17 65	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{˙}{\leq} (Q \underset{˙}{\lor} T)$
67	5 1 2 3 4	atmod4i1	$⊢ (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 ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\lor} Q = ((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} T)$
68	6 9 41 47 66 67	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} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\lor} Q = ((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} T)$
69	2 4	hlatj32	$⊢ (K \in HL \land (Q \in A \land R \in A \land Q \in A)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} Q = (Q \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
70	6 9 22 9 69	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{˙}{\lor} Q = (Q \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
71	5 2	latjidm	$⊢ (K \in Lat \land Q \in {Base}_{K}) \to Q \underset{˙}{\lor} Q = Q$
72	7 43 71	syl2anc	$⊢ ((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} Q = Q$
73	72	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 (Q \underset{˙}{\lor} Q) \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
74	70 73	eqtrd	$⊢ ((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{˙}{\lor} Q = Q \underset{˙}{\lor} R$
75	64 68 74	3brtr3d	$⊢ ((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{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
76	1 2 4	hlatlej1	$⊢ (K \in HL \land T \in A \land U \in A) \to T \underset{˙}{\leq} (T \underset{˙}{\lor} U)$
77	6 17 25 76	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{˙}{\leq} (T \underset{˙}{\lor} U)$
78	5 3	latmcl	$⊢ (K \in Lat \land (P \underset{˙}{\lor} S) \underset{˙}{\lor} Q \in {Base}_{K} \land Q \underset{˙}{\lor} T \in {Base}_{K}) \to ((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} T) \in {Base}_{K}$
79	7 45 47 78	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{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} T) \in {Base}_{K}$
80	5 1 3	latmlem12	$⊢ (K \in Lat \land (((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} T) \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K}) \land (T \in {Base}_{K} \land T \underset{˙}{\lor} U \in {Base}_{K})) \to (((((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land T \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to ((((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} T) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)))$
81	7 79 24 19 27 80	syl122anc	$⊢ ((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{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land T \underset{˙}{\leq} (T \underset{˙}{\lor} U)) \to ((((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} T) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)))$
82	75 77 81	mp2and	$⊢ ((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{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\land} T) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U))$
83	58 82	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 (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U))$
84	5 1 2	latlej1	$⊢ (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{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$
85	7 29 35 84	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{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$
86	5 1 7 21 29 37 83 85	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} S) \underset{˙}{\land} 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 dalawlem7

Proof