Proof of Theorem cdlemg17dN
Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇)) |
2 | | simp21 1207 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
3 | | simpl1 1192 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ HL) |
4 | | simpl2 1193 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻) |
5 | | simpl3 1194 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐺 ∈ 𝑇) |
6 | | simpr 488 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
7 | | cdlemg12.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
8 | | cdlemg12.j |
. . . . 5
⊢ ∨ =
(join‘𝐾) |
9 | | cdlemg12.m |
. . . . 5
⊢ ∧ =
(meet‘𝐾) |
10 | | cdlemg12.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
11 | | cdlemg12.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
12 | | cdlemg12.t |
. . . . 5
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
13 | | cdlemg12b.r |
. . . . 5
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
14 | 7, 8, 9, 10, 11, 12, 13 | trlval2 37789 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐺) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊)) |
15 | 3, 4, 5, 6, 14 | syl211anc 1377 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐺) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊)) |
16 | 1, 2, 15 | syl2anc 587 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → (𝑅‘𝐺) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊)) |
17 | | simp11 1204 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → 𝐾 ∈ HL) |
18 | | simp12 1205 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → 𝑊 ∈ 𝐻) |
19 | 17, 18 | jca 515 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
20 | | simp22 1208 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
21 | | simp13 1206 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → 𝐺 ∈ 𝑇) |
22 | | simp23 1209 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → 𝑃 ≠ 𝑄) |
23 | | simp33 1212 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → (𝐺‘𝑃) ≠ 𝑃) |
24 | | simp31 1210 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄)) |
25 | | simp32 1211 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟))) |
26 | 7, 8, 9, 10, 11, 12, 13 | cdlemg17b 38288 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ ((𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → (𝐺‘𝑃) = 𝑄) |
27 | 19, 2, 20, 21, 22, 23, 24, 25, 26 | syl323anc 1401 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → (𝐺‘𝑃) = 𝑄) |
28 | 27 | oveq2d 7180 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → (𝑃 ∨ (𝐺‘𝑃)) = (𝑃 ∨ 𝑄)) |
29 | 28 | oveq1d 7179 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) = ((𝑃 ∨ 𝑄) ∧ 𝑊)) |
30 | 16, 29 | eqtrd 2773 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) ∧ (𝐺‘𝑃) ≠ 𝑃)) → (𝑅‘𝐺) = ((𝑃 ∨ 𝑄) ∧ 𝑊)) |