| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. 2
⊢ (𝐾 ∈ 𝑋 → 𝐾 ∈ V) |
| 2 | | fveq2 6906 |
. . . . 5
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾)) |
| 3 | | hdmapval.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
| 4 | 2, 3 | eqtr4di 2795 |
. . . 4
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻) |
| 5 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾)) |
| 6 | 5 | reseq2d 5997 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ( I ↾ (Base‘𝑘)) = ( I ↾
(Base‘𝐾))) |
| 7 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (LTrn‘𝑘) = (LTrn‘𝐾)) |
| 8 | 7 | fveq1d 6908 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ((LTrn‘𝑘)‘𝑤) = ((LTrn‘𝐾)‘𝑤)) |
| 9 | 8 | reseq2d 5997 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ( I ↾ ((LTrn‘𝑘)‘𝑤)) = ( I ↾ ((LTrn‘𝐾)‘𝑤))) |
| 10 | 6, 9 | opeq12d 4881 |
. . . . . 6
⊢ (𝑘 = 𝐾 → 〈( I ↾ (Base‘𝑘)), ( I ↾
((LTrn‘𝑘)‘𝑤))〉 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉) |
| 11 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (DVecH‘𝑘) = (DVecH‘𝐾)) |
| 12 | 11 | fveq1d 6908 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ((DVecH‘𝑘)‘𝑤) = ((DVecH‘𝐾)‘𝑤)) |
| 13 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (HDMap1‘𝑘) = (HDMap1‘𝐾)) |
| 14 | 13 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → ((HDMap1‘𝑘)‘𝑤) = ((HDMap1‘𝐾)‘𝑤)) |
| 15 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝐾 → (LCDual‘𝑘) = (LCDual‘𝐾)) |
| 16 | 15 | fveq1d 6908 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐾 → ((LCDual‘𝑘)‘𝑤) = ((LCDual‘𝐾)‘𝑤)) |
| 17 | 16 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (Base‘((LCDual‘𝑘)‘𝑤)) = (Base‘((LCDual‘𝐾)‘𝑤))) |
| 18 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝐾 → (HVMap‘𝑘) = (HVMap‘𝐾)) |
| 19 | 18 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝐾 → ((HVMap‘𝑘)‘𝑤) = ((HVMap‘𝐾)‘𝑤)) |
| 20 | 19 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝐾 → (((HVMap‘𝑘)‘𝑤)‘𝑒) = (((HVMap‘𝐾)‘𝑤)‘𝑒)) |
| 21 | 20 | oteq2d 4886 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝐾 → 〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉 = 〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉) |
| 22 | 21 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝐾 → (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉) = (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉)) |
| 23 | 22 | oteq2d 4886 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝐾 → 〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉 = 〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉) |
| 24 | 23 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝐾 → (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉) = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)) |
| 25 | 24 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝐾 → (𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉) ↔ 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))) |
| 26 | 25 | imbi2d 340 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐾 → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)) ↔ (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) |
| 27 | 26 | ralbidv 3178 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)) ↔ ∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) |
| 28 | 17, 27 | riotaeqbidv 7391 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))) = (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) |
| 29 | 28 | mpteq2dv 5244 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) = (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))) |
| 30 | 29 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))))) |
| 31 | 14, 30 | sbceqbid 3795 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ([((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔
[((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))))) |
| 32 | 31 | sbcbidv 3845 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ([(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ [(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))))) |
| 33 | 12, 32 | sbceqbid 3795 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ([((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ [((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))))) |
| 34 | 10, 33 | sbceqbid 3795 |
. . . . 5
⊢ (𝑘 = 𝐾 → ([〈( I ↾
(Base‘𝑘)), ( I
↾ ((LTrn‘𝑘)‘𝑤))〉 / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))))) |
| 35 | 34 | abbidv 2808 |
. . . 4
⊢ (𝑘 = 𝐾 → {𝑎 ∣ [〈( I ↾
(Base‘𝑘)), ( I
↾ ((LTrn‘𝑘)‘𝑤))〉 / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))} = {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))}) |
| 36 | 4, 35 | mpteq12dv 5233 |
. . 3
⊢ (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [〈( I ↾
(Base‘𝑘)), ( I
↾ ((LTrn‘𝑘)‘𝑤))〉 / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))}) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))})) |
| 37 | | df-hdmap 41796 |
. . 3
⊢ HDMap =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [〈( I ↾
(Base‘𝑘)), ( I
↾ ((LTrn‘𝑘)‘𝑤))〉 / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))})) |
| 38 | 36, 37, 3 | mptfvmpt 7248 |
. 2
⊢ (𝐾 ∈ V →
(HDMap‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))})) |
| 39 | 1, 38 | syl 17 |
1
⊢ (𝐾 ∈ 𝑋 → (HDMap‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))})) |