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 37715
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 37714 . . . . 5 (𝐾𝐴 → (HDMap‘𝐾) = (𝑤𝐻 ↦ {𝑎[⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}))
54fveq1d 6377 . . . 4 (𝐾𝐴 → ((HDMap‘𝐾)‘𝑊) = ((𝑤𝐻 ↦ {𝑎[⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})‘𝑊))
62, 5syl5eq 2811 . . 3 (𝐾𝐴𝑆 = ((𝑤𝐻 ↦ {𝑎[⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})‘𝑊))
7 fveq2 6375 . . . . . . . . 9 (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊))
87reseq2d 5565 . . . . . . . 8 (𝑤 = 𝑊 → ( I ↾ ((LTrn‘𝐾)‘𝑤)) = ( I ↾ ((LTrn‘𝐾)‘𝑊)))
98opeq2d 4566 . . . . . . 7 (𝑤 = 𝑊 → ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩)
10 fveq2 6375 . . . . . . . 8 (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = ((DVecH‘𝐾)‘𝑊))
11 fveq2 6375 . . . . . . . . . 10 (𝑤 = 𝑊 → ((HDMap1‘𝐾)‘𝑤) = ((HDMap1‘𝐾)‘𝑊))
12 2fveq3 6380 . . . . . . . . . . . . 13 (𝑤 = 𝑊 → (Base‘((LCDual‘𝐾)‘𝑤)) = (Base‘((LCDual‘𝐾)‘𝑊)))
13 fveq2 6375 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑊 → ((HVMap‘𝐾)‘𝑤) = ((HVMap‘𝐾)‘𝑊))
1413fveq1d 6377 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑊 → (((HVMap‘𝐾)‘𝑤)‘𝑒) = (((HVMap‘𝐾)‘𝑊)‘𝑒))
1514oteq2d 4572 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑊 → ⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩ = ⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩)
1615fveq2d 6379 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑊 → (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩) = (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩))
1716oteq2d 4572 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑊 → ⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩ = ⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)
1817fveq2d 6379 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑊 → (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
1918eqeq2d 2775 . . . . . . . . . . . . . . 15 (𝑤 = 𝑊 → (𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩) ↔ 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))
2019imbi2d 331 . . . . . . . . . . . . . 14 (𝑤 = 𝑊 → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
2120ralbidv 3133 . . . . . . . . . . . . 13 (𝑤 = 𝑊 → (∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ ∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
2212, 21riotaeqbidv 6806 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))) = (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
2322mpteq2dv 4904 . . . . . . . . . . 11 (𝑤 = 𝑊 → (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) = (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))))
2423eleq2d 2830 . . . . . . . . . 10 (𝑤 = 𝑊 → (𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
2511, 24sbceqbid 3603 . . . . . . . . 9 (𝑤 = 𝑊 → ([((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
2625sbcbidv 3651 . . . . . . . 8 (𝑤 = 𝑊 → ([(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
2710, 26sbceqbid 3603 . . . . . . 7 (𝑤 = 𝑊 → ([((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
289, 27sbceqbid 3603 . . . . . 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 5088 . . . . . . 7 ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∈ V
30 fvex 6388 . . . . . . 7 ((DVecH‘𝐾)‘𝑊) ∈ V
31 fvex 6388 . . . . . . 7 (Base‘𝑢) ∈ V
32 simp1 1166 . . . . . . . . 9 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩)
33 hdmapfval.e . . . . . . . . 9 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩
3432, 33syl6eqr 2817 . . . . . . . 8 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑒 = 𝐸)
35 simp2 1167 . . . . . . . . 9 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑢 = ((DVecH‘𝐾)‘𝑊))
36 hdmapfval.u . . . . . . . . 9 𝑈 = ((DVecH‘𝐾)‘𝑊)
3735, 36syl6eqr 2817 . . . . . . . 8 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑢 = 𝑈)
38 simp3 1168 . . . . . . . . . 10 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = (Base‘𝑢))
3937fveq2d 6379 . . . . . . . . . 10 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → (Base‘𝑢) = (Base‘𝑈))
4038, 39eqtrd 2799 . . . . . . . . 9 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = (Base‘𝑈))
41 hdmapfval.v . . . . . . . . 9 𝑉 = (Base‘𝑈)
4240, 41syl6eqr 2817 . . . . . . . 8 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = 𝑉)
43 fvex 6388 . . . . . . . . . 10 ((HDMap1‘𝐾)‘𝑊) ∈ V
44 id 22 . . . . . . . . . . . 12 (𝑖 = ((HDMap1‘𝐾)‘𝑊) → 𝑖 = ((HDMap1‘𝐾)‘𝑊))
45 hdmapfval.i . . . . . . . . . . . 12 𝐼 = ((HDMap1‘𝐾)‘𝑊)
4644, 45syl6eqr 2817 . . . . . . . . . . 11 (𝑖 = ((HDMap1‘𝐾)‘𝑊) → 𝑖 = 𝐼)
47 fveq1 6374 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝐼 → (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
48 fveq1 6374 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝐼 → (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩) = (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩))
4948oteq2d 4572 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝐼 → ⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩ = ⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)
5049fveq2d 6379 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝐼 → (𝐼‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
5147, 50eqtrd 2799 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝐼 → (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
5251eqeq2d 2775 . . . . . . . . . . . . . . . 16 (𝑖 = 𝐼 → (𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) ↔ 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))
5352imbi2d 331 . . . . . . . . . . . . . . 15 (𝑖 = 𝐼 → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
5453ralbidv 3133 . . . . . . . . . . . . . 14 (𝑖 = 𝐼 → (∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ ∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
5554riotabidv 6805 . . . . . . . . . . . . 13 (𝑖 = 𝐼 → (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))) = (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
5655mpteq2dv 4904 . . . . . . . . . . . 12 (𝑖 = 𝐼 → (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) = (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))))
5756eleq2d 2830 . . . . . . . . . . 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 3631 . . . . . . . . 9 ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))))
60 simp3 1168 . . . . . . . . . . 11 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → 𝑣 = 𝑉)
61 hdmapfval.d . . . . . . . . . . . . . 14 𝐷 = (Base‘𝐶)
62 hdmapfval.c . . . . . . . . . . . . . . 15 𝐶 = ((LCDual‘𝐾)‘𝑊)
6362fveq2i 6378 . . . . . . . . . . . . . 14 (Base‘𝐶) = (Base‘((LCDual‘𝐾)‘𝑊))
6461, 63eqtr2i 2788 . . . . . . . . . . . . 13 (Base‘((LCDual‘𝐾)‘𝑊)) = 𝐷
6564a1i 11 . . . . . . . . . . . 12 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (Base‘((LCDual‘𝐾)‘𝑊)) = 𝐷)
66 simp2 1167 . . . . . . . . . . . . . . . . . . . 20 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → 𝑢 = 𝑈)
6766fveq2d 6379 . . . . . . . . . . . . . . . . . . 19 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (LSpan‘𝑢) = (LSpan‘𝑈))
68 hdmapfval.n . . . . . . . . . . . . . . . . . . 19 𝑁 = (LSpan‘𝑈)
6967, 68syl6eqr 2817 . . . . . . . . . . . . . . . . . 18 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (LSpan‘𝑢) = 𝑁)
70 simp1 1166 . . . . . . . . . . . . . . . . . . 19 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → 𝑒 = 𝐸)
7170sneqd 4346 . . . . . . . . . . . . . . . . . 18 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → {𝑒} = {𝐸})
7269, 71fveq12d 6382 . . . . . . . . . . . . . . . . 17 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ((LSpan‘𝑢)‘{𝑒}) = (𝑁‘{𝐸}))
7369fveq1d 6377 . . . . . . . . . . . . . . . . 17 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ((LSpan‘𝑢)‘{𝑡}) = (𝑁‘{𝑡}))
7472, 73uneq12d 3930 . . . . . . . . . . . . . . . 16 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) = ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})))
7574eleq2d 2830 . . . . . . . . . . . . . . 15 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) ↔ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡}))))
7675notbid 309 . . . . . . . . . . . . . 14 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) ↔ ¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡}))))
7770oteq1d 4571 . . . . . . . . . . . . . . . . . . 19 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩ = ⟨𝐸, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩)
7870fveq2d 6379 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (((HVMap‘𝐾)‘𝑊)‘𝑒) = (((HVMap‘𝐾)‘𝑊)‘𝐸))
79 hdmapfval.j . . . . . . . . . . . . . . . . . . . . . 22 𝐽 = ((HVMap‘𝐾)‘𝑊)
8079fveq1i 6376 . . . . . . . . . . . . . . . . . . . . 21 (𝐽𝐸) = (((HVMap‘𝐾)‘𝑊)‘𝐸)
8178, 80syl6eqr 2817 . . . . . . . . . . . . . . . . . . . 20 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (((HVMap‘𝐾)‘𝑊)‘𝑒) = (𝐽𝐸))
8281oteq2d 4572 . . . . . . . . . . . . . . . . . . 19 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ⟨𝐸, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩ = ⟨𝐸, (𝐽𝐸), 𝑧⟩)
8377, 82eqtrd 2799 . . . . . . . . . . . . . . . . . 18 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩ = ⟨𝐸, (𝐽𝐸), 𝑧⟩)
8483fveq2d 6379 . . . . . . . . . . . . . . . . 17 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩) = (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩))
8584oteq2d 4572 . . . . . . . . . . . . . . . 16 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩ = ⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)
8685fveq2d 6379 . . . . . . . . . . . . . . 15 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))
8786eqeq2d 2775 . . . . . . . . . . . . . 14 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) ↔ 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)))
8876, 87imbi12d 335 . . . . . . . . . . . . 13 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))))
8960, 88raleqbidv 3300 . . . . . . . . . . . 12 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ ∀𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))))
9065, 89riotaeqbidv 6806 . . . . . . . . . . 11 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))) = (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))))
9160, 90mpteq12dv 4892 . . . . . . . . . 10 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) = (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)))))
9291eleq2d 2830 . . . . . . . . 9 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → (𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))))))
9359, 92syl5bb 274 . . . . . . . 8 ((𝑒 = 𝐸𝑢 = 𝑈𝑣 = 𝑉) → ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))))))
9434, 37, 42, 93syl3anc 1490 . . . . . . 7 ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))))))
9529, 30, 31, 94sbc3ie 3666 . . . . . 6 ([⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ / 𝑒][((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)))))
9628, 95syl6bb 278 . . . . 5 (𝑤 = 𝑊 → ([⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩))))))
9796abbi1dv 2886 . . . 4 (𝑤 = 𝑊 → {𝑎[⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))} = (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)))))
98 eqid 2765 . . . 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 6683 . . 3 (𝑊𝐻 → ((𝑤𝐻 ↦ {𝑎[⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})‘𝑊) = (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)))))
1006, 99sylan9eq 2819 . 2 ((𝐾𝐴𝑊𝐻) → 𝑆 = (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)))))
1011, 100syl 17 1 (𝜑𝑆 = (𝑡𝑉 ↦ (𝑦𝐷𝑧𝑉𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽𝐸), 𝑧⟩), 𝑡⟩)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  {cab 2751  wral 3055  [wsbc 3596  cun 3730  {csn 4334  cop 4340  cotp 4342  cmpt 4888   I cid 5184  cres 5279  cfv 6068  crio 6802  Basecbs 16132  LSpanclspn 19243  LHypclh 35872  LTrncltrn 35989  DVecHcdvh 36966  LCDualclcd 37474  HVMapchvm 37644  HDMap1chdma1 37679  HDMapchdma 37680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pr 5062
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-ot 4343  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-hdmap 37682
This theorem is referenced by:  hdmapval  37716  hdmapfnN  37717
  Copyright terms: Public domain W3C validator