Proof of Theorem cdlemk2
Step | Hyp | Ref
| Expression |
1 | | simp1 1135 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | | simp2r 1199 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐺 ∈ 𝑇) |
3 | | simp2l 1198 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ∈ 𝑇) |
4 | | cdlemk.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
5 | | cdlemk.t |
. . . . . 6
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
6 | 4, 5 | ltrncnv 38156 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ◡𝐹 ∈ 𝑇) |
7 | 1, 3, 6 | syl2anc 584 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ◡𝐹 ∈ 𝑇) |
8 | 4, 5 | ltrnco 38729 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ ◡𝐹 ∈ 𝑇) → (𝐺 ∘ ◡𝐹) ∈ 𝑇) |
9 | 1, 2, 7, 8 | syl3anc 1370 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ ◡𝐹) ∈ 𝑇) |
10 | | cdlemk.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
11 | | cdlemk.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
12 | 10, 11, 4, 5 | ltrnel 38149 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) |
13 | 12 | 3adant2r 1178 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) |
14 | | cdlemk.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
15 | | cdlemk.r |
. . . 4
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
16 | 10, 14, 11, 4, 5, 15 | trljat3 38178 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ◡𝐹) ∈ 𝑇 ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))) = (((𝐺 ∘ ◡𝐹)‘(𝐹‘𝑃)) ∨ (𝑅‘(𝐺 ∘ ◡𝐹)))) |
17 | 1, 9, 13, 16 | syl3anc 1370 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))) = (((𝐺 ∘ ◡𝐹)‘(𝐹‘𝑃)) ∨ (𝑅‘(𝐺 ∘ ◡𝐹)))) |
18 | | simp3l 1200 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ 𝐴) |
19 | 10, 11, 4, 5 | ltrncoval 38155 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺 ∘ ◡𝐹) ∈ 𝑇 ∧ 𝐹 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (((𝐺 ∘ ◡𝐹) ∘ 𝐹)‘𝑃) = ((𝐺 ∘ ◡𝐹)‘(𝐹‘𝑃))) |
20 | 1, 9, 3, 18, 19 | syl121anc 1374 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺 ∘ ◡𝐹) ∘ 𝐹)‘𝑃) = ((𝐺 ∘ ◡𝐹)‘(𝐹‘𝑃))) |
21 | | coass 6168 |
. . . . . 6
⊢ ((𝐺 ∘ ◡𝐹) ∘ 𝐹) = (𝐺 ∘ (◡𝐹 ∘ 𝐹)) |
22 | | cdlemk.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝐾) |
23 | 22, 4, 5 | ltrn1o 38134 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵) |
24 | 1, 3, 23 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹:𝐵–1-1-onto→𝐵) |
25 | | f1ococnv1 6742 |
. . . . . . . . 9
⊢ (𝐹:𝐵–1-1-onto→𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐵)) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐵)) |
27 | 26 | coeq2d 5770 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ (◡𝐹 ∘ 𝐹)) = (𝐺 ∘ ( I ↾ 𝐵))) |
28 | 22, 4, 5 | ltrn1o 38134 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → 𝐺:𝐵–1-1-onto→𝐵) |
29 | 1, 2, 28 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐺:𝐵–1-1-onto→𝐵) |
30 | | f1of 6714 |
. . . . . . . 8
⊢ (𝐺:𝐵–1-1-onto→𝐵 → 𝐺:𝐵⟶𝐵) |
31 | | fcoi1 6646 |
. . . . . . . 8
⊢ (𝐺:𝐵⟶𝐵 → (𝐺 ∘ ( I ↾ 𝐵)) = 𝐺) |
32 | 29, 30, 31 | 3syl 18 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ ( I ↾ 𝐵)) = 𝐺) |
33 | 27, 32 | eqtrd 2780 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ (◡𝐹 ∘ 𝐹)) = 𝐺) |
34 | 21, 33 | eqtrid 2792 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺 ∘ ◡𝐹) ∘ 𝐹) = 𝐺) |
35 | 34 | fveq1d 6773 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺 ∘ ◡𝐹) ∘ 𝐹)‘𝑃) = (𝐺‘𝑃)) |
36 | 20, 35 | eqtr3d 2782 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺 ∘ ◡𝐹)‘(𝐹‘𝑃)) = (𝐺‘𝑃)) |
37 | 36 | oveq1d 7286 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺 ∘ ◡𝐹)‘(𝐹‘𝑃)) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))) = ((𝐺‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹)))) |
38 | 17, 37 | eqtr2d 2781 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))) = ((𝐹‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹)))) |