Proof of Theorem lhple
Step | Hyp | Ref
| Expression |
1 | | simp1l 1085 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → 𝐾 ∈ HL) |
2 | | hllat 34650 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → 𝐾 ∈ Lat) |
4 | | simp2l 1087 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → 𝑃 ∈ 𝐴) |
5 | | lhple.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
6 | | lhple.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
7 | 5, 6 | atbase 34576 |
. . . . 5
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵) |
8 | 4, 7 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → 𝑃 ∈ 𝐵) |
9 | | simp3l 1089 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → 𝑋 ∈ 𝐵) |
10 | | lhple.j |
. . . . 5
⊢ ∨ =
(join‘𝐾) |
11 | 5, 10 | latjcom 17059 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑃 ∨ 𝑋) = (𝑋 ∨ 𝑃)) |
12 | 3, 8, 9, 11 | syl3anc 1326 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑃 ∨ 𝑋) = (𝑋 ∨ 𝑃)) |
13 | 12 | oveq1d 6665 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → ((𝑃 ∨ 𝑋) ∧ 𝑊) = ((𝑋 ∨ 𝑃) ∧ 𝑊)) |
14 | | simp1 1061 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
15 | | simp3r 1090 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → 𝑋 ≤ 𝑊) |
16 | | lhple.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
17 | | lhple.m |
. . . 4
⊢ ∧ =
(meet‘𝐾) |
18 | | lhple.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
19 | 5, 16, 10, 17, 18 | lhpmod6i1 35325 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ 𝑋 ≤ 𝑊) → (𝑋 ∨ (𝑃 ∧ 𝑊)) = ((𝑋 ∨ 𝑃) ∧ 𝑊)) |
20 | 14, 9, 8, 15, 19 | syl121anc 1331 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑋 ∨ (𝑃 ∧ 𝑊)) = ((𝑋 ∨ 𝑃) ∧ 𝑊)) |
21 | | eqid 2622 |
. . . . . 6
⊢
(0.‘𝐾) =
(0.‘𝐾) |
22 | 16, 17, 21, 6, 18 | lhpmat 35316 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∧ 𝑊) = (0.‘𝐾)) |
23 | 22 | 3adant3 1081 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑃 ∧ 𝑊) = (0.‘𝐾)) |
24 | 23 | oveq2d 6666 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑋 ∨ (𝑃 ∧ 𝑊)) = (𝑋 ∨ (0.‘𝐾))) |
25 | | hlol 34648 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
26 | 1, 25 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → 𝐾 ∈ OL) |
27 | 5, 10, 21 | olj01 34512 |
. . . 4
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ (0.‘𝐾)) = 𝑋) |
28 | 26, 9, 27 | syl2anc 693 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑋 ∨ (0.‘𝐾)) = 𝑋) |
29 | 24, 28 | eqtrd 2656 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑋 ∨ (𝑃 ∧ 𝑊)) = 𝑋) |
30 | 13, 20, 29 | 3eqtr2d 2662 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → ((𝑃 ∨ 𝑋) ∧ 𝑊) = 𝑋) |