dalawlem9

Description: Lemma for dalaw . Special case to eliminate the requirement -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ P ) in dalawlem1 . (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	dalawlem9	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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		simp11	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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	5	hllatd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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$
7		simp22	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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$
8		simp32	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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$
9		eqid	$⊢ {Base}_{K} = {Base}_{K}$
10	9 2 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land T \in A) \to Q \underset{˙}{\lor} T \in {Base}_{K}$
11	5 7 8 10	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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}$
12		simp21	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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$
13		simp31	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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$
14	9 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land S \in A) \to P \underset{˙}{\lor} S \in {Base}_{K}$
15	5 12 13 14	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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}$
16	9 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)$
17	6 11 15 16	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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)$
18		simp12	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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} P)$
19		simp23	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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$
20	2 4	hlatjcom	$⊢ (K \in HL \land R \in A \land P \in A) \to R \underset{˙}{\lor} P = P \underset{˙}{\lor} R$
21	5 19 12 20	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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 = P \underset{˙}{\lor} R$
22	18 21	breqtrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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} R)$
23	17 22	eqbrtrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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} (P \underset{˙}{\lor} R)$
24		simp13	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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)$
25	17 24	eqbrtrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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)$
26		simp33	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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$
27	1 2 3 4	dalawlem8	$⊢ ((K \in HL \land ((Q \underset{˙}{\lor} T) \underset{˙}{\land} (P \underset{˙}{\lor} S)) \underset{˙}{\leq} (P \underset{˙}{\lor} R) \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 ((Q \underset{˙}{\lor} P) \underset{˙}{\land} (T \underset{˙}{\lor} S)) \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	5 23 25 7 12 19 8 13 26 27	syl333anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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{˙}{\land} (T \underset{˙}{\lor} S)) \underset{˙}{\leq} (((P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} Q) \underset{˙}{\land} (U \underset{˙}{\lor} T)))$
29	2 4	hlatjcom	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
30	5 12 7 29	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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$
31	2 4	hlatjcom	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\lor} T = T \underset{˙}{\lor} S$
32	5 13 8 31	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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$
33	30 32	oveq12d	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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) = (Q \underset{˙}{\lor} P) \underset{˙}{\land} (T \underset{˙}{\lor} S)$
34	9 2 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
35	5 7 19 34	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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}$
36	9 2 4	hlatjcl	$⊢ (K \in HL \land T \in A \land U \in A) \to T \underset{˙}{\lor} U \in {Base}_{K}$
37	5 8 26 36	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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}$
38	9 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}$
39	6 35 37 38	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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}$
40	9 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land P \in A) \to R \underset{˙}{\lor} P \in {Base}_{K}$
41	5 19 12 40	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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}$
42	9 2 4	hlatjcl	$⊢ (K \in HL \land U \in A \land S \in A) \to U \underset{˙}{\lor} S \in {Base}_{K}$
43	5 26 13 42	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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}$
44	9 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}$
45	6 41 43 44	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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}$
46	9 2	latjcom	$⊢ (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)) = ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U))$
47	6 39 45 46	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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)) = ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)) \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U))$
48	2 4	hlatjcom	$⊢ (K \in HL \land U \in A \land S \in A) \to U \underset{˙}{\lor} S = S \underset{˙}{\lor} U$
49	5 26 13 48	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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 = S \underset{˙}{\lor} U$
50	21 49	oveq12d	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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) = (P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} U)$
51	2 4	hlatjcom	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\lor} R = R \underset{˙}{\lor} Q$
52	5 7 19 51	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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 = R \underset{˙}{\lor} Q$
53	2 4	hlatjcom	$⊢ (K \in HL \land T \in A \land U \in A) \to T \underset{˙}{\lor} U = U \underset{˙}{\lor} T$
54	5 8 26 53	syl3anc	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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 = U \underset{˙}{\lor} T$
55	52 54	oveq12d	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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) = (R \underset{˙}{\lor} Q) \underset{˙}{\land} (U \underset{˙}{\lor} T)$
56	50 55	oveq12d	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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)) = ((P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} Q) \underset{˙}{\land} (U \underset{˙}{\lor} T))$
57	47 56	eqtrd	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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)) = ((P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} Q) \underset{˙}{\land} (U \underset{˙}{\lor} T))$
58	28 33 57	3brtr4d	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (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 dalawlem9

Proof