Proof of Theorem dihglblem3N
Step | Hyp | Ref
| Expression |
1 | | simp1 1054 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | | dihglblem.t |
. . . . . 6
⊢ 𝑇 = {𝑢 ∈ 𝐵 ∣ ∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊)} |
3 | | simp11l 1165 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → 𝐾 ∈ HL) |
4 | | hllat 33668 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → 𝐾 ∈ Lat) |
6 | | simp12l 1167 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → 𝑆 ⊆ 𝐵) |
7 | | simp3 1056 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → 𝑣 ∈ 𝑆) |
8 | 6, 7 | sseldd 3569 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → 𝑣 ∈ 𝐵) |
9 | | simp11r 1166 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → 𝑊 ∈ 𝐻) |
10 | | dihglblem.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝐾) |
11 | | dihglblem.h |
. . . . . . . . . . . . 13
⊢ 𝐻 = (LHyp‘𝐾) |
12 | 10, 11 | lhpbase 34302 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
13 | 9, 12 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → 𝑊 ∈ 𝐵) |
14 | | dihglblem.l |
. . . . . . . . . . . 12
⊢ ≤ =
(le‘𝐾) |
15 | | dihglblem.m |
. . . . . . . . . . . 12
⊢ ∧ =
(meet‘𝐾) |
16 | 10, 14, 15 | latmle2 16900 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ Lat ∧ 𝑣 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑣 ∧ 𝑊) ≤ 𝑊) |
17 | 5, 8, 13, 16 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆) → (𝑣 ∧ 𝑊) ≤ 𝑊) |
18 | 17 | 3expia 1259 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵) → (𝑣 ∈ 𝑆 → (𝑣 ∧ 𝑊) ≤ 𝑊)) |
19 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑢 = (𝑣 ∧ 𝑊) → (𝑢 ≤ 𝑊 ↔ (𝑣 ∧ 𝑊) ≤ 𝑊)) |
20 | 19 | biimprcd 239 |
. . . . . . . . 9
⊢ ((𝑣 ∧ 𝑊) ≤ 𝑊 → (𝑢 = (𝑣 ∧ 𝑊) → 𝑢 ≤ 𝑊)) |
21 | 18, 20 | syl6 34 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵) → (𝑣 ∈ 𝑆 → (𝑢 = (𝑣 ∧ 𝑊) → 𝑢 ≤ 𝑊))) |
22 | 21 | rexlimdv 3012 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑢 ∈ 𝐵) → (∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊) → 𝑢 ≤ 𝑊)) |
23 | 22 | ss2rabdv 3646 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → {𝑢 ∈ 𝐵 ∣ ∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊)} ⊆ {𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊}) |
24 | 2, 23 | syl5eqss 3612 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → 𝑇 ⊆ {𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊}) |
25 | | dihglblem.i |
. . . . . . 7
⊢ 𝐽 = ((DIsoB‘𝐾)‘𝑊) |
26 | 10, 14, 11, 25 | dibdmN 35464 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → dom 𝐽 = {𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊}) |
27 | 26 | 3ad2ant1 1075 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → dom 𝐽 = {𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊}) |
28 | 24, 27 | sseqtr4d 3605 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → 𝑇 ⊆ dom 𝐽) |
29 | | dihglblem.g |
. . . . . 6
⊢ 𝐺 = (glb‘𝐾) |
30 | 10, 14, 15, 29, 11, 2 | dihglblem2aN 35600 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → 𝑇 ≠ ∅) |
31 | 30 | 3adant3 1074 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → 𝑇 ≠ ∅) |
32 | 29, 11, 25 | dibglbN 35473 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑇 ⊆ dom 𝐽 ∧ 𝑇 ≠ ∅)) → (𝐽‘(𝐺‘𝑇)) = ∩
𝑥 ∈ 𝑇 (𝐽‘𝑥)) |
33 | 1, 28, 31, 32 | syl12anc 1316 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐽‘(𝐺‘𝑇)) = ∩
𝑥 ∈ 𝑇 (𝐽‘𝑥)) |
34 | 10, 14, 15, 29, 11, 2 | dihglblem2N 35601 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐺‘𝑆) = (𝐺‘𝑇)) |
35 | 34 | 3adant2r 1313 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐺‘𝑆) = (𝐺‘𝑇)) |
36 | 35 | fveq2d 6107 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐽‘(𝐺‘𝑆)) = (𝐽‘(𝐺‘𝑇))) |
37 | | simpl1 1057 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑇) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
38 | 24 | sselda 3568 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑇) → 𝑥 ∈ {𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊}) |
39 | | breq1 4586 |
. . . . . . 7
⊢ (𝑢 = 𝑥 → (𝑢 ≤ 𝑊 ↔ 𝑥 ≤ 𝑊)) |
40 | 39 | elrab 3331 |
. . . . . 6
⊢ (𝑥 ∈ {𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊} ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊)) |
41 | 38, 40 | sylib 207 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑇) → (𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊)) |
42 | | dihglblem.ih |
. . . . . 6
⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
43 | 10, 14, 11, 42, 25 | dihvalb 35544 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊)) → (𝐼‘𝑥) = (𝐽‘𝑥)) |
44 | 37, 41, 43 | syl2anc 691 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑇) → (𝐼‘𝑥) = (𝐽‘𝑥)) |
45 | 44 | iineq2dv 4479 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → ∩
𝑥 ∈ 𝑇 (𝐼‘𝑥) = ∩ 𝑥 ∈ 𝑇 (𝐽‘𝑥)) |
46 | 33, 36, 45 | 3eqtr4rd 2655 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → ∩
𝑥 ∈ 𝑇 (𝐼‘𝑥) = (𝐽‘(𝐺‘𝑆))) |
47 | | simp1l 1078 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ HL) |
48 | | hlclat 33663 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) |
49 | 47, 48 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ CLat) |
50 | | simp2l 1080 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → 𝑆 ⊆ 𝐵) |
51 | 10, 29 | clatglbcl 16937 |
. . . 4
⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵) |
52 | 49, 50, 51 | syl2anc 691 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐺‘𝑆) ∈ 𝐵) |
53 | | simp3 1056 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐺‘𝑆) ≤ 𝑊) |
54 | 10, 14, 11, 42, 25 | dihvalb 35544 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊)) → (𝐼‘(𝐺‘𝑆)) = (𝐽‘(𝐺‘𝑆))) |
55 | 1, 52, 53, 54 | syl12anc 1316 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑆)) = (𝐽‘(𝐺‘𝑆))) |
56 | 35 | fveq2d 6107 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑆)) = (𝐼‘(𝐺‘𝑇))) |
57 | 46, 55, 56 | 3eqtr2rd 2651 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑇)) = ∩
𝑥 ∈ 𝑇 (𝐼‘𝑥)) |