Step | Hyp | Ref
| Expression |
1 | | elex 3449 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ V) |
2 | | fveq2 6769 |
. . . . 5
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾)) |
3 | | dochval.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
4 | 2, 3 | eqtr4di 2798 |
. . . 4
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻) |
5 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (DVecH‘𝑘) = (DVecH‘𝐾)) |
6 | 5 | fveq1d 6771 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ((DVecH‘𝑘)‘𝑤) = ((DVecH‘𝐾)‘𝑤)) |
7 | 6 | fveq2d 6773 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (Base‘((DVecH‘𝑘)‘𝑤)) = (Base‘((DVecH‘𝐾)‘𝑤))) |
8 | 7 | pweqd 4558 |
. . . . 5
⊢ (𝑘 = 𝐾 → 𝒫
(Base‘((DVecH‘𝑘)‘𝑤)) = 𝒫
(Base‘((DVecH‘𝐾)‘𝑤))) |
9 | | fveq2 6769 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (DIsoH‘𝑘) = (DIsoH‘𝐾)) |
10 | 9 | fveq1d 6771 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ((DIsoH‘𝑘)‘𝑤) = ((DIsoH‘𝐾)‘𝑤)) |
11 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (oc‘𝑘) = (oc‘𝐾)) |
12 | | dochval.o |
. . . . . . . 8
⊢ ⊥ =
(oc‘𝐾) |
13 | 11, 12 | eqtr4di 2798 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (oc‘𝑘) = ⊥ ) |
14 | | fveq2 6769 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (glb‘𝑘) = (glb‘𝐾)) |
15 | | dochval.g |
. . . . . . . . 9
⊢ 𝐺 = (glb‘𝐾) |
16 | 14, 15 | eqtr4di 2798 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (glb‘𝑘) = 𝐺) |
17 | | fveq2 6769 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾)) |
18 | | dochval.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐾) |
19 | 17, 18 | eqtr4di 2798 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵) |
20 | 10 | fveq1d 6771 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (((DIsoH‘𝑘)‘𝑤)‘𝑦) = (((DIsoH‘𝐾)‘𝑤)‘𝑦)) |
21 | 20 | sseq2d 3958 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦) ↔ 𝑥 ⊆ (((DIsoH‘𝐾)‘𝑤)‘𝑦))) |
22 | 19, 21 | rabeqbidv 3419 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → {𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)} = {𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ (((DIsoH‘𝐾)‘𝑤)‘𝑦)}) |
23 | 16, 22 | fveq12d 6776 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}) = (𝐺‘{𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ (((DIsoH‘𝐾)‘𝑤)‘𝑦)})) |
24 | 13, 23 | fveq12d 6776 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})) = ( ⊥ ‘(𝐺‘{𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ (((DIsoH‘𝐾)‘𝑤)‘𝑦)}))) |
25 | 10, 24 | fveq12d 6776 |
. . . . 5
⊢ (𝑘 = 𝐾 → (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))) = (((DIsoH‘𝐾)‘𝑤)‘( ⊥ ‘(𝐺‘{𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ (((DIsoH‘𝐾)‘𝑤)‘𝑦)})))) |
26 | 8, 25 | mpteq12dv 5170 |
. . . 4
⊢ (𝑘 = 𝐾 → (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))) = (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((DIsoH‘𝐾)‘𝑤)‘( ⊥ ‘(𝐺‘{𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ (((DIsoH‘𝐾)‘𝑤)‘𝑦)}))))) |
27 | 4, 26 | mpteq12dv 5170 |
. . 3
⊢ (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((DIsoH‘𝐾)‘𝑤)‘( ⊥ ‘(𝐺‘{𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ (((DIsoH‘𝐾)‘𝑤)‘𝑦)})))))) |
28 | | df-doch 39356 |
. . 3
⊢ ocH =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))))) |
29 | 27, 28, 3 | mptfvmpt 7099 |
. 2
⊢ (𝐾 ∈ V →
(ocH‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((DIsoH‘𝐾)‘𝑤)‘( ⊥ ‘(𝐺‘{𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ (((DIsoH‘𝐾)‘𝑤)‘𝑦)})))))) |
30 | 1, 29 | syl 17 |
1
⊢ (𝐾 ∈ 𝑉 → (ocH‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((DIsoH‘𝐾)‘𝑤)‘( ⊥ ‘(𝐺‘{𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ (((DIsoH‘𝐾)‘𝑤)‘𝑦)})))))) |