Metamath Proof Explorer

Theorem 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 ⊢ ≤ ˙ = ≤ K
dalawlem.j ⊢ ∨ ˙ = join ⁡ K
dalawlem.m ⊢ ∧ ˙ = meet ⁡ K
dalawlem.a ⊢ A = Atoms ⁡ K
Assertion dalawlem2 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ∧ ˙ S ∨ ˙ T ≤ ˙ P ∨ ˙ Q ∨ ˙ T ∧ ˙ S ∨ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ T

Proof

Step Hyp Ref Expression
1 dalawlem.l ⊢ ≤ ˙ = ≤ K
2 dalawlem.j ⊢ ∨ ˙ = join ⁡ K
3 dalawlem.m ⊢ ∧ ˙ = meet ⁡ K
4 dalawlem.a ⊢ A = Atoms ⁡ K
5 simp1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → K ∈ HL
6 5 hllatd ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → K ∈ Lat
7 simp2l ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∈ A
8 simp2r ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → Q ∈ A
9 eqid ⊢ Base K = Base K
10 9 2 4 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ Base K
11 5 7 8 10 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ∈ Base K
12 simp3r ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → T ∈ A
13 9 4 atbase ⊢ T ∈ A → T ∈ Base K
14 12 13 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → T ∈ Base K
15 9 1 2 latlej1 ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ T ∈ Base K → P ∨ ˙ Q ≤ ˙ P ∨ ˙ Q ∨ ˙ T
16 6 11 14 15 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ≤ ˙ P ∨ ˙ Q ∨ ˙ T
17 simp3l ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → S ∈ A
18 9 4 atbase ⊢ S ∈ A → S ∈ Base K
19 17 18 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → S ∈ Base K
20 9 1 2 latlej1 ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ S ∈ Base K → P ∨ ˙ Q ≤ ˙ P ∨ ˙ Q ∨ ˙ S
21 6 11 19 20 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ≤ ˙ P ∨ ˙ Q ∨ ˙ S
22 9 2 latjcl ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ T ∈ Base K → P ∨ ˙ Q ∨ ˙ T ∈ Base K
23 6 11 14 22 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ∨ ˙ T ∈ Base K
24 9 2 latjcl ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ S ∈ Base K → P ∨ ˙ Q ∨ ˙ S ∈ Base K
25 6 11 19 24 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ∨ ˙ S ∈ Base K
26 9 1 3 latlem12 ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ P ∨ ˙ Q ∨ ˙ T ∈ Base K ∧ P ∨ ˙ Q ∨ ˙ S ∈ Base K → P ∨ ˙ Q ≤ ˙ P ∨ ˙ Q ∨ ˙ T ∧ P ∨ ˙ Q ≤ ˙ P ∨ ˙ Q ∨ ˙ S ↔ P ∨ ˙ Q ≤ ˙ P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S
27 6 11 23 25 26 syl13anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ≤ ˙ P ∨ ˙ Q ∨ ˙ T ∧ P ∨ ˙ Q ≤ ˙ P ∨ ˙ Q ∨ ˙ S ↔ P ∨ ˙ Q ≤ ˙ P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S
28 16 21 27 mpbi2and ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ≤ ˙ P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S
29 9 3 latmcl ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∨ ˙ T ∈ Base K ∧ P ∨ ˙ Q ∨ ˙ S ∈ Base K → P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S ∈ Base K
30 6 23 25 29 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S ∈ Base K
31 9 2 4 hlatjcl ⊢ K ∈ HL ∧ S ∈ A ∧ T ∈ A → S ∨ ˙ T ∈ Base K
32 5 17 12 31 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → S ∨ ˙ T ∈ Base K
33 9 1 3 latmlem1 ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S ∈ Base K ∧ S ∨ ˙ T ∈ Base K → P ∨ ˙ Q ≤ ˙ P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S → P ∨ ˙ Q ∧ ˙ S ∨ ˙ T ≤ ˙ P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ S ∨ ˙ T
34 6 11 30 32 33 syl13anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ≤ ˙ P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S → P ∨ ˙ Q ∧ ˙ S ∨ ˙ T ≤ ˙ P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ S ∨ ˙ T
35 28 34 mpd ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ∧ ˙ S ∨ ˙ T ≤ ˙ P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ S ∨ ˙ T
36 9 1 2 latlej2 ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ S ∈ Base K → S ≤ ˙ P ∨ ˙ Q ∨ ˙ S
37 6 11 19 36 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → S ≤ ˙ P ∨ ˙ Q ∨ ˙ S
38 9 1 2 3 4 atmod3i1 ⊢ K ∈ HL ∧ S ∈ A ∧ P ∨ ˙ Q ∨ ˙ S ∈ Base K ∧ T ∈ Base K ∧ S ≤ ˙ P ∨ ˙ Q ∨ ˙ S → S ∨ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ T = P ∨ ˙ Q ∨ ˙ S ∧ ˙ S ∨ ˙ T
39 5 17 25 14 37 38 syl131anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → S ∨ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ T = P ∨ ˙ Q ∨ ˙ S ∧ ˙ S ∨ ˙ T
40 39 oveq2d ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ∨ ˙ T ∧ ˙ S ∨ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ T = P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ S ∨ ˙ T
41 9 3 latmcl ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∨ ˙ S ∈ Base K ∧ T ∈ Base K → P ∨ ˙ Q ∨ ˙ S ∧ ˙ T ∈ Base K
42 6 25 14 41 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ∨ ˙ S ∧ ˙ T ∈ Base K
43 9 1 2 3 latmlej22 ⊢ K ∈ Lat ∧ T ∈ Base K ∧ P ∨ ˙ Q ∨ ˙ S ∈ Base K ∧ P ∨ ˙ Q ∈ Base K → P ∨ ˙ Q ∨ ˙ S ∧ ˙ T ≤ ˙ P ∨ ˙ Q ∨ ˙ T
44 6 14 25 11 43 syl13anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ∨ ˙ S ∧ ˙ T ≤ ˙ P ∨ ˙ Q ∨ ˙ T
45 9 1 2 3 4 atmod2i2 ⊢ K ∈ HL ∧ S ∈ A ∧ P ∨ ˙ Q ∨ ˙ T ∈ Base K ∧ P ∨ ˙ Q ∨ ˙ S ∧ ˙ T ∈ Base K ∧ P ∨ ˙ Q ∨ ˙ S ∧ ˙ T ≤ ˙ P ∨ ˙ Q ∨ ˙ T → P ∨ ˙ Q ∨ ˙ T ∧ ˙ S ∨ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ T = P ∨ ˙ Q ∨ ˙ T ∧ ˙ S ∨ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ T
46 5 17 23 42 44 45 syl131anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ∨ ˙ T ∧ ˙ S ∨ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ T = P ∨ ˙ Q ∨ ˙ T ∧ ˙ S ∨ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ T
47 hlol ⊢ K ∈ HL → K ∈ OL
48 5 47 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → K ∈ OL
49 9 3 latmassOLD ⊢ K ∈ OL ∧ P ∨ ˙ Q ∨ ˙ T ∈ Base K ∧ P ∨ ˙ Q ∨ ˙ S ∈ Base K ∧ S ∨ ˙ T ∈ Base K → P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ S ∨ ˙ T = P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ S ∨ ˙ T
50 48 23 25 32 49 syl13anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ S ∨ ˙ T = P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ S ∨ ˙ T
51 40 46 50 3eqtr4rd ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ∨ ˙ T ∧ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ S ∨ ˙ T = P ∨ ˙ Q ∨ ˙ T ∧ ˙ S ∨ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ T
52 35 51 breqtrd ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ T ∈ A → P ∨ ˙ Q ∧ ˙ S ∨ ˙ T ≤ ˙ P ∨ ˙ Q ∨ ˙ T ∧ ˙ S ∨ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ T