Step | Hyp | Ref
| Expression |
1 | | cdlemn11a.b |
. . 3
⊢ 𝐵 = (Base‘𝐾) |
2 | | cdlemn11a.l |
. . 3
⊢ ≤ =
(le‘𝐾) |
3 | | cdlemn11a.j |
. . 3
⊢ ∨ =
(join‘𝐾) |
4 | | cdlemn11a.a |
. . 3
⊢ 𝐴 = (Atoms‘𝐾) |
5 | | cdlemn11a.h |
. . 3
⊢ 𝐻 = (LHyp‘𝐾) |
6 | | cdlemn11a.p |
. . 3
⊢ 𝑃 = ((oc‘𝐾)‘𝑊) |
7 | | cdlemn11a.o |
. . 3
⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) |
8 | | cdlemn11a.t |
. . 3
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
9 | | cdlemn11a.r |
. . 3
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
10 | | cdlemn11a.e |
. . 3
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
11 | | cdlemn11a.i |
. . 3
⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) |
12 | | cdlemn11a.J |
. . 3
⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊) |
13 | | cdlemn11a.u |
. . 3
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
14 | | cdlemn11a.d |
. . 3
⊢ + =
(+g‘𝑈) |
15 | | cdlemn11a.s |
. . 3
⊢ ⊕ =
(LSSum‘𝑈) |
16 | | cdlemn11a.f |
. . 3
⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄) |
17 | | cdlemn11a.g |
. . 3
⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁) |
18 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17 | cdlemn11c 38846 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ∃𝑦 ∈ (𝐽‘𝑄)∃𝑧 ∈ (𝐼‘𝑋)〈𝐺, ( I ↾ 𝑇)〉 = (𝑦 + 𝑧)) |
19 | | simp1 1137 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
20 | | simp21 1207 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
21 | 2, 4, 5, 6, 8, 10,
12, 16 | dicelval3 38817 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑦 ∈ (𝐽‘𝑄) ↔ ∃𝑠 ∈ 𝐸 𝑦 = 〈(𝑠‘𝐹), 𝑠〉)) |
22 | 19, 20, 21 | syl2anc 587 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (𝑦 ∈ (𝐽‘𝑄) ↔ ∃𝑠 ∈ 𝐸 𝑦 = 〈(𝑠‘𝐹), 𝑠〉)) |
23 | | simp23 1209 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) |
24 | 1, 2, 5, 8, 9, 7, 11 | dibelval3 38784 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑧 ∈ (𝐼‘𝑋) ↔ ∃𝑔 ∈ 𝑇 (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ 𝑋))) |
25 | 19, 23, 24 | syl2anc 587 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (𝑧 ∈ (𝐼‘𝑋) ↔ ∃𝑔 ∈ 𝑇 (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ 𝑋))) |
26 | 22, 25 | anbi12d 634 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ((𝑦 ∈ (𝐽‘𝑄) ∧ 𝑧 ∈ (𝐼‘𝑋)) ↔ (∃𝑠 ∈ 𝐸 𝑦 = 〈(𝑠‘𝐹), 𝑠〉 ∧ ∃𝑔 ∈ 𝑇 (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ 𝑋)))) |
27 | | reeanv 3270 |
. . . . 5
⊢
(∃𝑠 ∈
𝐸 ∃𝑔 ∈ 𝑇 (𝑦 = 〈(𝑠‘𝐹), 𝑠〉 ∧ (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ 𝑋)) ↔ (∃𝑠 ∈ 𝐸 𝑦 = 〈(𝑠‘𝐹), 𝑠〉 ∧ ∃𝑔 ∈ 𝑇 (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ 𝑋))) |
28 | | simpl1 1192 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ 𝑋 ∧ 〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
29 | | simpl21 1252 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ 𝑋 ∧ 〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
30 | | simpl22 1253 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ 𝑋 ∧ 〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉))) → (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) |
31 | | simpl23 1254 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ 𝑋 ∧ 〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉))) → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) |
32 | | simpr1r 1232 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ 𝑋 ∧ 〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉))) → 𝑔 ∈ 𝑇) |
33 | | simpr1l 1231 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ 𝑋 ∧ 〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉))) → 𝑠 ∈ 𝐸) |
34 | | simpr3 1197 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ 𝑋 ∧ 〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉))) → 〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉)) |
35 | 1, 2, 4, 5, 6, 7, 8, 10, 13, 14, 16, 17 | cdlemn9 38842 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ 〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉))) → (𝑔‘𝑄) = 𝑁) |
36 | 28, 29, 30, 33, 32, 34, 35 | syl123anc 1388 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ 𝑋 ∧ 〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉))) → (𝑔‘𝑄) = 𝑁) |
37 | | simpr2 1196 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ 𝑋 ∧ 〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉))) → (𝑅‘𝑔) ≤ 𝑋) |
38 | 1, 2, 3, 4, 5, 8, 9 | cdlemn10 38843 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑄) = 𝑁 ∧ (𝑅‘𝑔) ≤ 𝑋)) → 𝑁 ≤ (𝑄 ∨ 𝑋)) |
39 | 28, 29, 30, 31, 32, 36, 37, 38 | syl133anc 1394 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) ∧ ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) ∧ (𝑅‘𝑔) ≤ 𝑋 ∧ 〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉))) → 𝑁 ≤ (𝑄 ∨ 𝑋)) |
40 | 39 | 3exp2 1355 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) → ((𝑅‘𝑔) ≤ 𝑋 → (〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉) → 𝑁 ≤ (𝑄 ∨ 𝑋))))) |
41 | | oveq12 7179 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 〈(𝑠‘𝐹), 𝑠〉 ∧ 𝑧 = 〈𝑔, 𝑂〉) → (𝑦 + 𝑧) = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉)) |
42 | 41 | eqeq2d 2749 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 〈(𝑠‘𝐹), 𝑠〉 ∧ 𝑧 = 〈𝑔, 𝑂〉) → (〈𝐺, ( I ↾ 𝑇)〉 = (𝑦 + 𝑧) ↔ 〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉))) |
43 | 42 | imbi1d 345 |
. . . . . . . . . . . 12
⊢ ((𝑦 = 〈(𝑠‘𝐹), 𝑠〉 ∧ 𝑧 = 〈𝑔, 𝑂〉) → ((〈𝐺, ( I ↾ 𝑇)〉 = (𝑦 + 𝑧) → 𝑁 ≤ (𝑄 ∨ 𝑋)) ↔ (〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉) → 𝑁 ≤ (𝑄 ∨ 𝑋)))) |
44 | 43 | imbi2d 344 |
. . . . . . . . . . 11
⊢ ((𝑦 = 〈(𝑠‘𝐹), 𝑠〉 ∧ 𝑧 = 〈𝑔, 𝑂〉) → (((𝑅‘𝑔) ≤ 𝑋 → (〈𝐺, ( I ↾ 𝑇)〉 = (𝑦 + 𝑧) → 𝑁 ≤ (𝑄 ∨ 𝑋))) ↔ ((𝑅‘𝑔) ≤ 𝑋 → (〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉) → 𝑁 ≤ (𝑄 ∨ 𝑋))))) |
45 | 44 | biimprd 251 |
. . . . . . . . . 10
⊢ ((𝑦 = 〈(𝑠‘𝐹), 𝑠〉 ∧ 𝑧 = 〈𝑔, 𝑂〉) → (((𝑅‘𝑔) ≤ 𝑋 → (〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉) → 𝑁 ≤ (𝑄 ∨ 𝑋))) → ((𝑅‘𝑔) ≤ 𝑋 → (〈𝐺, ( I ↾ 𝑇)〉 = (𝑦 + 𝑧) → 𝑁 ≤ (𝑄 ∨ 𝑋))))) |
46 | 45 | com23 86 |
. . . . . . . . 9
⊢ ((𝑦 = 〈(𝑠‘𝐹), 𝑠〉 ∧ 𝑧 = 〈𝑔, 𝑂〉) → ((𝑅‘𝑔) ≤ 𝑋 → (((𝑅‘𝑔) ≤ 𝑋 → (〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉) → 𝑁 ≤ (𝑄 ∨ 𝑋))) → (〈𝐺, ( I ↾ 𝑇)〉 = (𝑦 + 𝑧) → 𝑁 ≤ (𝑄 ∨ 𝑋))))) |
47 | 46 | impr 458 |
. . . . . . . 8
⊢ ((𝑦 = 〈(𝑠‘𝐹), 𝑠〉 ∧ (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ 𝑋)) → (((𝑅‘𝑔) ≤ 𝑋 → (〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉) → 𝑁 ≤ (𝑄 ∨ 𝑋))) → (〈𝐺, ( I ↾ 𝑇)〉 = (𝑦 + 𝑧) → 𝑁 ≤ (𝑄 ∨ 𝑋)))) |
48 | 47 | com12 32 |
. . . . . . 7
⊢ (((𝑅‘𝑔) ≤ 𝑋 → (〈𝐺, ( I ↾ 𝑇)〉 = (〈(𝑠‘𝐹), 𝑠〉 + 〈𝑔, 𝑂〉) → 𝑁 ≤ (𝑄 ∨ 𝑋))) → ((𝑦 = 〈(𝑠‘𝐹), 𝑠〉 ∧ (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ 𝑋)) → (〈𝐺, ( I ↾ 𝑇)〉 = (𝑦 + 𝑧) → 𝑁 ≤ (𝑄 ∨ 𝑋)))) |
49 | 40, 48 | syl6 35 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ((𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) → ((𝑦 = 〈(𝑠‘𝐹), 𝑠〉 ∧ (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ 𝑋)) → (〈𝐺, ( I ↾ 𝑇)〉 = (𝑦 + 𝑧) → 𝑁 ≤ (𝑄 ∨ 𝑋))))) |
50 | 49 | rexlimdvv 3203 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (∃𝑠 ∈ 𝐸 ∃𝑔 ∈ 𝑇 (𝑦 = 〈(𝑠‘𝐹), 𝑠〉 ∧ (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ 𝑋)) → (〈𝐺, ( I ↾ 𝑇)〉 = (𝑦 + 𝑧) → 𝑁 ≤ (𝑄 ∨ 𝑋)))) |
51 | 27, 50 | syl5bir 246 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ((∃𝑠 ∈ 𝐸 𝑦 = 〈(𝑠‘𝐹), 𝑠〉 ∧ ∃𝑔 ∈ 𝑇 (𝑧 = 〈𝑔, 𝑂〉 ∧ (𝑅‘𝑔) ≤ 𝑋)) → (〈𝐺, ( I ↾ 𝑇)〉 = (𝑦 + 𝑧) → 𝑁 ≤ (𝑄 ∨ 𝑋)))) |
52 | 26, 51 | sylbid 243 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ((𝑦 ∈ (𝐽‘𝑄) ∧ 𝑧 ∈ (𝐼‘𝑋)) → (〈𝐺, ( I ↾ 𝑇)〉 = (𝑦 + 𝑧) → 𝑁 ≤ (𝑄 ∨ 𝑋)))) |
53 | 52 | rexlimdvv 3203 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (∃𝑦 ∈ (𝐽‘𝑄)∃𝑧 ∈ (𝐼‘𝑋)〈𝐺, ( I ↾ 𝑇)〉 = (𝑦 + 𝑧) → 𝑁 ≤ (𝑄 ∨ 𝑋))) |
54 | 18, 53 | mpd 15 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → 𝑁 ≤ (𝑄 ∨ 𝑋)) |