Proof of Theorem pl42lem1N
Step | Hyp | Ref
| Expression |
1 | | simp11 1084 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → 𝐾 ∈ HL) |
2 | | hllat 33668 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → 𝐾 ∈ Lat) |
4 | | simp12 1085 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → 𝑋 ∈ 𝐵) |
5 | | simp13 1086 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → 𝑌 ∈ 𝐵) |
6 | | pl42lem.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐾) |
7 | | pl42lem.j |
. . . . . . . 8
⊢ ∨ =
(join‘𝐾) |
8 | 6, 7 | latjcl 16874 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵) |
9 | 3, 4, 5, 8 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → (𝑋 ∨ 𝑌) ∈ 𝐵) |
10 | | simp21 1087 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → 𝑍 ∈ 𝐵) |
11 | | pl42lem.m |
. . . . . . 7
⊢ ∧ =
(meet‘𝐾) |
12 | 6, 11 | latmcl 16875 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∨ 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 ∨ 𝑌) ∧ 𝑍) ∈ 𝐵) |
13 | 3, 9, 10, 12 | syl3anc 1318 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → ((𝑋 ∨ 𝑌) ∧ 𝑍) ∈ 𝐵) |
14 | | simp22 1088 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → 𝑊 ∈ 𝐵) |
15 | 6, 7 | latjcl 16874 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ ((𝑋 ∨ 𝑌) ∧ 𝑍) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∈ 𝐵) |
16 | 3, 13, 14, 15 | syl3anc 1318 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → (((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∈ 𝐵) |
17 | | simp23 1089 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → 𝑉 ∈ 𝐵) |
18 | | eqid 2610 |
. . . . 5
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
19 | | pl42lem.f |
. . . . 5
⊢ 𝐹 = (pmap‘𝐾) |
20 | 6, 11, 18, 19 | pmapmeet 34077 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉)) = ((𝐹‘(((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊)) ∩ (𝐹‘𝑉))) |
21 | 1, 16, 17, 20 | syl3anc 1318 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → (𝐹‘((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉)) = ((𝐹‘(((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊)) ∩ (𝐹‘𝑉))) |
22 | | pl42lem.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
23 | | hlop 33667 |
. . . . . . . . 9
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
24 | 1, 23 | syl 17 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → 𝐾 ∈ OP) |
25 | | pl42lem.o |
. . . . . . . . 9
⊢ ⊥ =
(oc‘𝐾) |
26 | 6, 25 | opoccl 33499 |
. . . . . . . 8
⊢ ((𝐾 ∈ OP ∧ 𝑊 ∈ 𝐵) → ( ⊥ ‘𝑊) ∈ 𝐵) |
27 | 24, 14, 26 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → ( ⊥ ‘𝑊) ∈ 𝐵) |
28 | 6, 22, 11 | latmle2 16900 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∨ 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 ∨ 𝑌) ∧ 𝑍) ≤ 𝑍) |
29 | 3, 9, 10, 28 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → ((𝑋 ∨ 𝑌) ∧ 𝑍) ≤ 𝑍) |
30 | | simp3r 1083 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → 𝑍 ≤ ( ⊥ ‘𝑊)) |
31 | 6, 22, 3, 13, 10, 27, 29, 30 | lattrd 16881 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → ((𝑋 ∨ 𝑌) ∧ 𝑍) ≤ ( ⊥ ‘𝑊)) |
32 | | pl42lem.p |
. . . . . . 7
⊢ + =
(+𝑃‘𝐾) |
33 | 6, 22, 7, 19, 25, 32 | pmapojoinN 34272 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ ((𝑋 ∨ 𝑌) ∧ 𝑍) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) ∧ ((𝑋 ∨ 𝑌) ∧ 𝑍) ≤ ( ⊥ ‘𝑊)) → (𝐹‘(((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊)) = ((𝐹‘((𝑋 ∨ 𝑌) ∧ 𝑍)) + (𝐹‘𝑊))) |
34 | 1, 13, 14, 31, 33 | syl31anc 1321 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → (𝐹‘(((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊)) = ((𝐹‘((𝑋 ∨ 𝑌) ∧ 𝑍)) + (𝐹‘𝑊))) |
35 | 6, 11, 18, 19 | pmapmeet 34077 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∨ 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐹‘((𝑋 ∨ 𝑌) ∧ 𝑍)) = ((𝐹‘(𝑋 ∨ 𝑌)) ∩ (𝐹‘𝑍))) |
36 | 1, 9, 10, 35 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → (𝐹‘((𝑋 ∨ 𝑌) ∧ 𝑍)) = ((𝐹‘(𝑋 ∨ 𝑌)) ∩ (𝐹‘𝑍))) |
37 | | simp3l 1082 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → 𝑋 ≤ ( ⊥ ‘𝑌)) |
38 | 6, 22, 7, 19, 25, 32 | pmapojoinN 34272 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → (𝐹‘(𝑋 ∨ 𝑌)) = ((𝐹‘𝑋) + (𝐹‘𝑌))) |
39 | 1, 4, 5, 37, 38 | syl31anc 1321 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → (𝐹‘(𝑋 ∨ 𝑌)) = ((𝐹‘𝑋) + (𝐹‘𝑌))) |
40 | 39 | ineq1d 3775 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → ((𝐹‘(𝑋 ∨ 𝑌)) ∩ (𝐹‘𝑍)) = (((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍))) |
41 | 36, 40 | eqtrd 2644 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → (𝐹‘((𝑋 ∨ 𝑌) ∧ 𝑍)) = (((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍))) |
42 | 41 | oveq1d 6564 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → ((𝐹‘((𝑋 ∨ 𝑌) ∧ 𝑍)) + (𝐹‘𝑊)) = ((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊))) |
43 | 34, 42 | eqtrd 2644 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → (𝐹‘(((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊)) = ((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊))) |
44 | 43 | ineq1d 3775 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → ((𝐹‘(((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊)) ∩ (𝐹‘𝑉)) = (((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊)) ∩ (𝐹‘𝑉))) |
45 | 21, 44 | eqtrd 2644 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) ∧ (𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊))) → (𝐹‘((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉)) = (((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊)) ∩ (𝐹‘𝑉))) |
46 | 45 | 3expia 1259 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊)) → (𝐹‘((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉)) = (((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊)) ∩ (𝐹‘𝑉)))) |