Proof of Theorem cdlemg19a
Step | Hyp | Ref
| Expression |
1 | | simp11l 1340 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → 𝐾 ∈ HL) |
2 | 1 | hllatd 35523 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → 𝐾 ∈ Lat) |
3 | | simp12l 1342 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → 𝑃 ∈ 𝐴) |
4 | | simp11 1217 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
5 | | simp21 1220 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) |
6 | | cdlemg12.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
7 | | cdlemg12.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
8 | | cdlemg12.h |
. . . . . . 7
⊢ 𝐻 = (LHyp‘𝐾) |
9 | | cdlemg12.t |
. . . . . . 7
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
10 | 6, 7, 8, 9 | ltrncoat 36303 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (𝐹‘(𝐺‘𝑃)) ∈ 𝐴) |
11 | 4, 5, 3, 10 | syl3anc 1439 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → (𝐹‘(𝐺‘𝑃)) ∈ 𝐴) |
12 | | eqid 2778 |
. . . . . 6
⊢
(Base‘𝐾) =
(Base‘𝐾) |
13 | | cdlemg12.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
14 | 12, 13, 7 | hlatjcl 35526 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑃)) ∈ 𝐴) → (𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∈ (Base‘𝐾)) |
15 | 1, 3, 11, 14 | syl3anc 1439 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → (𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∈ (Base‘𝐾)) |
16 | | simp13l 1344 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → 𝑄 ∈ 𝐴) |
17 | 6, 7, 8, 9 | ltrncoat 36303 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑄 ∈ 𝐴) → (𝐹‘(𝐺‘𝑄)) ∈ 𝐴) |
18 | 4, 5, 16, 17 | syl3anc 1439 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → (𝐹‘(𝐺‘𝑄)) ∈ 𝐴) |
19 | 12, 13, 7 | hlatjcl 35526 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑄)) ∈ 𝐴) → (𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∈ (Base‘𝐾)) |
20 | 1, 16, 18, 19 | syl3anc 1439 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → (𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∈ (Base‘𝐾)) |
21 | | cdlemg12.m |
. . . . 5
⊢ ∧ =
(meet‘𝐾) |
22 | 12, 6, 21 | latmle1 17466 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∈ (Base‘𝐾) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∈ (Base‘𝐾)) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ (𝑃 ∨ (𝐹‘(𝐺‘𝑃)))) |
23 | 2, 15, 20, 22 | syl3anc 1439 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ (𝑃 ∨ (𝐹‘(𝐺‘𝑃)))) |
24 | | cdlemg12b.r |
. . . 4
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
25 | 6, 13, 21, 7, 8, 9,
24 | cdlemg18 36841 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ 𝑊) |
26 | 6, 13, 21, 7, 8, 9,
24 | cdlemg18d 36840 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ∈ 𝐴) |
27 | 12, 7 | atbase 35448 |
. . . . 5
⊢ (((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ∈ 𝐴 → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ∈ (Base‘𝐾)) |
28 | 26, 27 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ∈ (Base‘𝐾)) |
29 | | simp11r 1341 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → 𝑊 ∈ 𝐻) |
30 | 12, 8 | lhpbase 36157 |
. . . . 5
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
31 | 29, 30 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → 𝑊 ∈ (Base‘𝐾)) |
32 | 12, 6, 21 | latlem12 17468 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ (((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ∈ (Base‘𝐾) ∧ (𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ (𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ 𝑊) ↔ ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊))) |
33 | 2, 28, 15, 31, 32 | syl13anc 1440 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ((((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ (𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ 𝑊) ↔ ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊))) |
34 | 23, 25, 33 | mpbi2and 702 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊)) |
35 | | hlatl 35519 |
. . . 4
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
36 | 1, 35 | syl 17 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → 𝐾 ∈ AtLat) |
37 | | simp12 1218 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
38 | | simp13 1219 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
39 | | simp21l 1346 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → 𝐹 ∈ 𝑇) |
40 | | simp21r 1347 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → 𝐺 ∈ 𝑇) |
41 | | simp32 1224 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄)) |
42 | 6, 13, 21, 7, 8, 9 | cdlemg11a 36796 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄))) → (𝐹‘(𝐺‘𝑃)) ≠ 𝑃) |
43 | 4, 37, 38, 39, 40, 41, 42 | syl123anc 1455 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → (𝐹‘(𝐺‘𝑃)) ≠ 𝑃) |
44 | 43 | necomd 3024 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → 𝑃 ≠ (𝐹‘(𝐺‘𝑃))) |
45 | 6, 13, 21, 7, 8 | lhpat 36202 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ ((𝐹‘(𝐺‘𝑃)) ∈ 𝐴 ∧ 𝑃 ≠ (𝐹‘(𝐺‘𝑃)))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) ∈ 𝐴) |
46 | 4, 37, 11, 44, 45 | syl112anc 1442 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) ∈ 𝐴) |
47 | 6, 7 | atcmp 35470 |
. . 3
⊢ ((𝐾 ∈ AtLat ∧ ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ∈ 𝐴 ∧ ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) ∈ 𝐴) → (((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) ↔ ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) = ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊))) |
48 | 36, 26, 46, 47 | syl3anc 1439 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → (((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) ↔ ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) = ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊))) |
49 | 34, 48 | mpbid 224 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) = ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊)) |