dalawlem4

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

	Ref	Expression
Hypotheses	dalawlem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dalawlem.j	$⊢ \underset{˙}{\lor} = join (K)$
	dalawlem.m	$⊢ \underset{˙}{\land} = meet (K)$
	dalawlem.a	$⊢ A = Atoms (K)$
Assertion	dalawlem4	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q) \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		simp11	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to K \in HL$
6		simp12	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
7	5	hllatd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to K \in Lat$
8		simp22	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to Q \in A$
9		simp32	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to T \in A$
10		eqid	$⊢ {Base}_{K} = {Base}_{K}$
11	10 2 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land T \in A) \to Q \underset{˙}{\lor} T \in {Base}_{K}$
12	5 8 9 11	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to Q \underset{˙}{\lor} T \in {Base}_{K}$
13		simp21	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to P \in A$
14		simp31	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to S \in A$
15	10 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land S \in A) \to P \underset{˙}{\lor} S \in {Base}_{K}$
16	5 13 14 15	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to P \underset{˙}{\lor} S \in {Base}_{K}$
17	10 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)$
18	7 12 16 17	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S) = (P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)$
19	2 4	hlatjcom	$⊢ (K \in HL \land Q \in A \land P \in A) \to Q \underset{˙}{\lor} P = P \underset{˙}{\lor} Q$
20	5 8 13 19	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to Q \underset{˙}{\lor} P = P \underset{˙}{\lor} Q$
21	6 18 20	3brtr4d	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\leq} (Q \underset{˙}{\lor} P)$
22		simp13	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
23	18 22	eqbrtrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
24		simp23	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to R \in A$
25		simp33	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to U \in A$
26	1 2 3 4	dalawlem3	$⊢ ((K \in HL \land ((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\leq} (Q \underset{˙}{\lor} P) \land ((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (Q \in A \land P \in A \land R \in A) \land (T \in A \land S \in A \land U \in A)) \to (((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q) \underset{˙}{\land} T) \underset{˙}{\leq} (((P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} Q) \underset{˙}{\land} (U \underset{˙}{\lor} T)))$
27	5 21 23 8 13 24 9 14 25 26	syl333anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q) \underset{˙}{\land} T) \underset{˙}{\leq} (((P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} Q) \underset{˙}{\land} (U \underset{˙}{\lor} T)))$
28	2 4	hlatjcom	$⊢ (K \in HL \land P \in A \land R \in A) \to P \underset{˙}{\lor} R = R \underset{˙}{\lor} P$
29	5 13 24 28	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to P \underset{˙}{\lor} R = R \underset{˙}{\lor} P$
30	2 4	hlatjcom	$⊢ (K \in HL \land S \in A \land U \in A) \to S \underset{˙}{\lor} U = U \underset{˙}{\lor} S$
31	5 14 25 30	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to S \underset{˙}{\lor} U = U \underset{˙}{\lor} S$
32	29 31	oveq12d	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} U) = (R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)$
33	2 4	hlatjcom	$⊢ (K \in HL \land R \in A \land Q \in A) \to R \underset{˙}{\lor} Q = Q \underset{˙}{\lor} R$
34	5 24 8 33	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to R \underset{˙}{\lor} Q = Q \underset{˙}{\lor} R$
35	2 4	hlatjcom	$⊢ (K \in HL \land U \in A \land T \in A) \to U \underset{˙}{\lor} T = T \underset{˙}{\lor} U$
36	5 25 9 35	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to U \underset{˙}{\lor} T = T \underset{˙}{\lor} U$
37	34 36	oveq12d	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (R \underset{˙}{\lor} Q) \underset{˙}{\land} (U \underset{˙}{\lor} T) = (Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)$
38	32 37	oveq12d	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} Q) \underset{˙}{\land} (U \underset{˙}{\lor} T)) = ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U))$
39	10 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land P \in A) \to R \underset{˙}{\lor} P \in {Base}_{K}$
40	5 24 13 39	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to R \underset{˙}{\lor} P \in {Base}_{K}$
41	10 2 4	hlatjcl	$⊢ (K \in HL \land U \in A \land S \in A) \to U \underset{˙}{\lor} S \in {Base}_{K}$
42	5 25 14 41	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to U \underset{˙}{\lor} S \in {Base}_{K}$
43	10 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}$
44	7 40 42 43	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S) \in {Base}_{K}$
45	10 2 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
46	5 8 24 45	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
47	10 2 4	hlatjcl	$⊢ (K \in HL \land T \in A \land U \in A) \to T \underset{˙}{\lor} U \in {Base}_{K}$
48	5 9 25 47	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to T \underset{˙}{\lor} U \in {Base}_{K}$
49	10 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}$
50	7 46 48 49	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U) \in {Base}_{K}$
51	10 2	latjcom	$⊢ (K \in Lat \land (R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S) \in {Base}_{K} \land (Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U) \in {Base}_{K}) \to ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) = ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))$
52	7 44 50 51	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) = ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))$
53	38 52	eqtrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} Q) \underset{˙}{\land} (U \underset{˙}{\lor} T)) = ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))$
54	27 53	breqtrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q) \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 dalawlem4

Proof