Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hdmapffval Structured version   Visualization version   GIF version

Theorem hdmapffval 35934
Description: Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
Hypothesis
Ref Expression
hdmapval.h 𝐻 = (LHyp‘𝐾)
Assertion
Ref Expression
hdmapffval (𝐾𝑋 → (HDMap‘𝐾) = (𝑤𝐻 ↦ {𝑎[⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}))
Distinct variable groups:   𝑤,𝐻   𝑒,𝑎,𝑖,𝑡,𝑢,𝑣,𝑤,𝑦,𝑧,𝐾
Allowed substitution hints:   𝐻(𝑦,𝑧,𝑣,𝑢,𝑡,𝑒,𝑖,𝑎)   𝑋(𝑦,𝑧,𝑤,𝑣,𝑢,𝑡,𝑒,𝑖,𝑎)

Proof of Theorem hdmapffval
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 elex 3179 . 2 (𝐾𝑋𝐾 ∈ V)
2 fveq2 6083 . . . . 5 (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾))
3 hdmapval.h . . . . 5 𝐻 = (LHyp‘𝐾)
42, 3syl6eqr 2656 . . . 4 (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻)
5 fveq2 6083 . . . . . . . 8 (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾))
65reseq2d 5299 . . . . . . 7 (𝑘 = 𝐾 → ( I ↾ (Base‘𝑘)) = ( I ↾ (Base‘𝐾)))
7 fveq2 6083 . . . . . . . . 9 (𝑘 = 𝐾 → (LTrn‘𝑘) = (LTrn‘𝐾))
87fveq1d 6085 . . . . . . . 8 (𝑘 = 𝐾 → ((LTrn‘𝑘)‘𝑤) = ((LTrn‘𝐾)‘𝑤))
98reseq2d 5299 . . . . . . 7 (𝑘 = 𝐾 → ( I ↾ ((LTrn‘𝑘)‘𝑤)) = ( I ↾ ((LTrn‘𝐾)‘𝑤)))
106, 9opeq12d 4337 . . . . . 6 (𝑘 = 𝐾 → ⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩ = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩)
11 fveq2 6083 . . . . . . . 8 (𝑘 = 𝐾 → (DVecH‘𝑘) = (DVecH‘𝐾))
1211fveq1d 6085 . . . . . . 7 (𝑘 = 𝐾 → ((DVecH‘𝑘)‘𝑤) = ((DVecH‘𝐾)‘𝑤))
13 fveq2 6083 . . . . . . . . . 10 (𝑘 = 𝐾 → (HDMap1‘𝑘) = (HDMap1‘𝐾))
1413fveq1d 6085 . . . . . . . . 9 (𝑘 = 𝐾 → ((HDMap1‘𝑘)‘𝑤) = ((HDMap1‘𝐾)‘𝑤))
15 fveq2 6083 . . . . . . . . . . . . . 14 (𝑘 = 𝐾 → (LCDual‘𝑘) = (LCDual‘𝐾))
1615fveq1d 6085 . . . . . . . . . . . . 13 (𝑘 = 𝐾 → ((LCDual‘𝑘)‘𝑤) = ((LCDual‘𝐾)‘𝑤))
1716fveq2d 6087 . . . . . . . . . . . 12 (𝑘 = 𝐾 → (Base‘((LCDual‘𝑘)‘𝑤)) = (Base‘((LCDual‘𝐾)‘𝑤)))
18 fveq2 6083 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝐾 → (HVMap‘𝑘) = (HVMap‘𝐾))
1918fveq1d 6085 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝐾 → ((HVMap‘𝑘)‘𝑤) = ((HVMap‘𝐾)‘𝑤))
2019fveq1d 6085 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝐾 → (((HVMap‘𝑘)‘𝑤)‘𝑒) = (((HVMap‘𝐾)‘𝑤)‘𝑒))
2120oteq2d 4342 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝐾 → ⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩ = ⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩)
2221fveq2d 6087 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝐾 → (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩) = (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩))
2322oteq2d 4342 . . . . . . . . . . . . . . . 16 (𝑘 = 𝐾 → ⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩ = ⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)
2423fveq2d 6087 . . . . . . . . . . . . . . 15 (𝑘 = 𝐾 → (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))
2524eqeq2d 2614 . . . . . . . . . . . . . 14 (𝑘 = 𝐾 → (𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩) ↔ 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))
2625imbi2d 328 . . . . . . . . . . . . 13 (𝑘 = 𝐾 → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))
2726ralbidv 2963 . . . . . . . . . . . 12 (𝑘 = 𝐾 → (∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ ∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))
2817, 27riotaeqbidv 6487 . . . . . . . . . . 11 (𝑘 = 𝐾 → (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))) = (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))
2928mpteq2dv 4662 . . . . . . . . . 10 (𝑘 = 𝐾 → (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) = (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))))
3029eleq2d 2667 . . . . . . . . 9 (𝑘 = 𝐾 → (𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))))
3114, 30sbceqbid 3403 . . . . . . . 8 (𝑘 = 𝐾 → ([((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))))
3231sbcbidv 3451 . . . . . . 7 (𝑘 = 𝐾 → ([(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))))
3312, 32sbceqbid 3403 . . . . . 6 (𝑘 = 𝐾 → ([((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))))
3410, 33sbceqbid 3403 . . . . 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‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))))
3534abbidv 2722 . . . 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‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})
364, 35mpteq12dv 4652 . . 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 35900 . . 3 HDMap = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎[⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩ / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}))
38 fvex 6093 . . . . 5 (LHyp‘𝐾) ∈ V
393, 38eqeltri 2678 . . . 4 𝐻 ∈ V
4039mptex 6363 . . 3 (𝑤𝐻 ↦ {𝑎[⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}) ∈ V
4136, 37, 40fvmpt 6171 . 2 (𝐾 ∈ V → (HDMap‘𝐾) = (𝑤𝐻 ↦ {𝑎[⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}))
421, 41syl 17 1 (𝐾𝑋 → (HDMap‘𝐾) = (𝑤𝐻 ↦ {𝑎[⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wcel 1975  {cab 2590  wral 2890  Vcvv 3167  [wsbc 3396  cun 3532  {csn 4119  cop 4125  cotp 4127  cmpt 4632   I cid 4933  cres 5025  cfv 5785  crio 6483  Basecbs 15636  LSpanclspn 18733  LHypclh 34086  LTrncltrn 34203  DVecHcdvh 35183  LCDualclcd 35691  HVMapchvm 35861  HDMap1chdma1 35897  HDMapchdma 35898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-rep 4688  ax-sep 4698  ax-nul 4707  ax-pr 4823
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2456  df-mo 2457  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ne 2776  df-ral 2895  df-rex 2896  df-reu 2897  df-rab 2899  df-v 3169  df-sbc 3397  df-csb 3494  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-nul 3869  df-if 4031  df-sn 4120  df-pr 4122  df-op 4126  df-ot 4128  df-uni 4362  df-iun 4446  df-br 4573  df-opab 4633  df-mpt 4634  df-id 4938  df-xp 5029  df-rel 5030  df-cnv 5031  df-co 5032  df-dm 5033  df-rn 5034  df-res 5035  df-ima 5036  df-iota 5749  df-fun 5787  df-fn 5788  df-f 5789  df-f1 5790  df-fo 5791  df-f1o 5792  df-fv 5793  df-riota 6484  df-hdmap 35900
This theorem is referenced by:  hdmapfval  35935
  Copyright terms: Public domain W3C validator