Proof of Theorem cdlemk55u1
Step | Hyp | Ref
| Expression |
1 | | simp11 1084 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | | simp21l 1171 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = (𝑅‘𝑁)) |
3 | | simp12 1085 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ∈ 𝑇) |
4 | | simp13 1086 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑁 ∈ 𝑇) |
5 | | simp21r 1172 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ≠ 𝑁) |
6 | | cdlemk5.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
7 | | cdlemk5.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
8 | | cdlemk5.t |
. . . . . 6
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
9 | | cdlemk5.r |
. . . . . 6
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
10 | 6, 7, 8, 9 | trlnid 34484 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝐹 ≠ 𝑁 ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → 𝐹 ≠ ( I ↾ 𝐵)) |
11 | 1, 3, 4, 5, 2, 10 | syl122anc 1327 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ≠ ( I ↾ 𝐵)) |
12 | 3, 11, 4 | 3jca 1235 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑁 ∈ 𝑇)) |
13 | | simp22 1088 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐺 ∈ 𝑇) |
14 | | simp23 1089 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐼 ∈ 𝑇) |
15 | | simp3 1056 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
16 | | cdlemk5.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
17 | | cdlemk5.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
18 | | cdlemk5.m |
. . . 4
⊢ ∧ =
(meet‘𝐾) |
19 | | cdlemk5.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
20 | | cdlemk5.z |
. . . 4
⊢ 𝑍 = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) |
21 | | cdlemk5.y |
. . . 4
⊢ 𝑌 = ((𝑃 ∨ (𝑅‘𝑔)) ∧ (𝑍 ∨ (𝑅‘(𝑔 ∘ ◡𝑏)))) |
22 | | cdlemk5.x |
. . . 4
⊢ 𝑋 = (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝑔)) → (𝑧‘𝑃) = 𝑌)) |
23 | 6, 16, 17, 18, 19, 7, 8, 9, 20,
21, 22 | cdlemk55 35267 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑁 ∈ 𝑇) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋 = (⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)) |
24 | 1, 2, 12, 13, 14, 15, 23 | syl231anc 1338 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋 = (⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)) |
25 | 7, 8 | ltrnco 35025 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) → (𝐺 ∘ 𝐼) ∈ 𝑇) |
26 | 1, 13, 14, 25 | syl3anc 1318 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ 𝐼) ∈ 𝑇) |
27 | | cdlemk5.u |
. . . 4
⊢ 𝑈 = (𝑔 ∈ 𝑇 ↦ if(𝐹 = 𝑁, 𝑔, 𝑋)) |
28 | 22, 27 | cdlemk40f 35225 |
. . 3
⊢ ((𝐹 ≠ 𝑁 ∧ (𝐺 ∘ 𝐼) ∈ 𝑇) → (𝑈‘(𝐺 ∘ 𝐼)) = ⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋) |
29 | 5, 26, 28 | syl2anc 691 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑈‘(𝐺 ∘ 𝐼)) = ⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋) |
30 | 22, 27 | cdlemk40f 35225 |
. . . 4
⊢ ((𝐹 ≠ 𝑁 ∧ 𝐺 ∈ 𝑇) → (𝑈‘𝐺) = ⦋𝐺 / 𝑔⦌𝑋) |
31 | 5, 13, 30 | syl2anc 691 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑈‘𝐺) = ⦋𝐺 / 𝑔⦌𝑋) |
32 | 22, 27 | cdlemk40f 35225 |
. . . 4
⊢ ((𝐹 ≠ 𝑁 ∧ 𝐼 ∈ 𝑇) → (𝑈‘𝐼) = ⦋𝐼 / 𝑔⦌𝑋) |
33 | 5, 14, 32 | syl2anc 691 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑈‘𝐼) = ⦋𝐼 / 𝑔⦌𝑋) |
34 | 31, 33 | coeq12d 5208 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘𝐺) ∘ (𝑈‘𝐼)) = (⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)) |
35 | 24, 29, 34 | 3eqtr4d 2654 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑈‘(𝐺 ∘ 𝐼)) = ((𝑈‘𝐺) ∘ (𝑈‘𝐼))) |