Step | Hyp | Ref
| Expression |
1 | | dihmeetlem4.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | dihmeetlem4.i |
. . . . 5
⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
3 | 1, 2 | dihvalrel 36568 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘𝑄)) |
4 | | relin1 5236 |
. . . 4
⊢ (Rel
(𝐼‘𝑄) → Rel ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊)))) |
5 | 3, 4 | syl 17 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊)))) |
6 | 5 | 3ad2ant1 1082 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → Rel ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊)))) |
7 | 1, 2 | dihvalrel 36568 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘(0.‘𝐾))) |
8 | | eqid 2622 |
. . . . . 6
⊢
(0.‘𝐾) =
(0.‘𝐾) |
9 | | dihmeetlem4.u |
. . . . . 6
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
10 | | dihmeetlem4.z |
. . . . . 6
⊢ 0 =
(0g‘𝑈) |
11 | 8, 1, 2, 9, 10 | dih0 36569 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐼‘(0.‘𝐾)) = { 0 }) |
12 | 11 | releqd 5203 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Rel (𝐼‘(0.‘𝐾)) ↔ Rel { 0 })) |
13 | 7, 12 | mpbid 222 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel { 0 }) |
14 | 13 | 3ad2ant1 1082 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → Rel { 0 }) |
15 | | id 22 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) |
16 | | elin 3796 |
. . . 4
⊢
(〈𝑓, 𝑠〉 ∈ ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))) ↔ (〈𝑓, 𝑠〉 ∈ (𝐼‘𝑄) ∧ 〈𝑓, 𝑠〉 ∈ (𝐼‘(𝑋 ∧ 𝑊)))) |
17 | | dihmeetlem4.l |
. . . . . . . . . 10
⊢ ≤ =
(le‘𝐾) |
18 | | dihmeetlem4.a |
. . . . . . . . . 10
⊢ 𝐴 = (Atoms‘𝐾) |
19 | | dihmeetlem4.p |
. . . . . . . . . 10
⊢ 𝑃 = ((oc‘𝐾)‘𝑊) |
20 | | dihmeetlem4.t |
. . . . . . . . . 10
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
21 | | dihmeetlem4.e |
. . . . . . . . . 10
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
22 | | dihmeetlem4.g |
. . . . . . . . . 10
⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄) |
23 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑓 ∈ V |
24 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑠 ∈ V |
25 | 17, 18, 1, 19, 20, 21, 2, 22, 23, 24 | dihopelvalcqat 36535 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (〈𝑓, 𝑠〉 ∈ (𝐼‘𝑄) ↔ (𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸))) |
26 | 25 | 3adant2 1080 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (〈𝑓, 𝑠〉 ∈ (𝐼‘𝑄) ↔ (𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸))) |
27 | | simp1 1061 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
28 | | simp1l 1085 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐾 ∈ HL) |
29 | | hllat 34650 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
30 | 28, 29 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐾 ∈ Lat) |
31 | | simp2l 1087 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝑋 ∈ 𝐵) |
32 | | simp1r 1086 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝑊 ∈ 𝐻) |
33 | | dihmeetlem4.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝐾) |
34 | 33, 1 | lhpbase 35284 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
35 | 32, 34 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝑊 ∈ 𝐵) |
36 | | dihmeetlem4.m |
. . . . . . . . . . 11
⊢ ∧ =
(meet‘𝐾) |
37 | 33, 36 | latmcl 17052 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵) |
38 | 30, 31, 35, 37 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑋 ∧ 𝑊) ∈ 𝐵) |
39 | 33, 17, 36 | latmle2 17077 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑊) |
40 | 30, 31, 35, 39 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑋 ∧ 𝑊) ≤ 𝑊) |
41 | | dihmeetlem4.r |
. . . . . . . . . 10
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
42 | | dihmeetlem4.o |
. . . . . . . . . 10
⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) |
43 | 33, 17, 1, 20, 41, 42, 2 | dihopelvalbN 36527 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊)) → (〈𝑓, 𝑠〉 ∈ (𝐼‘(𝑋 ∧ 𝑊)) ↔ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) |
44 | 27, 38, 40, 43 | syl12anc 1324 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (〈𝑓, 𝑠〉 ∈ (𝐼‘(𝑋 ∧ 𝑊)) ↔ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) |
45 | 26, 44 | anbi12d 747 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((〈𝑓, 𝑠〉 ∈ (𝐼‘𝑄) ∧ 〈𝑓, 𝑠〉 ∈ (𝐼‘(𝑋 ∧ 𝑊))) ↔ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂)))) |
46 | | simprll 802 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → 𝑓 = (𝑠‘𝐺)) |
47 | | simprrr 805 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → 𝑠 = 𝑂) |
48 | 47 | fveq1d 6193 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → (𝑠‘𝐺) = (𝑂‘𝐺)) |
49 | | simpl1 1064 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
50 | 17, 18, 1, 19 | lhpocnel2 35305 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
52 | | simpl3 1066 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
53 | 17, 18, 1, 20, 22 | ltrniotacl 35867 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐺 ∈ 𝑇) |
54 | 49, 51, 52, 53 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → 𝐺 ∈ 𝑇) |
55 | 42, 33 | tendo02 36075 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ 𝑇 → (𝑂‘𝐺) = ( I ↾ 𝐵)) |
56 | 54, 55 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → (𝑂‘𝐺) = ( I ↾ 𝐵)) |
57 | 46, 48, 56 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → 𝑓 = ( I ↾ 𝐵)) |
58 | 57, 47 | jca 554 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) → (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) |
59 | | simpl1 1064 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
60 | 59, 50 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
61 | | simpl3 1066 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
62 | 59, 60, 61, 53 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝐺 ∈ 𝑇) |
63 | 62, 55 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑂‘𝐺) = ( I ↾ 𝐵)) |
64 | | simprr 796 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝑠 = 𝑂) |
65 | 64 | fveq1d 6193 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑠‘𝐺) = (𝑂‘𝐺)) |
66 | | simprl 794 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝑓 = ( I ↾ 𝐵)) |
67 | 63, 65, 66 | 3eqtr4rd 2667 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝑓 = (𝑠‘𝐺)) |
68 | 33, 1, 20, 21, 42 | tendo0cl 36078 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑂 ∈ 𝐸) |
69 | 59, 68 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝑂 ∈ 𝐸) |
70 | 64, 69 | eqeltrd 2701 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝑠 ∈ 𝐸) |
71 | 33, 1, 20 | idltrn 35436 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝐵) ∈ 𝑇) |
72 | 59, 71 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → ( I ↾ 𝐵) ∈ 𝑇) |
73 | 66, 72 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝑓 ∈ 𝑇) |
74 | 66 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑅‘𝑓) = (𝑅‘( I ↾ 𝐵))) |
75 | 33, 8, 1, 41 | trlid0 35463 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑅‘( I ↾ 𝐵)) = (0.‘𝐾)) |
76 | 59, 75 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑅‘( I ↾ 𝐵)) = (0.‘𝐾)) |
77 | 74, 76 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑅‘𝑓) = (0.‘𝐾)) |
78 | | simpl1l 1112 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝐾 ∈ HL) |
79 | | hlatl 34647 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → 𝐾 ∈ AtLat) |
81 | 38 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑋 ∧ 𝑊) ∈ 𝐵) |
82 | 33, 17, 8 | atl0le 34591 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ AtLat ∧ (𝑋 ∧ 𝑊) ∈ 𝐵) → (0.‘𝐾) ≤ (𝑋 ∧ 𝑊)) |
83 | 80, 81, 82 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (0.‘𝐾) ≤ (𝑋 ∧ 𝑊)) |
84 | 77, 83 | eqbrtrd 4675 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) |
85 | 73, 84, 64 | jca31 557 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂)) |
86 | 67, 70, 85 | jca31 557 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) → ((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂))) |
87 | 58, 86 | impbida 877 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (((𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸) ∧ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑠 = 𝑂)) ↔ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂))) |
88 | 45, 87 | bitrd 268 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((〈𝑓, 𝑠〉 ∈ (𝐼‘𝑄) ∧ 〈𝑓, 𝑠〉 ∈ (𝐼‘(𝑋 ∧ 𝑊))) ↔ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂))) |
89 | | opex 4932 |
. . . . . . . 8
⊢
〈𝑓, 𝑠〉 ∈ V |
90 | 89 | elsn 4192 |
. . . . . . 7
⊢
(〈𝑓, 𝑠〉 ∈ {〈( I ↾
𝐵), 𝑂〉} ↔ 〈𝑓, 𝑠〉 = 〈( I ↾ 𝐵), 𝑂〉) |
91 | 23, 24 | opth 4945 |
. . . . . . 7
⊢
(〈𝑓, 𝑠〉 = 〈( I ↾ 𝐵), 𝑂〉 ↔ (𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂)) |
92 | 90, 91 | bitr2i 265 |
. . . . . 6
⊢ ((𝑓 = ( I ↾ 𝐵) ∧ 𝑠 = 𝑂) ↔ 〈𝑓, 𝑠〉 ∈ {〈( I ↾ 𝐵), 𝑂〉}) |
93 | 88, 92 | syl6bb 276 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((〈𝑓, 𝑠〉 ∈ (𝐼‘𝑄) ∧ 〈𝑓, 𝑠〉 ∈ (𝐼‘(𝑋 ∧ 𝑊))) ↔ 〈𝑓, 𝑠〉 ∈ {〈( I ↾ 𝐵), 𝑂〉})) |
94 | 33, 1, 20, 9, 10, 42 | dvh0g 36400 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 0 = 〈( I ↾ 𝐵), 𝑂〉) |
95 | 94 | 3ad2ant1 1082 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 0 = 〈( I ↾ 𝐵), 𝑂〉) |
96 | 95 | sneqd 4189 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → { 0 } = {〈( I ↾
𝐵), 𝑂〉}) |
97 | 96 | eleq2d 2687 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (〈𝑓, 𝑠〉 ∈ { 0 } ↔ 〈𝑓, 𝑠〉 ∈ {〈( I ↾ 𝐵), 𝑂〉})) |
98 | 93, 97 | bitr4d 271 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((〈𝑓, 𝑠〉 ∈ (𝐼‘𝑄) ∧ 〈𝑓, 𝑠〉 ∈ (𝐼‘(𝑋 ∧ 𝑊))) ↔ 〈𝑓, 𝑠〉 ∈ { 0 })) |
99 | 16, 98 | syl5bb 272 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (〈𝑓, 𝑠〉 ∈ ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))) ↔ 〈𝑓, 𝑠〉 ∈ { 0 })) |
100 | 99 | eqrelrdv2 5219 |
. 2
⊢ (((Rel
((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))) ∧ Rel { 0 }) ∧ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))) = { 0 }) |
101 | 6, 14, 15, 100 | syl21anc 1325 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))) = { 0 }) |