Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . 4
⊢
(Base‘𝐾) =
(Base‘𝐾) |
2 | | lvolex3.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
3 | | eqid 2738 |
. . . 4
⊢
(join‘𝐾) =
(join‘𝐾) |
4 | | lvolex3.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
5 | | lvolex3.p |
. . . 4
⊢ 𝑃 = (LPlanes‘𝐾) |
6 | 1, 2, 3, 4, 5 | islpln2 37162 |
. . 3
⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝑃 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 ∃𝑡 ∈ 𝐴 (𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ (𝑟(join‘𝐾)𝑠) ∧ 𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡))))) |
7 | | simp1l 1198 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴)) ∧ 𝑡 ∈ 𝐴 ∧ (𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ (𝑟(join‘𝐾)𝑠) ∧ 𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡))) → 𝐾 ∈ HL) |
8 | | simp1rl 1239 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴)) ∧ 𝑡 ∈ 𝐴 ∧ (𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ (𝑟(join‘𝐾)𝑠) ∧ 𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡))) → 𝑟 ∈ 𝐴) |
9 | | simp1rr 1240 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴)) ∧ 𝑡 ∈ 𝐴 ∧ (𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ (𝑟(join‘𝐾)𝑠) ∧ 𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡))) → 𝑠 ∈ 𝐴) |
10 | | simp2 1138 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴)) ∧ 𝑡 ∈ 𝐴 ∧ (𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ (𝑟(join‘𝐾)𝑠) ∧ 𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡))) → 𝑡 ∈ 𝐴) |
11 | 3, 2, 4 | 3dim3 37095 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴)) → ∃𝑞 ∈ 𝐴 ¬ 𝑞 ≤ ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡)) |
12 | 7, 8, 9, 10, 11 | syl13anc 1373 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴)) ∧ 𝑡 ∈ 𝐴 ∧ (𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ (𝑟(join‘𝐾)𝑠) ∧ 𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡))) → ∃𝑞 ∈ 𝐴 ¬ 𝑞 ≤ ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡)) |
13 | | simp33 1212 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴)) ∧ 𝑡 ∈ 𝐴 ∧ (𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ (𝑟(join‘𝐾)𝑠) ∧ 𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡))) → 𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡)) |
14 | | breq2 5031 |
. . . . . . . . . 10
⊢ (𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡) → (𝑞 ≤ 𝑋 ↔ 𝑞 ≤ ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡))) |
15 | 14 | notbid 321 |
. . . . . . . . 9
⊢ (𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡) → (¬ 𝑞 ≤ 𝑋 ↔ ¬ 𝑞 ≤ ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡))) |
16 | 15 | rexbidv 3206 |
. . . . . . . 8
⊢ (𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡) → (∃𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋 ↔ ∃𝑞 ∈ 𝐴 ¬ 𝑞 ≤ ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡))) |
17 | 13, 16 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴)) ∧ 𝑡 ∈ 𝐴 ∧ (𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ (𝑟(join‘𝐾)𝑠) ∧ 𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡))) → (∃𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋 ↔ ∃𝑞 ∈ 𝐴 ¬ 𝑞 ≤ ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡))) |
18 | 12, 17 | mpbird 260 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴)) ∧ 𝑡 ∈ 𝐴 ∧ (𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ (𝑟(join‘𝐾)𝑠) ∧ 𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡))) → ∃𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋) |
19 | 18 | rexlimdv3a 3195 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴)) → (∃𝑡 ∈ 𝐴 (𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ (𝑟(join‘𝐾)𝑠) ∧ 𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡)) → ∃𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋)) |
20 | 19 | rexlimdvva 3203 |
. . . 4
⊢ (𝐾 ∈ HL → (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 ∃𝑡 ∈ 𝐴 (𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ (𝑟(join‘𝐾)𝑠) ∧ 𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡)) → ∃𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋)) |
21 | 20 | adantld 494 |
. . 3
⊢ (𝐾 ∈ HL → ((𝑋 ∈ (Base‘𝐾) ∧ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 ∃𝑡 ∈ 𝐴 (𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ (𝑟(join‘𝐾)𝑠) ∧ 𝑋 = ((𝑟(join‘𝐾)𝑠)(join‘𝐾)𝑡))) → ∃𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋)) |
22 | 6, 21 | sylbid 243 |
. 2
⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝑃 → ∃𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋)) |
23 | 22 | imp 410 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃) → ∃𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋) |