Step | Hyp | Ref
| Expression |
1 | | diaval.i |
. . 3
⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) |
2 | | diaval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐾) |
3 | | diaval.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
4 | | diaval.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
5 | 2, 3, 4 | diaffval 35337 |
. . . 4
⊢ (𝐾 ∈ 𝑉 → (DIsoA‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥}))) |
6 | 5 | fveq1d 6105 |
. . 3
⊢ (𝐾 ∈ 𝑉 → ((DIsoA‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥}))‘𝑊)) |
7 | 1, 6 | syl5eq 2656 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐼 = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥}))‘𝑊)) |
8 | | breq2 4587 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑦 ≤ 𝑤 ↔ 𝑦 ≤ 𝑊)) |
9 | 8 | rabbidv 3164 |
. . . 4
⊢ (𝑤 = 𝑊 → {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} = {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑊}) |
10 | | fveq2 6103 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊)) |
11 | | diaval.t |
. . . . . 6
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
12 | 10, 11 | syl6eqr 2662 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = 𝑇) |
13 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((trL‘𝐾)‘𝑤) = ((trL‘𝐾)‘𝑊)) |
14 | | diaval.r |
. . . . . . . 8
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
15 | 13, 14 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((trL‘𝐾)‘𝑤) = 𝑅) |
16 | 15 | fveq1d 6105 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (((trL‘𝐾)‘𝑤)‘𝑓) = (𝑅‘𝑓)) |
17 | 16 | breq1d 4593 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥 ↔ (𝑅‘𝑓) ≤ 𝑥)) |
18 | 12, 17 | rabeqbidv 3168 |
. . . 4
⊢ (𝑤 = 𝑊 → {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥} = {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ 𝑥}) |
19 | 9, 18 | mpteq12dv 4663 |
. . 3
⊢ (𝑤 = 𝑊 → (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥}) = (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑊} ↦ {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ 𝑥})) |
20 | | eqid 2610 |
. . 3
⊢ (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥})) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥})) |
21 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝐾)
∈ V |
22 | 2, 21 | eqeltri 2684 |
. . . 4
⊢ 𝐵 ∈ V |
23 | 22 | mptrabex 6392 |
. . 3
⊢ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑊} ↦ {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ 𝑥}) ∈ V |
24 | 19, 20, 23 | fvmpt 6191 |
. 2
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥}))‘𝑊) = (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑊} ↦ {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ 𝑥})) |
25 | 7, 24 | sylan9eq 2664 |
1
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑊} ↦ {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ 𝑥})) |