Step | Hyp | Ref
| Expression |
1 | | simpl1 1064 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊))) |
2 | | simpl2l 1114 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → 𝑋 ∈ 𝐵) |
3 | | simpl2r 1115 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → 𝑌 ∈ 𝐵) |
4 | | simpl3 1066 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) |
5 | | simprl 794 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → 𝑓 ∈ 𝑇) |
6 | | simprr 796 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) |
7 | | dihjust.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
8 | | dihjust.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
9 | | dihjust.j |
. . . . . . 7
⊢ ∨ =
(join‘𝐾) |
10 | | dihjust.m |
. . . . . . 7
⊢ ∧ =
(meet‘𝐾) |
11 | | dihjust.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
12 | | dihjust.h |
. . . . . . 7
⊢ 𝐻 = (LHyp‘𝐾) |
13 | | dihjust.i |
. . . . . . 7
⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) |
14 | | dihjust.J |
. . . . . . 7
⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊) |
15 | | dihjust.u |
. . . . . . 7
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
16 | | dihjust.s |
. . . . . . 7
⊢ ⊕ =
(LSSum‘𝑈) |
17 | | dihord2c.t |
. . . . . . 7
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
18 | | dihord2c.r |
. . . . . . 7
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
19 | | dihord2c.o |
. . . . . . 7
⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) |
20 | | dihord2.p |
. . . . . . 7
⊢ 𝑃 = ((oc‘𝐾)‘𝑊) |
21 | | dihord2.e |
. . . . . . 7
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
22 | | dihord2.d |
. . . . . . 7
⊢ + =
(+g‘𝑈) |
23 | | dihord2.g |
. . . . . . 7
⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁) |
24 | 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 | dihord11c 36513 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊))) ∧ 𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → ∃𝑦 ∈ (𝐽‘𝑁)∃𝑧 ∈ (𝐼‘(𝑌 ∧ 𝑊))〈𝑓, 𝑂〉 = (𝑦 + 𝑧)) |
25 | 1, 2, 3, 4, 5, 6, 24 | syl123anc 1343 |
. . . . 5
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → ∃𝑦 ∈ (𝐽‘𝑁)∃𝑧 ∈ (𝐼‘(𝑌 ∧ 𝑊))〈𝑓, 𝑂〉 = (𝑦 + 𝑧)) |
26 | | simpl11 1136 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
27 | | simpl13 1138 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) |
28 | 8, 11, 12, 20, 17, 21, 14, 23 | dicelval3 36469 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) → (𝑦 ∈ (𝐽‘𝑁) ↔ ∃𝑠 ∈ 𝐸 𝑦 = 〈(𝑠‘𝐺), 𝑠〉)) |
29 | 26, 27, 28 | syl2anc 693 |
. . . . . . . 8
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → (𝑦 ∈ (𝐽‘𝑁) ↔ ∃𝑠 ∈ 𝐸 𝑦 = 〈(𝑠‘𝐺), 𝑠〉)) |
30 | | simp11l 1172 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → 𝐾 ∈ HL) |
31 | 30 | adantr 481 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → 𝐾 ∈ HL) |
32 | | hllat 34650 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → 𝐾 ∈ Lat) |
34 | | simp11r 1173 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → 𝑊 ∈ 𝐻) |
35 | 34 | adantr 481 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → 𝑊 ∈ 𝐻) |
36 | 7, 12 | lhpbase 35284 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
37 | 35, 36 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → 𝑊 ∈ 𝐵) |
38 | 7, 10 | latmcl 17052 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑌 ∧ 𝑊) ∈ 𝐵) |
39 | 33, 3, 37, 38 | syl3anc 1326 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → (𝑌 ∧ 𝑊) ∈ 𝐵) |
40 | 7, 8, 10 | latmle2 17077 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑌 ∧ 𝑊) ≤ 𝑊) |
41 | 33, 3, 37, 40 | syl3anc 1326 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → (𝑌 ∧ 𝑊) ≤ 𝑊) |
42 | 7, 8, 12, 17, 18, 19, 13 | dibelval3 36436 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑌 ∧ 𝑊) ∈ 𝐵 ∧ (𝑌 ∧ 𝑊) ≤ 𝑊)) → (𝑧 ∈ (𝐼‘(𝑌 ∧ 𝑊)) ↔ ∃𝑔 ∈ 𝑇 (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊)))) |
43 | 26, 39, 41, 42 | syl12anc 1324 |
. . . . . . . 8
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → (𝑧 ∈ (𝐼‘(𝑌 ∧ 𝑊)) ↔ ∃𝑔 ∈ 𝑇 (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊)))) |
44 | 29, 43 | anbi12d 747 |
. . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → ((𝑦 ∈ (𝐽‘𝑁) ∧ 𝑧 ∈ (𝐼‘(𝑌 ∧ 𝑊))) ↔ (∃𝑠 ∈ 𝐸 𝑦 = 〈(𝑠‘𝐺), 𝑠〉 ∧ ∃𝑔 ∈ 𝑇 (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊))))) |
45 | | reeanv 3107 |
. . . . . . . 8
⊢
(∃𝑠 ∈
𝐸 ∃𝑔 ∈ 𝑇 (𝑦 = 〈(𝑠‘𝐺), 𝑠〉 ∧ (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊))) ↔ (∃𝑠 ∈ 𝐸 𝑦 = 〈(𝑠‘𝐺), 𝑠〉 ∧ ∃𝑔 ∈ 𝑇 (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊)))) |
46 | | simpll1 1100 |
. . . . . . . . . . . 12
⊢
((((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) ∧ 〈𝑓, 𝑂〉 = (〈(𝑠‘𝐺), 𝑠〉 + 〈𝑔, 𝑂〉))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊))) |
47 | | simplr 792 |
. . . . . . . . . . . 12
⊢
((((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) ∧ 〈𝑓, 𝑂〉 = (〈(𝑠‘𝐺), 𝑠〉 + 〈𝑔, 𝑂〉))) → (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) |
48 | | simpr 477 |
. . . . . . . . . . . 12
⊢
((((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) ∧ 〈𝑓, 𝑂〉 = (〈(𝑠‘𝐺), 𝑠〉 + 〈𝑔, 𝑂〉))) → ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) ∧ 〈𝑓, 𝑂〉 = (〈(𝑠‘𝐺), 𝑠〉 + 〈𝑔, 𝑂〉))) |
49 | 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 | dihord10 36512 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) ∧ 〈𝑓, 𝑂〉 = (〈(𝑠‘𝐺), 𝑠〉 + 〈𝑔, 𝑂〉))) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊)) |
50 | 46, 47, 48, 49 | syl3anc 1326 |
. . . . . . . . . . 11
⊢
((((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) ∧ 〈𝑓, 𝑂〉 = (〈(𝑠‘𝐺), 𝑠〉 + 〈𝑔, 𝑂〉))) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊)) |
51 | 50 | 3exp2 1285 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) → ((𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) → (〈𝑓, 𝑂〉 = (〈(𝑠‘𝐺), 𝑠〉 + 〈𝑔, 𝑂〉) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊))))) |
52 | | oveq12 6659 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 = 〈(𝑠‘𝐺), 𝑠〉 ∧ 𝑧 = 〈𝑔, 𝑂〉) → (𝑦 + 𝑧) = (〈(𝑠‘𝐺), 𝑠〉 + 〈𝑔, 𝑂〉)) |
53 | 52 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 = 〈(𝑠‘𝐺), 𝑠〉 ∧ 𝑧 = 〈𝑔, 𝑂〉) → (〈𝑓, 𝑂〉 = (𝑦 + 𝑧) ↔ 〈𝑓, 𝑂〉 = (〈(𝑠‘𝐺), 𝑠〉 + 〈𝑔, 𝑂〉))) |
54 | 53 | imbi1d 331 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 = 〈(𝑠‘𝐺), 𝑠〉 ∧ 𝑧 = 〈𝑔, 𝑂〉) → ((〈𝑓, 𝑂〉 = (𝑦 + 𝑧) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊)) ↔ (〈𝑓, 𝑂〉 = (〈(𝑠‘𝐺), 𝑠〉 + 〈𝑔, 𝑂〉) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊)))) |
55 | 54 | imbi2d 330 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 〈(𝑠‘𝐺), 𝑠〉 ∧ 𝑧 = 〈𝑔, 𝑂〉) → (((𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) → (〈𝑓, 𝑂〉 = (𝑦 + 𝑧) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊))) ↔ ((𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) → (〈𝑓, 𝑂〉 = (〈(𝑠‘𝐺), 𝑠〉 + 〈𝑔, 𝑂〉) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊))))) |
56 | 55 | biimprd 238 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 〈(𝑠‘𝐺), 𝑠〉 ∧ 𝑧 = 〈𝑔, 𝑂〉) → (((𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) → (〈𝑓, 𝑂〉 = (〈(𝑠‘𝐺), 𝑠〉 + 〈𝑔, 𝑂〉) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊))) → ((𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) → (〈𝑓, 𝑂〉 = (𝑦 + 𝑧) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊))))) |
57 | 56 | com23 86 |
. . . . . . . . . . . 12
⊢ ((𝑦 = 〈(𝑠‘𝐺), 𝑠〉 ∧ 𝑧 = 〈𝑔, 𝑂〉) → ((𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) → (((𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) → (〈𝑓, 𝑂〉 = (〈(𝑠‘𝐺), 𝑠〉 + 〈𝑔, 𝑂〉) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊))) → (〈𝑓, 𝑂〉 = (𝑦 + 𝑧) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊))))) |
58 | 57 | impr 649 |
. . . . . . . . . . 11
⊢ ((𝑦 = 〈(𝑠‘𝐺), 𝑠〉 ∧ (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊))) → (((𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) → (〈𝑓, 𝑂〉 = (〈(𝑠‘𝐺), 𝑠〉 + 〈𝑔, 𝑂〉) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊))) → (〈𝑓, 𝑂〉 = (𝑦 + 𝑧) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊)))) |
59 | 58 | com12 32 |
. . . . . . . . . 10
⊢ (((𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊) → (〈𝑓, 𝑂〉 = (〈(𝑠‘𝐺), 𝑠〉 + 〈𝑔, 𝑂〉) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊))) → ((𝑦 = 〈(𝑠‘𝐺), 𝑠〉 ∧ (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊))) → (〈𝑓, 𝑂〉 = (𝑦 + 𝑧) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊)))) |
60 | 51, 59 | syl6 35 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) → ((𝑦 = 〈(𝑠‘𝐺), 𝑠〉 ∧ (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊))) → (〈𝑓, 𝑂〉 = (𝑦 + 𝑧) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊))))) |
61 | 60 | rexlimdvv 3037 |
. . . . . . . 8
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → (∃𝑠 ∈ 𝐸 ∃𝑔 ∈ 𝑇 (𝑦 = 〈(𝑠‘𝐺), 𝑠〉 ∧ (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊))) → (〈𝑓, 𝑂〉 = (𝑦 + 𝑧) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊)))) |
62 | 45, 61 | syl5bir 233 |
. . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → ((∃𝑠 ∈ 𝐸 𝑦 = 〈(𝑠‘𝐺), 𝑠〉 ∧ ∃𝑔 ∈ 𝑇 (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ (𝑌 ∧ 𝑊))) → (〈𝑓, 𝑂〉 = (𝑦 + 𝑧) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊)))) |
63 | 44, 62 | sylbid 230 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → ((𝑦 ∈ (𝐽‘𝑁) ∧ 𝑧 ∈ (𝐼‘(𝑌 ∧ 𝑊))) → (〈𝑓, 𝑂〉 = (𝑦 + 𝑧) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊)))) |
64 | 63 | rexlimdvv 3037 |
. . . . 5
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → (∃𝑦 ∈ (𝐽‘𝑁)∃𝑧 ∈ (𝐼‘(𝑌 ∧ 𝑊))〈𝑓, 𝑂〉 = (𝑦 + 𝑧) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊))) |
65 | 25, 64 | mpd 15 |
. . . 4
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊)) |
66 | 65 | exp32 631 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → (𝑓 ∈ 𝑇 → ((𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊)))) |
67 | 66 | ralrimiv 2965 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → ∀𝑓 ∈ 𝑇 ((𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊))) |
68 | | simp11 1091 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
69 | 30, 32 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → 𝐾 ∈ Lat) |
70 | | simp2l 1087 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → 𝑋 ∈ 𝐵) |
71 | 34, 36 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → 𝑊 ∈ 𝐵) |
72 | 7, 10 | latmcl 17052 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵) |
73 | 69, 70, 71, 72 | syl3anc 1326 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → (𝑋 ∧ 𝑊) ∈ 𝐵) |
74 | 7, 8, 10 | latmle2 17077 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑊) |
75 | 69, 70, 71, 74 | syl3anc 1326 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → (𝑋 ∧ 𝑊) ≤ 𝑊) |
76 | | simp2r 1088 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → 𝑌 ∈ 𝐵) |
77 | 69, 76, 71, 38 | syl3anc 1326 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → (𝑌 ∧ 𝑊) ∈ 𝐵) |
78 | 69, 76, 71, 40 | syl3anc 1326 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → (𝑌 ∧ 𝑊) ≤ 𝑊) |
79 | 7, 8, 11, 12, 17, 18 | trlord 35857 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊) ∧ ((𝑌 ∧ 𝑊) ∈ 𝐵 ∧ (𝑌 ∧ 𝑊) ≤ 𝑊)) → ((𝑋 ∧ 𝑊) ≤ (𝑌 ∧ 𝑊) ↔ ∀𝑓 ∈ 𝑇 ((𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊)))) |
80 | 68, 73, 75, 77, 78, 79 | syl122anc 1335 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → ((𝑋 ∧ 𝑊) ≤ (𝑌 ∧ 𝑊) ↔ ∀𝑓 ∈ 𝑇 ((𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊) → (𝑅‘𝑓) ≤ (𝑌 ∧ 𝑊)))) |
81 | 67, 80 | mpbird 247 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑁) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) → (𝑋 ∧ 𝑊) ≤ (𝑌 ∧ 𝑊)) |