Proof of Theorem cdlemkid1
Step | Hyp | Ref
| Expression |
1 | | cdlemk5.z |
. . 3
⊢ 𝑍 = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) |
2 | 1 | oveq1i 6559 |
. 2
⊢ (𝑍 ∨ (𝑅‘𝑏)) = (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) ∨ (𝑅‘𝑏)) |
3 | | simp1l 1078 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ HL) |
4 | | simp1 1054 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
5 | | simp3rl 1127 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑏 ∈ 𝑇) |
6 | | simp3rr 1128 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑏 ≠ ( I ↾ 𝐵)) |
7 | | cdlemk5.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
8 | | cdlemk5.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
9 | | cdlemk5.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
10 | | cdlemk5.t |
. . . . . 6
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
11 | | cdlemk5.r |
. . . . . 6
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
12 | 7, 8, 9, 10, 11 | trlnidat 34478 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)) → (𝑅‘𝑏) ∈ 𝐴) |
13 | 4, 5, 6, 12 | syl3anc 1318 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑏) ∈ 𝐴) |
14 | | simp3ll 1125 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑃 ∈ 𝐴) |
15 | | cdlemk5.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
16 | 7, 15, 8 | hlatjcl 33671 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝑏) ∈ 𝐴) → (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵) |
17 | 3, 14, 13, 16 | syl3anc 1318 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵) |
18 | | hllat 33668 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
19 | 3, 18 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ Lat) |
20 | | simp22 1088 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑁 ∈ 𝑇) |
21 | 7, 8 | atbase 33594 |
. . . . . . 7
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵) |
22 | 14, 21 | syl 17 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑃 ∈ 𝐵) |
23 | 7, 9, 10 | ltrncl 34429 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵) → (𝑁‘𝑃) ∈ 𝐵) |
24 | 4, 20, 22, 23 | syl3anc 1318 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑁‘𝑃) ∈ 𝐵) |
25 | | simp21 1087 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐹 ∈ 𝑇) |
26 | 9, 10 | ltrncnv 34450 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ◡𝐹 ∈ 𝑇) |
27 | 4, 25, 26 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ◡𝐹 ∈ 𝑇) |
28 | 9, 10 | ltrnco 35025 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑏 ∈ 𝑇 ∧ ◡𝐹 ∈ 𝑇) → (𝑏 ∘ ◡𝐹) ∈ 𝑇) |
29 | 4, 5, 27, 28 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑏 ∘ ◡𝐹) ∈ 𝑇) |
30 | 7, 9, 10, 11 | trlcl 34469 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑏 ∘ ◡𝐹) ∈ 𝑇) → (𝑅‘(𝑏 ∘ ◡𝐹)) ∈ 𝐵) |
31 | 4, 29, 30 | syl2anc 691 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘(𝑏 ∘ ◡𝐹)) ∈ 𝐵) |
32 | 7, 15 | latjcl 16874 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑁‘𝑃) ∈ 𝐵 ∧ (𝑅‘(𝑏 ∘ ◡𝐹)) ∈ 𝐵) → ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))) ∈ 𝐵) |
33 | 19, 24, 31, 32 | syl3anc 1318 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))) ∈ 𝐵) |
34 | | cdlemk5.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
35 | 34, 15, 8 | hlatlej2 33680 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝑏) ∈ 𝐴) → (𝑅‘𝑏) ≤ (𝑃 ∨ (𝑅‘𝑏))) |
36 | 3, 14, 13, 35 | syl3anc 1318 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑏) ≤ (𝑃 ∨ (𝑅‘𝑏))) |
37 | | cdlemk5.m |
. . . . 5
⊢ ∧ =
(meet‘𝐾) |
38 | 7, 34, 15, 37, 8 | atmod2i1 34165 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ ((𝑅‘𝑏) ∈ 𝐴 ∧ (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵 ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))) ∈ 𝐵) ∧ (𝑅‘𝑏) ≤ (𝑃 ∨ (𝑅‘𝑏))) → (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) ∨ (𝑅‘𝑏)) = ((𝑃 ∨ (𝑅‘𝑏)) ∧ (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))) ∨ (𝑅‘𝑏)))) |
39 | 3, 13, 17, 33, 36, 38 | syl131anc 1331 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) ∨ (𝑅‘𝑏)) = ((𝑃 ∨ (𝑅‘𝑏)) ∧ (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))) ∨ (𝑅‘𝑏)))) |
40 | 7, 8 | atbase 33594 |
. . . . . . . 8
⊢ ((𝑅‘𝑏) ∈ 𝐴 → (𝑅‘𝑏) ∈ 𝐵) |
41 | 13, 40 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑏) ∈ 𝐵) |
42 | 7, 9, 10, 11 | trlcl 34469 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇) → (𝑅‘𝑁) ∈ 𝐵) |
43 | 4, 20, 42 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑁) ∈ 𝐵) |
44 | 7, 15 | latj32 16920 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵 ∧ (𝑅‘𝑁) ∈ 𝐵)) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = ((𝑃 ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏))) |
45 | 19, 22, 41, 43, 44 | syl13anc 1320 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = ((𝑃 ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏))) |
46 | | simp3l 1082 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
47 | 34, 15, 8, 9, 10, 11 | trljat3 34473 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ (𝑅‘𝑁)) = ((𝑁‘𝑃) ∨ (𝑅‘𝑁))) |
48 | 4, 20, 46, 47 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∨ (𝑅‘𝑁)) = ((𝑁‘𝑃) ∨ (𝑅‘𝑁))) |
49 | 48 | oveq1d 6564 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)) = (((𝑁‘𝑃) ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏))) |
50 | 7, 15 | latjass 16918 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ ((𝑁‘𝑃) ∈ 𝐵 ∧ (𝑅‘𝑁) ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵)) → (((𝑁‘𝑃) ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏)))) |
51 | 19, 24, 43, 41, 50 | syl13anc 1320 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑁‘𝑃) ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏)))) |
52 | 45, 49, 51 | 3eqtrd 2648 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏)))) |
53 | 7, 15 | latjass 16918 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ ((𝑁‘𝑃) ∈ 𝐵 ∧ (𝑅‘(𝑏 ∘ ◡𝐹)) ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵)) → (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘(𝑏 ∘ ◡𝐹)) ∨ (𝑅‘𝑏)))) |
54 | 19, 24, 31, 41, 53 | syl13anc 1320 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘(𝑏 ∘ ◡𝐹)) ∨ (𝑅‘𝑏)))) |
55 | 7, 15 | latjcom 16882 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝑁) ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘𝑏) ∨ (𝑅‘𝑁))) |
56 | 19, 43, 41, 55 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘𝑏) ∨ (𝑅‘𝑁))) |
57 | 9, 10, 11 | trlcnv 34470 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘◡𝐹) = (𝑅‘𝐹)) |
58 | 4, 25, 57 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘◡𝐹) = (𝑅‘𝐹)) |
59 | | simp23 1089 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝐹) = (𝑅‘𝑁)) |
60 | 58, 59 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘◡𝐹) = (𝑅‘𝑁)) |
61 | 60 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑏) ∨ (𝑅‘◡𝐹)) = ((𝑅‘𝑏) ∨ (𝑅‘𝑁))) |
62 | 56, 61 | eqtr4d 2647 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘𝑏) ∨ (𝑅‘◡𝐹))) |
63 | 15, 9, 10, 11 | trljco 35046 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑏 ∈ 𝑇 ∧ ◡𝐹 ∈ 𝑇) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))) = ((𝑅‘𝑏) ∨ (𝑅‘◡𝐹))) |
64 | 4, 5, 27, 63 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))) = ((𝑅‘𝑏) ∨ (𝑅‘◡𝐹))) |
65 | 7, 15 | latjcom 16882 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝑏) ∈ 𝐵 ∧ (𝑅‘(𝑏 ∘ ◡𝐹)) ∈ 𝐵) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))) = ((𝑅‘(𝑏 ∘ ◡𝐹)) ∨ (𝑅‘𝑏))) |
66 | 19, 41, 31, 65 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))) = ((𝑅‘(𝑏 ∘ ◡𝐹)) ∨ (𝑅‘𝑏))) |
67 | 62, 64, 66 | 3eqtr2d 2650 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘(𝑏 ∘ ◡𝐹)) ∨ (𝑅‘𝑏))) |
68 | 67 | oveq2d 6565 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))) = ((𝑁‘𝑃) ∨ ((𝑅‘(𝑏 ∘ ◡𝐹)) ∨ (𝑅‘𝑏)))) |
69 | 54, 68 | eqtr4d 2647 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏)))) |
70 | 52, 69 | eqtr4d 2647 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))) ∨ (𝑅‘𝑏))) |
71 | 70 | oveq2d 6565 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁))) = ((𝑃 ∨ (𝑅‘𝑏)) ∧ (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))) ∨ (𝑅‘𝑏)))) |
72 | 7, 15, 37 | latabs2 16911 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵 ∧ (𝑅‘𝑁) ∈ 𝐵) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁))) = (𝑃 ∨ (𝑅‘𝑏))) |
73 | 19, 17, 43, 72 | syl3anc 1318 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁))) = (𝑃 ∨ (𝑅‘𝑏))) |
74 | 39, 71, 73 | 3eqtr2d 2650 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) ∨ (𝑅‘𝑏)) = (𝑃 ∨ (𝑅‘𝑏))) |
75 | 2, 74 | syl5eq 2656 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑍 ∨ (𝑅‘𝑏)) = (𝑃 ∨ (𝑅‘𝑏))) |