Step | Hyp | Ref
| Expression |
1 | | simpll 786 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → 𝐾 ∈ HL) |
2 | | simpr 476 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
3 | | lhpj1.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
4 | | lhpj1.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
5 | 3, 4 | lhpbase 34302 |
. . . . 5
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
6 | 5 | ad2antlr 759 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → 𝑊 ∈ 𝐵) |
7 | | lhpj1.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
8 | | eqid 2610 |
. . . . 5
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
9 | 3, 7, 8 | hlrelat2 33707 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (¬ 𝑋 ≤ 𝑊 ↔ ∃𝑝 ∈ (Atoms‘𝐾)(𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊))) |
10 | 1, 2, 6, 9 | syl3anc 1318 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (¬ 𝑋 ≤ 𝑊 ↔ ∃𝑝 ∈ (Atoms‘𝐾)(𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊))) |
11 | | simp1l 1078 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
12 | | simp2 1055 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → 𝑝 ∈ (Atoms‘𝐾)) |
13 | | simp3r 1083 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → ¬ 𝑝 ≤ 𝑊) |
14 | | lhpj1.j |
. . . . . . . 8
⊢ ∨ =
(join‘𝐾) |
15 | | lhpj1.u |
. . . . . . . 8
⊢ 1 =
(1.‘𝐾) |
16 | 7, 14, 15, 8, 4 | lhpjat1 34324 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝 ≤ 𝑊)) → (𝑊 ∨ 𝑝) = 1 ) |
17 | 11, 12, 13, 16 | syl12anc 1316 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → (𝑊 ∨ 𝑝) = 1 ) |
18 | | simp3l 1082 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → 𝑝 ≤ 𝑋) |
19 | | simp1ll 1117 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → 𝐾 ∈ HL) |
20 | | hllat 33668 |
. . . . . . . . 9
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
21 | 19, 20 | syl 17 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → 𝐾 ∈ Lat) |
22 | 3, 8 | atbase 33594 |
. . . . . . . . 9
⊢ (𝑝 ∈ (Atoms‘𝐾) → 𝑝 ∈ 𝐵) |
23 | 22 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → 𝑝 ∈ 𝐵) |
24 | | simp1r 1079 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → 𝑋 ∈ 𝐵) |
25 | 6 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → 𝑊 ∈ 𝐵) |
26 | 3, 7, 14 | latjlej2 16889 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ (𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (𝑝 ≤ 𝑋 → (𝑊 ∨ 𝑝) ≤ (𝑊 ∨ 𝑋))) |
27 | 21, 23, 24, 25, 26 | syl13anc 1320 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → (𝑝 ≤ 𝑋 → (𝑊 ∨ 𝑝) ≤ (𝑊 ∨ 𝑋))) |
28 | 18, 27 | mpd 15 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → (𝑊 ∨ 𝑝) ≤ (𝑊 ∨ 𝑋)) |
29 | 17, 28 | eqbrtrrd 4607 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → 1 ≤ (𝑊 ∨ 𝑋)) |
30 | | hlop 33667 |
. . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
31 | 19, 30 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → 𝐾 ∈ OP) |
32 | 3, 14 | latjcl 16874 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑊 ∨ 𝑋) ∈ 𝐵) |
33 | 21, 25, 24, 32 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → (𝑊 ∨ 𝑋) ∈ 𝐵) |
34 | 3, 7, 15 | op1le 33497 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ (𝑊 ∨ 𝑋) ∈ 𝐵) → ( 1 ≤ (𝑊 ∨ 𝑋) ↔ (𝑊 ∨ 𝑋) = 1 )) |
35 | 31, 33, 34 | syl2anc 691 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → ( 1 ≤ (𝑊 ∨ 𝑋) ↔ (𝑊 ∨ 𝑋) = 1 )) |
36 | 29, 35 | mpbid 221 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊)) → (𝑊 ∨ 𝑋) = 1 ) |
37 | 36 | rexlimdv3a 3015 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (∃𝑝 ∈ (Atoms‘𝐾)(𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊) → (𝑊 ∨ 𝑋) = 1 )) |
38 | 10, 37 | sylbid 229 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (¬ 𝑋 ≤ 𝑊 → (𝑊 ∨ 𝑋) = 1 )) |
39 | 38 | impr 647 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) → (𝑊 ∨ 𝑋) = 1 ) |