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

Theorem hdmapfval 41526
Description: Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
Hypotheses
Ref Expression
hdmapval.h 𝐻 = (LHyp‘𝐾)
hdmapfval.e 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩
hdmapfval.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
hdmapfval.v 𝑉 = (Base‘𝑈)
hdmapfval.n 𝑁 = (LSpan‘𝑈)
hdmapfval.c 𝐶 = ((LCDual‘𝐾)‘𝑊)
hdmapfval.d 𝐷 = (Base‘𝐶)
hdmapfval.j 𝐽 = ((HVMap‘𝐾)‘𝑊)
hdmapfval.i 𝐼 = ((HDMap1‘𝐾)‘𝑊)
hdmapfval.s 𝑆 = ((HDMap‘𝐾)‘𝑊)
hdmapfval.k (𝜑 → (𝐾𝐴𝑊𝐻))
Assertion
Ref Expression
hdmapfval (𝜑𝑆 = (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)))))
Distinct variable groups:   𝑦,𝑡,𝑧,𝐾   𝑦,𝐷   𝑡,𝐸,𝑦,𝑧   𝑡,𝐼,𝑦,𝑧   𝑡,𝑈,𝑦,𝑧   𝑡,𝑉,𝑦,𝑧   𝑡,𝑊,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑦,𝑧,𝑡)   𝐴(𝑦,𝑧,𝑡)   𝐶(𝑦,𝑧,𝑡)   𝐷(𝑧,𝑡)   𝑆(𝑦,𝑧,𝑡)   𝐻(𝑦,𝑧,𝑡)   𝐽(𝑦,𝑧,𝑡)   𝑁(𝑦,𝑧,𝑡)

