Step | Hyp | Ref
| Expression |
1 | | simpl1 1057 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | | simpl3 1059 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌)) → (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) |
3 | | dihord5apre.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
4 | | dihord5apre.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
5 | | dihord5apre.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
6 | | dihord5apre.m |
. . . 4
⊢ ∧ =
(meet‘𝐾) |
7 | | dihord5apre.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
8 | | dihord5apre.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
9 | 3, 4, 5, 6, 7, 8 | lhpmcvr2 34328 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) → ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) |
10 | 1, 2, 9 | syl2anc 691 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌)) → ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) |
11 | | simp11l 1165 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝐾 ∈ HL) |
12 | | hllat 33668 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
13 | 11, 12 | syl 17 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝐾 ∈ Lat) |
14 | | simp12l 1167 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝑋 ∈ 𝐵) |
15 | | simp3ll 1125 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝑟 ∈ 𝐴) |
16 | 3, 7 | atbase 33594 |
. . . . . . . . 9
⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ 𝐵) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝑟 ∈ 𝐵) |
18 | 3, 5 | latjcl 16874 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ 𝑟 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑟 ∨ 𝑋) ∈ 𝐵) |
19 | 13, 17, 14, 18 | syl3anc 1318 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝑟 ∨ 𝑋) ∈ 𝐵) |
20 | | simp13l 1169 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝑌 ∈ 𝐵) |
21 | 3, 4, 5 | latlej2 16884 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ 𝑟 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ (𝑟 ∨ 𝑋)) |
22 | 13, 17, 14, 21 | syl3anc 1318 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝑋 ≤ (𝑟 ∨ 𝑋)) |
23 | | simp11 1084 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
24 | | simp3lr 1126 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → ¬ 𝑟 ≤ 𝑊) |
25 | 3, 4, 5 | latlej1 16883 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Lat ∧ 𝑟 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → 𝑟 ≤ (𝑟 ∨ 𝑋)) |
26 | 13, 17, 14, 25 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝑟 ≤ (𝑟 ∨ 𝑋)) |
27 | | simp11r 1166 |
. . . . . . . . . . . . . 14
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝑊 ∈ 𝐻) |
28 | 3, 8 | lhpbase 34302 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝑊 ∈ 𝐵) |
30 | 3, 4 | lattr 16879 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Lat ∧ (𝑟 ∈ 𝐵 ∧ (𝑟 ∨ 𝑋) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑟 ≤ (𝑟 ∨ 𝑋) ∧ (𝑟 ∨ 𝑋) ≤ 𝑊) → 𝑟 ≤ 𝑊)) |
31 | 13, 17, 19, 29, 30 | syl13anc 1320 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → ((𝑟 ≤ (𝑟 ∨ 𝑋) ∧ (𝑟 ∨ 𝑋) ≤ 𝑊) → 𝑟 ≤ 𝑊)) |
32 | 26, 31 | mpand 707 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → ((𝑟 ∨ 𝑋) ≤ 𝑊 → 𝑟 ≤ 𝑊)) |
33 | 24, 32 | mtod 188 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → ¬ (𝑟 ∨ 𝑋) ≤ 𝑊) |
34 | | simp3l 1082 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊)) |
35 | | simp12 1085 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) |
36 | 3, 4, 5, 6, 7, 8 | lhple 34346 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → ((𝑟 ∨ 𝑋) ∧ 𝑊) = 𝑋) |
37 | 23, 34, 35, 36 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → ((𝑟 ∨ 𝑋) ∧ 𝑊) = 𝑋) |
38 | 37 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝑟 ∨ ((𝑟 ∨ 𝑋) ∧ 𝑊)) = (𝑟 ∨ 𝑋)) |
39 | | dihord5apre.i |
. . . . . . . . . . 11
⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
40 | | eqid 2610 |
. . . . . . . . . . 11
⊢
((DIsoB‘𝐾)‘𝑊) = ((DIsoB‘𝐾)‘𝑊) |
41 | | eqid 2610 |
. . . . . . . . . . 11
⊢
((DIsoC‘𝐾)‘𝑊) = ((DIsoC‘𝐾)‘𝑊) |
42 | | dihord5apre.u |
. . . . . . . . . . 11
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
43 | | dihord5apre.s |
. . . . . . . . . . 11
⊢ ⊕ =
(LSSum‘𝑈) |
44 | 3, 4, 5, 6, 7, 8, 39, 40, 41, 42, 43 | dihvalcq 35543 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑟 ∨ 𝑋) ∈ 𝐵 ∧ ¬ (𝑟 ∨ 𝑋) ≤ 𝑊) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ ((𝑟 ∨ 𝑋) ∧ 𝑊)) = (𝑟 ∨ 𝑋))) → (𝐼‘(𝑟 ∨ 𝑋)) = ((((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊕
(((DIsoB‘𝐾)‘𝑊)‘((𝑟 ∨ 𝑋) ∧ 𝑊)))) |
45 | 23, 19, 33, 34, 38, 44 | syl122anc 1327 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝐼‘(𝑟 ∨ 𝑋)) = ((((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊕
(((DIsoB‘𝐾)‘𝑊)‘((𝑟 ∨ 𝑋) ∧ 𝑊)))) |
46 | 8, 42, 23 | dvhlmod 35417 |
. . . . . . . . . . . . . 14
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝑈 ∈ LMod) |
47 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
48 | 47 | lsssssubg 18779 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ LMod →
(LSubSp‘𝑈) ⊆
(SubGrp‘𝑈)) |
49 | 46, 48 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈)) |
50 | 4, 7, 8, 42, 41, 47 | diclss 35500 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ∈ (LSubSp‘𝑈)) |
51 | 23, 34, 50 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ∈ (LSubSp‘𝑈)) |
52 | 49, 51 | sseldd 3569 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ∈ (SubGrp‘𝑈)) |
53 | 3, 6 | latmcl 16875 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑌 ∧ 𝑊) ∈ 𝐵) |
54 | 13, 20, 29, 53 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝑌 ∧ 𝑊) ∈ 𝐵) |
55 | 3, 4, 6 | latmle2 16900 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑌 ∧ 𝑊) ≤ 𝑊) |
56 | 13, 20, 29, 55 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝑌 ∧ 𝑊) ≤ 𝑊) |
57 | 3, 4, 8, 42, 40, 47 | diblss 35477 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑌 ∧ 𝑊) ∈ 𝐵 ∧ (𝑌 ∧ 𝑊) ≤ 𝑊)) → (((DIsoB‘𝐾)‘𝑊)‘(𝑌 ∧ 𝑊)) ∈ (LSubSp‘𝑈)) |
58 | 23, 54, 56, 57 | syl12anc 1316 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘(𝑌 ∧ 𝑊)) ∈ (LSubSp‘𝑈)) |
59 | 49, 58 | sseldd 3569 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘(𝑌 ∧ 𝑊)) ∈ (SubGrp‘𝑈)) |
60 | 43 | lsmub1 17894 |
. . . . . . . . . . . 12
⊢
(((((DIsoC‘𝐾)‘𝑊)‘𝑟) ∈ (SubGrp‘𝑈) ∧ (((DIsoB‘𝐾)‘𝑊)‘(𝑌 ∧ 𝑊)) ∈ (SubGrp‘𝑈)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊆ ((((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊕
(((DIsoB‘𝐾)‘𝑊)‘(𝑌 ∧ 𝑊)))) |
61 | 52, 59, 60 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊆ ((((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊕
(((DIsoB‘𝐾)‘𝑊)‘(𝑌 ∧ 𝑊)))) |
62 | | simp13 1086 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) |
63 | | simp3r 1083 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌) |
64 | 3, 4, 5, 6, 7, 8, 39, 40, 41, 42, 43 | dihvalcq 35543 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝐼‘𝑌) = ((((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊕
(((DIsoB‘𝐾)‘𝑊)‘(𝑌 ∧ 𝑊)))) |
65 | 23, 62, 34, 63, 64 | syl112anc 1322 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝐼‘𝑌) = ((((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊕
(((DIsoB‘𝐾)‘𝑊)‘(𝑌 ∧ 𝑊)))) |
66 | 61, 65 | sseqtr4d 3605 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊆ (𝐼‘𝑌)) |
67 | 37 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 ∨ 𝑋) ∧ 𝑊)) = (((DIsoB‘𝐾)‘𝑊)‘𝑋)) |
68 | 3, 4, 8, 39, 40 | dihvalb 35544 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = (((DIsoB‘𝐾)‘𝑊)‘𝑋)) |
69 | 23, 35, 68 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝐼‘𝑋) = (((DIsoB‘𝐾)‘𝑊)‘𝑋)) |
70 | 67, 69 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 ∨ 𝑋) ∧ 𝑊)) = (𝐼‘𝑋)) |
71 | | simp2 1055 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝐼‘𝑋) ⊆ (𝐼‘𝑌)) |
72 | 70, 71 | eqsstrd 3602 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 ∨ 𝑋) ∧ 𝑊)) ⊆ (𝐼‘𝑌)) |
73 | 3, 6 | latmcl 16875 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ Lat ∧ (𝑟 ∨ 𝑋) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → ((𝑟 ∨ 𝑋) ∧ 𝑊) ∈ 𝐵) |
74 | 13, 19, 29, 73 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → ((𝑟 ∨ 𝑋) ∧ 𝑊) ∈ 𝐵) |
75 | 3, 4, 6 | latmle2 16900 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ Lat ∧ (𝑟 ∨ 𝑋) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → ((𝑟 ∨ 𝑋) ∧ 𝑊) ≤ 𝑊) |
76 | 13, 19, 29, 75 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → ((𝑟 ∨ 𝑋) ∧ 𝑊) ≤ 𝑊) |
77 | 3, 4, 8, 42, 40, 47 | diblss 35477 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (((𝑟 ∨ 𝑋) ∧ 𝑊) ∈ 𝐵 ∧ ((𝑟 ∨ 𝑋) ∧ 𝑊) ≤ 𝑊)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 ∨ 𝑋) ∧ 𝑊)) ∈ (LSubSp‘𝑈)) |
78 | 23, 74, 76, 77 | syl12anc 1316 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 ∨ 𝑋) ∧ 𝑊)) ∈ (LSubSp‘𝑈)) |
79 | 49, 78 | sseldd 3569 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 ∨ 𝑋) ∧ 𝑊)) ∈ (SubGrp‘𝑈)) |
80 | 3, 8, 39, 42, 47 | dihlss 35557 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝐵) → (𝐼‘𝑌) ∈ (LSubSp‘𝑈)) |
81 | 23, 20, 80 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝐼‘𝑌) ∈ (LSubSp‘𝑈)) |
82 | 49, 81 | sseldd 3569 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝐼‘𝑌) ∈ (SubGrp‘𝑈)) |
83 | 43 | lsmlub 17901 |
. . . . . . . . . . 11
⊢
(((((DIsoC‘𝐾)‘𝑊)‘𝑟) ∈ (SubGrp‘𝑈) ∧ (((DIsoB‘𝐾)‘𝑊)‘((𝑟 ∨ 𝑋) ∧ 𝑊)) ∈ (SubGrp‘𝑈) ∧ (𝐼‘𝑌) ∈ (SubGrp‘𝑈)) → (((((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊆ (𝐼‘𝑌) ∧ (((DIsoB‘𝐾)‘𝑊)‘((𝑟 ∨ 𝑋) ∧ 𝑊)) ⊆ (𝐼‘𝑌)) ↔ ((((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊕
(((DIsoB‘𝐾)‘𝑊)‘((𝑟 ∨ 𝑋) ∧ 𝑊))) ⊆ (𝐼‘𝑌))) |
84 | 52, 79, 82, 83 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (((((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊆ (𝐼‘𝑌) ∧ (((DIsoB‘𝐾)‘𝑊)‘((𝑟 ∨ 𝑋) ∧ 𝑊)) ⊆ (𝐼‘𝑌)) ↔ ((((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊕
(((DIsoB‘𝐾)‘𝑊)‘((𝑟 ∨ 𝑋) ∧ 𝑊))) ⊆ (𝐼‘𝑌))) |
85 | 66, 72, 84 | mpbi2and 958 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → ((((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊕
(((DIsoB‘𝐾)‘𝑊)‘((𝑟 ∨ 𝑋) ∧ 𝑊))) ⊆ (𝐼‘𝑌)) |
86 | 45, 85 | eqsstrd 3602 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝐼‘(𝑟 ∨ 𝑋)) ⊆ (𝐼‘𝑌)) |
87 | 3, 4, 8, 39 | dihord4 35565 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑟 ∨ 𝑋) ∈ 𝐵 ∧ ¬ (𝑟 ∨ 𝑋) ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) → ((𝐼‘(𝑟 ∨ 𝑋)) ⊆ (𝐼‘𝑌) ↔ (𝑟 ∨ 𝑋) ≤ 𝑌)) |
88 | 23, 19, 33, 62, 87 | syl121anc 1323 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → ((𝐼‘(𝑟 ∨ 𝑋)) ⊆ (𝐼‘𝑌) ↔ (𝑟 ∨ 𝑋) ≤ 𝑌)) |
89 | 86, 88 | mpbid 221 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝑟 ∨ 𝑋) ≤ 𝑌) |
90 | 3, 4, 13, 14, 19, 20, 22, 89 | lattrd 16881 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝑋 ≤ 𝑌) |
91 | 90 | 3expia 1259 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌)) → (((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑋 ≤ 𝑌)) |
92 | 91 | exp4c 634 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌)) → (𝑟 ∈ 𝐴 → (¬ 𝑟 ≤ 𝑊 → ((𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌 → 𝑋 ≤ 𝑌)))) |
93 | 92 | imp4a 612 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌)) → (𝑟 ∈ 𝐴 → ((¬ 𝑟 ≤ 𝑊 ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑋 ≤ 𝑌))) |
94 | 93 | rexlimdv 3012 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌)) → (∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑟 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑋 ≤ 𝑌)) |
95 | 10, 94 | mpd 15 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) ∧ (𝐼‘𝑋) ⊆ (𝐼‘𝑌)) → 𝑋 ≤ 𝑌) |