Proof of Theorem dihmeetlem7N
Step | Hyp | Ref
| Expression |
1 | | simprr 796 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → ¬ 𝑝 ≤ 𝑌) |
2 | | simpl1 1064 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → 𝐾 ∈ HL) |
3 | | hlatl 34647 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → 𝐾 ∈ AtLat) |
5 | | simprl 794 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → 𝑝 ∈ 𝐴) |
6 | | simpl3 1066 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → 𝑌 ∈ 𝐵) |
7 | | dihmeetlem7.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
8 | | dihmeetlem7.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
9 | | dihmeetlem7.m |
. . . . . 6
⊢ ∧ =
(meet‘𝐾) |
10 | | eqid 2622 |
. . . . . 6
⊢
(0.‘𝐾) =
(0.‘𝐾) |
11 | | dihmeetlem7.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
12 | 7, 8, 9, 10, 11 | atnle 34604 |
. . . . 5
⊢ ((𝐾 ∈ AtLat ∧ 𝑝 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (¬ 𝑝 ≤ 𝑌 ↔ (𝑝 ∧ 𝑌) = (0.‘𝐾))) |
13 | 4, 5, 6, 12 | syl3anc 1326 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → (¬ 𝑝 ≤ 𝑌 ↔ (𝑝 ∧ 𝑌) = (0.‘𝐾))) |
14 | 1, 13 | mpbid 222 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → (𝑝 ∧ 𝑌) = (0.‘𝐾)) |
15 | 14 | oveq2d 6666 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → ((𝑋 ∧ 𝑌) ∨ (𝑝 ∧ 𝑌)) = ((𝑋 ∧ 𝑌) ∨ (0.‘𝐾))) |
16 | | hllat 34650 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
17 | 2, 16 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → 𝐾 ∈ Lat) |
18 | | simpl2 1065 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → 𝑋 ∈ 𝐵) |
19 | 7, 9 | latmcl 17052 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵) |
20 | 17, 18, 6, 19 | syl3anc 1326 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → (𝑋 ∧ 𝑌) ∈ 𝐵) |
21 | 7, 8, 9 | latmle2 17077 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌) |
22 | 17, 18, 6, 21 | syl3anc 1326 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → (𝑋 ∧ 𝑌) ≤ 𝑌) |
23 | | dihmeetlem7.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
24 | 7, 8, 23, 9, 11 | atmod1i2 35145 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑝 ∈ 𝐴 ∧ (𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑌) → ((𝑋 ∧ 𝑌) ∨ (𝑝 ∧ 𝑌)) = (((𝑋 ∧ 𝑌) ∨ 𝑝) ∧ 𝑌)) |
25 | 2, 5, 20, 6, 22, 24 | syl131anc 1339 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → ((𝑋 ∧ 𝑌) ∨ (𝑝 ∧ 𝑌)) = (((𝑋 ∧ 𝑌) ∨ 𝑝) ∧ 𝑌)) |
26 | | hlol 34648 |
. . . 4
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
27 | 2, 26 | syl 17 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → 𝐾 ∈ OL) |
28 | 7, 23, 10 | olj01 34512 |
. . 3
⊢ ((𝐾 ∈ OL ∧ (𝑋 ∧ 𝑌) ∈ 𝐵) → ((𝑋 ∧ 𝑌) ∨ (0.‘𝐾)) = (𝑋 ∧ 𝑌)) |
29 | 27, 20, 28 | syl2anc 693 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → ((𝑋 ∧ 𝑌) ∨ (0.‘𝐾)) = (𝑋 ∧ 𝑌)) |
30 | 15, 25, 29 | 3eqtr3d 2664 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → (((𝑋 ∧ 𝑌) ∨ 𝑝) ∧ 𝑌) = (𝑋 ∧ 𝑌)) |