dalawlem2

Description: Lemma for dalaw . Utility lemma that breaks ( ( P .\/ Q ) ./\ ( S .\/ T ) ) into a join of two pieces. (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	dalawlem2	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} ((((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} S) \underset{˙}{\lor} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T))$

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		simp1	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to K \in HL$
6	5	hllatd	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to K \in Lat$
7		simp2l	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to P \in A$
8		simp2r	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to Q \in A$
9		eqid	$⊢ {Base}_{K} = {Base}_{K}$
10	9 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
11	5 7 8 10	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
12		simp3r	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to T \in A$
13	9 4	atbase	$⊢ T \in A \to T \in {Base}_{K}$
14	12 13	syl	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to T \in {Base}_{K}$
15	9 1 2	latlej1	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land T \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T)$
16	6 11 14 15	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T)$
17		simp3l	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to S \in A$
18	9 4	atbase	$⊢ S \in A \to S \in {Base}_{K}$
19	17 18	syl	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to S \in {Base}_{K}$
20	9 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)$
21	6 11 19 20	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)$
22	9 2	latjcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land T \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} T \in {Base}_{K}$
23	6 11 14 22	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} T \in {Base}_{K}$
24	9 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}$
25	6 11 19 24	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S \in {Base}_{K}$
26	9 1 3	latlem12	$⊢ (K \in Lat \land (P \underset{˙}{\lor} Q \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} T \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S \in {Base}_{K})) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \land (P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\leq} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)))$
27	6 11 23 25 26	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \land (P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\leq} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)))$
28	16 21 27	mpbi2and	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S))$
29	9 3	latmcl	$⊢ (K \in Lat \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} T \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \in {Base}_{K}$
30	6 23 25 29	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \in {Base}_{K}$
31	9 2 4	hlatjcl	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\lor} T \in {Base}_{K}$
32	5 17 12 31	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to S \underset{˙}{\lor} T \in {Base}_{K}$
33	9 1 3	latmlem1	$⊢ (K \in Lat \land (P \underset{˙}{\lor} Q \in {Base}_{K} \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \in {Base}_{K} \land S \underset{˙}{\lor} T \in {Base}_{K})) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\leq} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} ((((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)) \underset{˙}{\land} (S \underset{˙}{\lor} T)))$
34	6 11 30 32 33	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\leq} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} ((((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)) \underset{˙}{\land} (S \underset{˙}{\lor} T)))$
35	28 34	mpd	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} ((((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)) \underset{˙}{\land} (S \underset{˙}{\lor} T))$
36	9 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)$
37	6 11 19 36	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)$
38	9 1 2 3 4	atmod3i1	$⊢ (K \in HL \land (S \in A \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S \in {Base}_{K} \land T \in {Base}_{K}) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)) \to S \underset{˙}{\lor} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T) = ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} (S \underset{˙}{\lor} T)$
39	5 17 25 14 37 38	syl131anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to S \underset{˙}{\lor} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T) = ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} (S \underset{˙}{\lor} T)$
40	39	oveq2d	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} (S \underset{˙}{\lor} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T)) = ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} (S \underset{˙}{\lor} T))$
41	9 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}$
42	6 25 14 41	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T \in {Base}_{K}$
43	9 1 2 3	latmlej22	$⊢ (K \in Lat \land (T \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K})) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T)$
44	6 14 25 11 43	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T)$
45	9 1 2 3 4	atmod2i2	$⊢ (K \in HL \land (S \in A \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} T \in {Base}_{K} \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T \in {Base}_{K}) \land (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} S) \underset{˙}{\lor} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T) = ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} (S \underset{˙}{\lor} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T))$
46	5 17 23 42 44 45	syl131anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} S) \underset{˙}{\lor} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T) = ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} (S \underset{˙}{\lor} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T))$
47		hlol	$⊢ K \in HL \to K \in OL$
48	5 47	syl	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to K \in OL$
49	9 3	latmassOLD	$⊢ (K \in OL \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S \in {Base}_{K} \land S \underset{˙}{\lor} T \in {Base}_{K})) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)) \underset{˙}{\land} (S \underset{˙}{\lor} T) = ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} (S \underset{˙}{\lor} T))$
50	48 23 25 32 49	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)) \underset{˙}{\land} (S \underset{˙}{\lor} T) = ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} (S \underset{˙}{\lor} T))$
51	40 46 50	3eqtr4rd	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)) \underset{˙}{\land} (S \underset{˙}{\lor} T) = (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} S) \underset{˙}{\lor} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T)$
52	35 51	breqtrd	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (S \in A \land T \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} ((((P \underset{˙}{\lor} Q) \underset{˙}{\lor} T) \underset{˙}{\land} S) \underset{˙}{\lor} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S) \underset{˙}{\land} T))$

Metamath Proof Explorer

Theorem dalawlem2

Proof