| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 2 | | dib1dim.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐾) |
| 3 | | dib1dim.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
| 4 | | dib1dim.t |
. . . . 5
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| 5 | | dib1dim.r |
. . . . 5
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
| 6 | 2, 3, 4, 5 | trlcl 40166 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) ∈ 𝐵) |
| 7 | | eqid 2737 |
. . . . 5
⊢
(le‘𝐾) =
(le‘𝐾) |
| 8 | 7, 3, 4, 5 | trlle 40186 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹)(le‘𝐾)𝑊) |
| 9 | | dib1dim.o |
. . . . 5
⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) |
| 10 | | eqid 2737 |
. . . . 5
⊢
((DIsoA‘𝐾)‘𝑊) = ((DIsoA‘𝐾)‘𝑊) |
| 11 | | dib1dim.i |
. . . . 5
⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) |
| 12 | 2, 7, 3, 4, 9, 10,
11 | dibval2 41146 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅‘𝐹) ∈ 𝐵 ∧ (𝑅‘𝐹)(le‘𝐾)𝑊)) → (𝐼‘(𝑅‘𝐹)) = ((((DIsoA‘𝐾)‘𝑊)‘(𝑅‘𝐹)) × {𝑂})) |
| 13 | 1, 6, 8, 12 | syl12anc 837 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐼‘(𝑅‘𝐹)) = ((((DIsoA‘𝐾)‘𝑊)‘(𝑅‘𝐹)) × {𝑂})) |
| 14 | | relxp 5703 |
. . . 4
⊢ Rel
((((DIsoA‘𝐾)‘𝑊)‘(𝑅‘𝐹)) × {𝑂}) |
| 15 | | opelxp 5721 |
. . . . 5
⊢
(〈𝑓, 𝑡〉 ∈
((((DIsoA‘𝐾)‘𝑊)‘(𝑅‘𝐹)) × {𝑂}) ↔ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘(𝑅‘𝐹)) ∧ 𝑡 ∈ {𝑂})) |
| 16 | | dib1dim.e |
. . . . . . . . 9
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
| 17 | 3, 4, 5, 16, 10 | dia1dim 41063 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (((DIsoA‘𝐾)‘𝑊)‘(𝑅‘𝐹)) = {𝑓 ∣ ∃𝑠 ∈ 𝐸 𝑓 = (𝑠‘𝐹)}) |
| 18 | 17 | eqabrd 2884 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘(𝑅‘𝐹)) ↔ ∃𝑠 ∈ 𝐸 𝑓 = (𝑠‘𝐹))) |
| 19 | 18 | anbi1d 631 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘(𝑅‘𝐹)) ∧ 𝑡 ∈ {𝑂}) ↔ (∃𝑠 ∈ 𝐸 𝑓 = (𝑠‘𝐹) ∧ 𝑡 ∈ {𝑂}))) |
| 20 | 3, 4, 16 | tendocl 40769 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑠‘𝐹) ∈ 𝑇) |
| 21 | 20 | 3expa 1119 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸) ∧ 𝐹 ∈ 𝑇) → (𝑠‘𝐹) ∈ 𝑇) |
| 22 | 21 | an32s 652 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑠 ∈ 𝐸) → (𝑠‘𝐹) ∈ 𝑇) |
| 23 | 2, 3, 4, 16, 9 | tendo0cl 40792 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑂 ∈ 𝐸) |
| 24 | 23 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑠 ∈ 𝐸) → 𝑂 ∈ 𝐸) |
| 25 | 22, 24 | jca 511 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑠 ∈ 𝐸) → ((𝑠‘𝐹) ∈ 𝑇 ∧ 𝑂 ∈ 𝐸)) |
| 26 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑠‘𝐹) → (𝑓 ∈ 𝑇 ↔ (𝑠‘𝐹) ∈ 𝑇)) |
| 27 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑂 → (𝑡 ∈ 𝐸 ↔ 𝑂 ∈ 𝐸)) |
| 28 | 26, 27 | bi2anan9 638 |
. . . . . . . . . 10
⊢ ((𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂) → ((𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸) ↔ ((𝑠‘𝐹) ∈ 𝑇 ∧ 𝑂 ∈ 𝐸))) |
| 29 | 25, 28 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑠 ∈ 𝐸) → ((𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂) → (𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸))) |
| 30 | 29 | rexlimdva 3155 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (∃𝑠 ∈ 𝐸 (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂) → (𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸))) |
| 31 | 30 | pm4.71rd 562 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (∃𝑠 ∈ 𝐸 (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸) ∧ ∃𝑠 ∈ 𝐸 (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂)))) |
| 32 | | velsn 4642 |
. . . . . . . . 9
⊢ (𝑡 ∈ {𝑂} ↔ 𝑡 = 𝑂) |
| 33 | 32 | anbi2i 623 |
. . . . . . . 8
⊢
((∃𝑠 ∈
𝐸 𝑓 = (𝑠‘𝐹) ∧ 𝑡 ∈ {𝑂}) ↔ (∃𝑠 ∈ 𝐸 𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂)) |
| 34 | | r19.41v 3189 |
. . . . . . . 8
⊢
(∃𝑠 ∈
𝐸 (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂) ↔ (∃𝑠 ∈ 𝐸 𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂)) |
| 35 | 33, 34 | bitr4i 278 |
. . . . . . 7
⊢
((∃𝑠 ∈
𝐸 𝑓 = (𝑠‘𝐹) ∧ 𝑡 ∈ {𝑂}) ↔ ∃𝑠 ∈ 𝐸 (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂)) |
| 36 | | df-3an 1089 |
. . . . . . 7
⊢ ((𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ∧ ∃𝑠 ∈ 𝐸 (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸) ∧ ∃𝑠 ∈ 𝐸 (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂))) |
| 37 | 31, 35, 36 | 3bitr4g 314 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((∃𝑠 ∈ 𝐸 𝑓 = (𝑠‘𝐹) ∧ 𝑡 ∈ {𝑂}) ↔ (𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ∧ ∃𝑠 ∈ 𝐸 (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂)))) |
| 38 | 19, 37 | bitrd 279 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘(𝑅‘𝐹)) ∧ 𝑡 ∈ {𝑂}) ↔ (𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ∧ ∃𝑠 ∈ 𝐸 (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂)))) |
| 39 | 15, 38 | bitrid 283 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (〈𝑓, 𝑡〉 ∈ ((((DIsoA‘𝐾)‘𝑊)‘(𝑅‘𝐹)) × {𝑂}) ↔ (𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ∧ ∃𝑠 ∈ 𝐸 (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂)))) |
| 40 | 14, 39 | opabbi2dv 5860 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((((DIsoA‘𝐾)‘𝑊)‘(𝑅‘𝐹)) × {𝑂}) = {〈𝑓, 𝑡〉 ∣ (𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ∧ ∃𝑠 ∈ 𝐸 (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂))}) |
| 41 | 13, 40 | eqtrd 2777 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐼‘(𝑅‘𝐹)) = {〈𝑓, 𝑡〉 ∣ (𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ∧ ∃𝑠 ∈ 𝐸 (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂))}) |
| 42 | | eqeq1 2741 |
. . . . 5
⊢ (𝑔 = 〈𝑓, 𝑡〉 → (𝑔 = 〈(𝑠‘𝐹), 𝑂〉 ↔ 〈𝑓, 𝑡〉 = 〈(𝑠‘𝐹), 𝑂〉)) |
| 43 | | vex 3484 |
. . . . . 6
⊢ 𝑓 ∈ V |
| 44 | | vex 3484 |
. . . . . 6
⊢ 𝑡 ∈ V |
| 45 | 43, 44 | opth 5481 |
. . . . 5
⊢
(〈𝑓, 𝑡〉 = 〈(𝑠‘𝐹), 𝑂〉 ↔ (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂)) |
| 46 | 42, 45 | bitrdi 287 |
. . . 4
⊢ (𝑔 = 〈𝑓, 𝑡〉 → (𝑔 = 〈(𝑠‘𝐹), 𝑂〉 ↔ (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂))) |
| 47 | 46 | rexbidv 3179 |
. . 3
⊢ (𝑔 = 〈𝑓, 𝑡〉 → (∃𝑠 ∈ 𝐸 𝑔 = 〈(𝑠‘𝐹), 𝑂〉 ↔ ∃𝑠 ∈ 𝐸 (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂))) |
| 48 | 47 | rabxp 5733 |
. 2
⊢ {𝑔 ∈ (𝑇 × 𝐸) ∣ ∃𝑠 ∈ 𝐸 𝑔 = 〈(𝑠‘𝐹), 𝑂〉} = {〈𝑓, 𝑡〉 ∣ (𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ∧ ∃𝑠 ∈ 𝐸 (𝑓 = (𝑠‘𝐹) ∧ 𝑡 = 𝑂))} |
| 49 | 41, 48 | eqtr4di 2795 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐼‘(𝑅‘𝐹)) = {𝑔 ∈ (𝑇 × 𝐸) ∣ ∃𝑠 ∈ 𝐸 𝑔 = 〈(𝑠‘𝐹), 𝑂〉}) |