Proof of Theorem hdmapfval
Dummy variables 𝑤 𝑒 𝑎 𝑖 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hdmapfval.k . 2 (𝜑 → (𝐾𝐴𝑊𝐻))
2 hdmapfval.s . . . 4 𝑆 = ((HDMap‘𝐾)‘𝑊)
3 hdmapval.h . . . . . 6 𝐻 = (LHyp‘𝐾)
43hdmapffval 41525 . . . . 5 (𝐾𝐴 → (HDMap‘𝐾) = (𝑤𝐻 ↦ {𝑎[⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}))
54fveq1d 6903 . . . 4 (𝐾𝐴 → ((HDMap‘𝐾)‘𝑊) = ((𝑤𝐻 ↦ {𝑎[⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})‘𝑊))
62, 5eqtrid 2778 . . 3 (𝐾𝐴𝑆 = ((𝑤𝐻 ↦ {𝑎[⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})‘𝑊))
7 fveq2 6901 . . . . . . . . 9 (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊))
87reseq2d 5989 . . . . . . . 8 (𝑤 = 𝑊 → ( I ↾ ((LTrn‘𝐾)‘𝑤)) = ( I ↾ ((LTrn‘𝐾)‘𝑊)))
98opeq2d 4886 . . . . . . 7 (𝑤 = 𝑊 → ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩)
10 fveq2 6901 . . . . . . . 8 (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = ((DVecH‘𝐾)‘𝑊))
11 fveq2 6901 . . . . . . . . . 10 (𝑤 = 𝑊 → ((HDMap1‘𝐾)‘𝑤) = ((HDMap1‘𝐾)‘𝑊))
12 2fveq3 6906 . . . . . . . . . . . . 13 (𝑤 = 𝑊 → (Base‘((LCDual‘𝐾)‘𝑤)) = (Base‘((LCDual‘𝐾)‘𝑊)))
13 fveq2 6901 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑊 → ((HVMap‘𝐾)‘𝑤) = ((HVMap‘𝐾)‘𝑊))
1413fveq1d 6903 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑊 → (((HVMap‘𝐾)‘𝑤)‘𝑒) = (((HVMap‘𝐾)‘𝑊)‘𝑒))
1514oteq2d 4892 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑊 → ⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩ = ⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩)
1615fveq2d 6905 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑊 → (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩) = (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩))
1716oteq2d 4892 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑊 → ⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩ = ⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)
1817fveq2d 6905 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑊 → (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
1918eqeq2d 2737 . . . . . . . . . . . . . . 15 (𝑤 = 𝑊 → (𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩) ↔ 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))
2019imbi2d 339 . . . . . . . . . . . . . 14 (𝑤 = 𝑊 → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
2120ralbidv 3168 . . . . . . . . . . . . 13 (𝑤 = 𝑊 → (∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ ∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
2212, 21riotaeqbidv 7383 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))) = (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
2322mpteq2dv 5255 . . . . . . . . . . 11 (𝑤 = 𝑊 → (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) = (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))))
2423eleq2d 2812 . . . . . . . . . 10 (𝑤 = 𝑊 → (𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
2511, 24sbceqbid 3783 . . . . . . . . 9 (𝑤 = 𝑊 → ([((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
2625sbcbidv 3836 . . . . . . . 8 (𝑤 = 𝑊 → ([(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
2710, 26sbceqbid 3783 . . . . . . 7 (𝑤 = 𝑊 → ([((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
289, 27sbceqbid 3783 . . . . . 6 (𝑤 = 𝑊 → ([⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ / 𝑒][((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
29 opex 5470 . . . . . . 7 ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∈ V
30 fvex 6914 . . . . . . 7 ((DVecH‘𝐾)‘𝑊) ∈ V
31 fvex 6914 . . . . . . 7 (Base‘𝑢) ∈ V
32 simp1 1133 . . . . . . . . 9 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩)
33 hdmapfval.e . . . . . . . . 9 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩
3432, 33eqtr4di 2784 . . . . . . . 8 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑒 = 𝐸)
35 simp2 1134 . . . . . . . . 9 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑢 = ((DVecH‘𝐾)‘𝑊))
36 hdmapfval.u . . . . . . . . 9 𝑈 = ((DVecH‘𝐾)‘𝑊)
3735, 36eqtr4di 2784 . . . . . . . 8 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑢 = 𝑈)
38 simp3 1135 . . . . . . . . . 10 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = (Base‘𝑢))
3937fveq2d 6905 . . . . . . . . . 10 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → (Base‘𝑢) = (Base‘𝑈))
4038, 39eqtrd 2766 . . . . . . . . 9 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = (Base‘𝑈))
41 hdmapfval.v . . . . . . . . 9 𝑉 = (Base‘𝑈)
4240, 41eqtr4di 2784 . . . . . . . 8 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = 𝑉)
43 fvex 6914 . . . . . . . . . 10 ((HDMap1‘𝐾)‘𝑊) ∈ V
44 id 22 . . . . . . . . . . . 12 (𝑖 = ((HDMap1‘𝐾)‘𝑊) → 𝑖 = ((HDMap1‘𝐾)‘𝑊))
45 hdmapfval.i . . . . . . . . . . . 12 𝐼 = ((HDMap1‘𝐾)‘𝑊)
4644, 45eqtr4di 2784 . . . . . . . . . . 11 (𝑖 = ((HDMap1‘𝐾)‘𝑊) → 𝑖 = 𝐼)
47 fveq1 6900 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝐼 → (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
48 fveq1 6900 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝐼 → (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩) = (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩))
4948oteq2d 4892 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝐼 → ⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩ = ⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)
5049fveq2d 6905 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝐼 → (𝐼‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
5147, 50eqtrd 2766 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝐼 → (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
5251eqeq2d 2737 . . . . . . . . . . . . . . . 16 (𝑖 = 𝐼 → (𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) ↔ 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))
5352imbi2d 339 . . . . . . . . . . . . . . 15 (𝑖 = 𝐼 → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
5453ralbidv 3168 . . . . . . . . . . . . . 14 (𝑖 = 𝐼 → (∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ ∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
5554riotabidv 7382 . . . . . . . . . . . . 13 (𝑖 = 𝐼 → (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))) = (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
5655mpteq2dv 5255 . . . . . . . . . . . 12 (𝑖 = 𝐼 → (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) = (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))))
5756eleq2d 2812 . . . . . . . . . . 11 (𝑖 = 𝐼 → (𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
5846, 57syl 17 . . . . . . . . . 10 (𝑖 = ((HDMap1‘𝐾)‘𝑊) → (𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
5943, 58sbcie 3820 . . . . . . . . 9 ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))))
60 simp3 1135 . . . . . . . . . . 11 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → 𝑣 = 𝑉)
61 hdmapfval.d . . . . . . . . . . . . . 14 𝐷 = (Base‘𝐶)
62 hdmapfval.c . . . . . . . . . . . . . . 15 𝐶 = ((LCDual‘𝐾)‘𝑊)
6362fveq2i 6904 . . . . . . . . . . . . . 14 (Base‘𝐶) = (Base‘((LCDual‘𝐾)‘𝑊))
6461, 63eqtr2i 2755 . . . . . . . . . . . . 13 (Base‘((LCDual‘𝐾)‘𝑊)) = 𝐷
6564a1i 11 . . . . . . . . . . . 12 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (Base‘((LCDual‘𝐾)‘𝑊)) = 𝐷)
66 simp2 1134 . . . . . . . . . . . . . . . . . . . 20 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → 𝑢 = 𝑈)
6766fveq2d 6905 . . . . . . . . . . . . . . . . . . 19 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (LSpan‘𝑢) = (LSpan‘𝑈))
68 hdmapfval.n . . . . . . . . . . . . . . . . . . 19 𝑁 = (LSpan‘𝑈)
6967, 68eqtr4di 2784 . . . . . . . . . . . . . . . . . 18 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (LSpan‘𝑢) = 𝑁)
70 simp1 1133 . . . . . . . . . . . . . . . . . . 19 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → 𝑒 = 𝐸)
7170sneqd 4645 . . . . . . . . . . . . . . . . . 18 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → {𝑒} = {𝐸})
7269, 71fveq12d 6908 . . . . . . . . . . . . . . . . 17 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ((LSpan‘𝑢)‘{𝑒}) = (𝑁‘{𝐸}))
7369fveq1d 6903 . . . . . . . . . . . . . . . . 17 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ((LSpan‘𝑢)‘{𝑡}) = (𝑁‘{𝑡}))
7472, 73uneq12d 4164 . . . . . . . . . . . . . . . 16 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) = ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})))
7574eleq2d 2812 . . . . . . . . . . . . . . 15 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) ↔ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡}))))
7675notbid 317 . . . . . . . . . . . . . 14 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) ↔ ¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡}))))
7770oteq1d 4891 . . . . . . . . . . . . . . . . . . 19 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩ = ⟨𝐸, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩)
7870fveq2d 6905 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (((HVMap‘𝐾)‘𝑊)‘𝑒) = (((HVMap‘𝐾)‘𝑊)‘𝐸))
79 hdmapfval.j . . . . . . . . . . . . . . . . . . . . . 22 𝐽 = ((HVMap‘𝐾)‘𝑊)
8079fveq1i 6902 . . . . . . . . . . . . . . . . . . . . 21 (𝐽𝐸) = (((HVMap‘𝐾)‘𝑊)‘𝐸)
8178, 80eqtr4di 2784 . . . . . . . . . . . . . . . . . . . 20 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (((HVMap‘𝐾)‘𝑊)‘𝑒) = (𝐽𝐸))
8281oteq2d 4892 . . . . . . . . . . . . . . . . . . 19 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ⟨𝐸, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩ = ⟨𝐸, (𝐽𝐸), 𝑧⟩)
8377, 82eqtrd 2766 . . . . . . . . . . . . . . . . . 18 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩ = ⟨𝐸, (𝐽𝐸), 𝑧⟩)
8483fveq2d 6905 . . . . . . . . . . . . . . . . 17 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩) = (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩))
8584oteq2d 4892 . . . . . . . . . . . . . . . 16 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩ = ⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)
8685fveq2d 6905 . . . . . . . . . . . . . . 15 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))
8786eqeq2d 2737 . . . . . . . . . . . . . 14 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) ↔ 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)))
8876, 87imbi12d 343 . . . . . . . . . . . . 13 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))))
8960, 88raleqbidv 3330 . . . . . . . . . . . 12 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ ∀𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))))
9065, 89riotaeqbidv 7383 . . . . . . . . . . 11 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))) = (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))))
9160, 90mpteq12dv 5244 . . . . . . . . . 10 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) = (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)))))
9291eleq2d 2812 . . . . . . . . 9 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))))))
9359, 92bitrid 282 . . . . . . . 8 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))))))
9434, 37, 42, 93syl3anc 1368 . . . . . . 7 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))))))
9529, 30, 31, 94sbc3ie 3862 . . . . . 6 ([⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ / 𝑒][((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)))))
9628, 95bitrdi 286 . . . . 5 (𝑤 = 𝑊 → ([⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))))))
9796eqabcdv 2861 . . . 4 (𝑤 = 𝑊 → {𝑎[⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))} = (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)))))
98 eqid 2726 . . . 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‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})
9997, 98, 41mptfvmpt 7245 . . 3 (𝑊𝐻 → ((𝑤𝐻 ↦ {𝑎[⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})‘𝑊) = (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)))))
1006, 99sylan9eq 2786 . 2 ((𝐾𝐴𝑊𝐻) → 𝑆 = (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)))))
1011, 100syl 17 1 (𝜑𝑆 = (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  {cab 2703  wral 3051  [wsbc 3776  cun 3945  {csn 4633  cop 4639  cotp 4641  cmpt 5236   I cid 5579  cres 5684  cfv 6554  crio 7379  Basecbs 17213  LSpanclspn 20948  LHypclh 39683  LTrncltrn 39800  DVecHcdvh 40777  LCDualclcd 41285  HVMapchvm 41455  HDMap1chdma1 41490  HDMapchdma 41491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pr 5433
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-ot 4642  df-uni 4914  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-riota 7380  df-hdmap 41493
This theorem is referenced by:  hdmapval  41527  hdmapfnN  41528
  Copyright terms: Public domain W3C validator