Proof of Theorem dihmeetlem3N
Step | Hyp | Ref
| Expression |
1 | | simp2lr 1122 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → ¬ 𝑄 ≤ 𝑊) |
2 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑄 = 𝑅 → (𝑄 ∨ (𝑌 ∧ 𝑊)) = (𝑅 ∨ (𝑌 ∧ 𝑊))) |
3 | | simpr 476 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌) |
4 | 2, 3 | sylan9eqr 2666 |
. . . . . 6
⊢ ((((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌) ∧ 𝑄 = 𝑅) → (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) |
5 | | dihmeetlem3.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐾) |
6 | | dihmeetlem3.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝐾) |
7 | | simp11l 1165 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝐾 ∈ HL) |
8 | | hllat 33668 |
. . . . . . . . 9
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
9 | 7, 8 | syl 17 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝐾 ∈ Lat) |
10 | | simp2ll 1121 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ∈ 𝐴) |
11 | | dihmeetlem3.a |
. . . . . . . . . 10
⊢ 𝐴 = (Atoms‘𝐾) |
12 | 5, 11 | atbase 33594 |
. . . . . . . . 9
⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵) |
13 | 10, 12 | syl 17 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ∈ 𝐵) |
14 | | simp12l 1167 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑋 ∈ 𝐵) |
15 | | simp12r 1168 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑌 ∈ 𝐵) |
16 | | dihmeetlem3.m |
. . . . . . . . . 10
⊢ ∧ =
(meet‘𝐾) |
17 | 5, 16 | latmcl 16875 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵) |
18 | 9, 14, 15, 17 | syl3anc 1318 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑋 ∧ 𝑌) ∈ 𝐵) |
19 | | simp11r 1166 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑊 ∈ 𝐻) |
20 | | dihmeetlem3.h |
. . . . . . . . . 10
⊢ 𝐻 = (LHyp‘𝐾) |
21 | 5, 20 | lhpbase 34302 |
. . . . . . . . 9
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
22 | 19, 21 | syl 17 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑊 ∈ 𝐵) |
23 | 5, 16 | latmcl 16875 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵) |
24 | 9, 14, 22, 23 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑋 ∧ 𝑊) ∈ 𝐵) |
25 | | dihmeetlem3.j |
. . . . . . . . . . . 12
⊢ ∨ =
(join‘𝐾) |
26 | 5, 6, 25 | latlej1 16883 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ∈ 𝐵) → 𝑄 ≤ (𝑄 ∨ (𝑋 ∧ 𝑊))) |
27 | 9, 13, 24, 26 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ≤ (𝑄 ∨ (𝑋 ∧ 𝑊))) |
28 | | simp2r 1081 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) |
29 | 27, 28 | breqtrd 4609 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ≤ 𝑋) |
30 | 5, 16 | latmcl 16875 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑌 ∧ 𝑊) ∈ 𝐵) |
31 | 9, 15, 22, 30 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑌 ∧ 𝑊) ∈ 𝐵) |
32 | 5, 6, 25 | latlej1 16883 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ (𝑌 ∧ 𝑊) ∈ 𝐵) → 𝑄 ≤ (𝑄 ∨ (𝑌 ∧ 𝑊))) |
33 | 9, 13, 31, 32 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ≤ (𝑄 ∨ (𝑌 ∧ 𝑊))) |
34 | | simp3 1056 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) |
35 | 33, 34 | breqtrd 4609 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ≤ 𝑌) |
36 | 5, 6, 16 | latlem12 16901 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑄 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌) ↔ 𝑄 ≤ (𝑋 ∧ 𝑌))) |
37 | 9, 13, 14, 15, 36 | syl13anc 1320 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → ((𝑄 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌) ↔ 𝑄 ≤ (𝑋 ∧ 𝑌))) |
38 | 29, 35, 37 | mpbi2and 958 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ≤ (𝑋 ∧ 𝑌)) |
39 | | simp13 1086 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑋 ∧ 𝑌) ≤ 𝑊) |
40 | 5, 6, 9, 13, 18, 22, 38, 39 | lattrd 16881 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ≤ 𝑊) |
41 | 40 | 3exp 1256 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) → (((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → ((𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌 → 𝑄 ≤ 𝑊))) |
42 | 4, 41 | syl7 72 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) → (((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → ((((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌) ∧ 𝑄 = 𝑅) → 𝑄 ≤ 𝑊))) |
43 | 42 | exp4a 631 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) → (((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → (((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑄 = 𝑅 → 𝑄 ≤ 𝑊)))) |
44 | 43 | 3imp 1249 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝑄 = 𝑅 → 𝑄 ≤ 𝑊)) |
45 | 44 | necon3bd 2796 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (¬ 𝑄 ≤ 𝑊 → 𝑄 ≠ 𝑅)) |
46 | 1, 45 | mpd 15 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝑄 ≠ 𝑅) |