# Metamath Proof Explorer

## Theorem hdmapfval

Description: Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015)

Ref Expression
Hypotheses hdmapval.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmapfval.e ${⊢}{E}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩$
hdmapfval.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmapfval.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmapfval.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
hdmapfval.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
hdmapfval.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
hdmapfval.j ${⊢}{J}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
hdmapfval.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
hdmapfval.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
hdmapfval.k ${⊢}{\phi }\to \left({K}\in {A}\wedge {W}\in {H}\right)$
Assertion hdmapfval ${⊢}{\phi }\to {S}=\left({t}\in {V}⟼\left(\iota {y}\in {D}|\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 hdmapval.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmapfval.e ${⊢}{E}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩$
3 hdmapfval.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 hdmapfval.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 hdmapfval.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
6 hdmapfval.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
7 hdmapfval.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
8 hdmapfval.j ${⊢}{J}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
9 hdmapfval.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
10 hdmapfval.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
11 hdmapfval.k ${⊢}{\phi }\to \left({K}\in {A}\wedge {W}\in {H}\right)$
12 1 hdmapffval
13 12 fveq1d
14 10 13 syl5eq
15 fveq2 ${⊢}{w}={W}\to \mathrm{LTrn}\left({K}\right)\left({w}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
16 15 reseq2d ${⊢}{w}={W}\to {\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({w}\right)}={\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}$
17 16 opeq2d ${⊢}{w}={W}\to ⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({w}\right)}⟩=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩$
18 fveq2 ${⊢}{w}={W}\to \mathrm{DVecH}\left({K}\right)\left({w}\right)=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
19 fveq2 ${⊢}{w}={W}\to \mathrm{HDMap1}\left({K}\right)\left({w}\right)=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
20 2fveq3 ${⊢}{w}={W}\to {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({w}\right)}={\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
21 fveq2 ${⊢}{w}={W}\to \mathrm{HVMap}\left({K}\right)\left({w}\right)=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
22 21 fveq1d ${⊢}{w}={W}\to \mathrm{HVMap}\left({K}\right)\left({w}\right)\left({e}\right)=\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right)$
23 22 oteq2d ${⊢}{w}={W}\to ⟨{e},\mathrm{HVMap}\left({K}\right)\left({w}\right)\left({e}\right),{z}⟩=⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩$
24 23 fveq2d ${⊢}{w}={W}\to {i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({w}\right)\left({e}\right),{z}⟩\right)={i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right)$
25 24 oteq2d ${⊢}{w}={W}\to ⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({w}\right)\left({e}\right),{z}⟩\right),{t}⟩=⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩$
26 25 fveq2d ${⊢}{w}={W}\to {i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({w}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)$
27 26 eqeq2d ${⊢}{w}={W}\to \left({y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({w}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)↔{y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)$
28 27 imbi2d ${⊢}{w}={W}\to \left(\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({w}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)↔\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)$
29 28 ralbidv ${⊢}{w}={W}\to \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({w}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)↔\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)$
30 20 29 riotaeqbidv ${⊢}{w}={W}\to \left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({w}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({w}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)=\left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)$
31 30 mpteq2dv ${⊢}{w}={W}\to \left({t}\in {v}⟼\left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({w}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({w}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)=\left({t}\in {v}⟼\left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)$
32 31 eleq2d ${⊢}{w}={W}\to \left({a}\in \left({t}\in {v}⟼\left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({w}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({w}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)↔{a}\in \left({t}\in {v}⟼\left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)\right)$
33 19 32 sbceqbid
34 33 sbcbidv
35 18 34 sbceqbid
36 17 35 sbceqbid
37 opex ${⊢}⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\in \mathrm{V}$
38 fvex ${⊢}\mathrm{DVecH}\left({K}\right)\left({W}\right)\in \mathrm{V}$
39 fvex ${⊢}{\mathrm{Base}}_{{u}}\in \mathrm{V}$
40 simp1 ${⊢}\left({e}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\wedge {u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\right)\to {e}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩$
41 40 2 syl6eqr ${⊢}\left({e}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\wedge {u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\right)\to {e}={E}$
42 simp2 ${⊢}\left({e}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\wedge {u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\right)\to {u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
43 42 3 syl6eqr ${⊢}\left({e}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\wedge {u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\right)\to {u}={U}$
44 simp3 ${⊢}\left({e}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\wedge {u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\right)\to {v}={\mathrm{Base}}_{{u}}$
45 43 fveq2d ${⊢}\left({e}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\wedge {u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\right)\to {\mathrm{Base}}_{{u}}={\mathrm{Base}}_{{U}}$
46 44 45 eqtrd ${⊢}\left({e}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\wedge {u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\right)\to {v}={\mathrm{Base}}_{{U}}$
47 46 4 syl6eqr ${⊢}\left({e}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\wedge {u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\right)\to {v}={V}$
48 fvex ${⊢}\mathrm{HDMap1}\left({K}\right)\left({W}\right)\in \mathrm{V}$
49 id ${⊢}{i}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)\to {i}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
50 49 9 syl6eqr ${⊢}{i}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)\to {i}={I}$
51 fveq1 ${⊢}{i}={I}\to {i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)={I}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)$
52 fveq1 ${⊢}{i}={I}\to {i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right)={I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right)$
53 52 oteq2d ${⊢}{i}={I}\to ⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩=⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩$
54 53 fveq2d ${⊢}{i}={I}\to {I}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)={I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)$
55 51 54 eqtrd ${⊢}{i}={I}\to {i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)={I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)$
56 55 eqeq2d ${⊢}{i}={I}\to \left({y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)↔{y}={I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)$
57 56 imbi2d ${⊢}{i}={I}\to \left(\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)↔\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)$
58 57 ralbidv ${⊢}{i}={I}\to \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)↔\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)$
59 58 riotabidv ${⊢}{i}={I}\to \left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)=\left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)$
60 59 mpteq2dv ${⊢}{i}={I}\to \left({t}\in {v}⟼\left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)=\left({t}\in {v}⟼\left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)$
61 60 eleq2d ${⊢}{i}={I}\to \left({a}\in \left({t}\in {v}⟼\left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)↔{a}\in \left({t}\in {v}⟼\left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)\right)$
62 50 61 syl ${⊢}{i}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)\to \left({a}\in \left({t}\in {v}⟼\left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={i}\left(⟨{z},{i}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)↔{a}\in \left({t}\in {v}⟼\left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)\right)$
63 48 62 sbcie
64 simp3 ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to {v}={V}$
65 6 fveq2i ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
66 7 65 eqtr2i ${⊢}{\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}={D}$
67 66 a1i ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}={D}$
68 simp2 ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to {u}={U}$
69 68 fveq2d ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \mathrm{LSpan}\left({u}\right)=\mathrm{LSpan}\left({U}\right)$
70 69 5 syl6eqr ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \mathrm{LSpan}\left({u}\right)={N}$
71 simp1 ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to {e}={E}$
72 71 sneqd ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \left\{{e}\right\}=\left\{{E}\right\}$
73 70 72 fveq12d ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)={N}\left(\left\{{E}\right\}\right)$
74 70 fveq1d ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)={N}\left(\left\{{t}\right\}\right)$
75 73 74 uneq12d ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)={N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{t}\right\}\right)$
76 75 eleq2d ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \left({z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)↔{z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{t}\right\}\right)\right)\right)$
77 76 notbid ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)↔¬{z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{t}\right\}\right)\right)\right)$
78 71 oteq1d ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to ⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩=⟨{E},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩$
79 71 fveq2d ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right)=\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({E}\right)$
80 8 fveq1i ${⊢}{J}\left({E}\right)=\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({E}\right)$
81 79 80 syl6eqr ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right)={J}\left({E}\right)$
82 81 oteq2d ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to ⟨{E},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩=⟨{E},{J}\left({E}\right),{z}⟩$
83 78 82 eqtrd ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to ⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩=⟨{E},{J}\left({E}\right),{z}⟩$
84 83 fveq2d ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to {I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right)={I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right)$
85 84 oteq2d ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to ⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩=⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{t}⟩$
86 85 fveq2d ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to {I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)={I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{t}⟩\right)$
87 86 eqeq2d ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \left({y}={I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)↔{y}={I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{t}⟩\right)\right)$
88 77 87 imbi12d ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \left(\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)↔\left(¬{z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{t}⟩\right)\right)\right)$
89 64 88 raleqbidv ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \left(\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)↔\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{t}⟩\right)\right)\right)$
90 67 89 riotaeqbidv ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)=\left(\iota {y}\in {D}|\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{t}⟩\right)\right)\right)$
91 64 90 mpteq12dv ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \left({t}\in {v}⟼\left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)=\left({t}\in {V}⟼\left(\iota {y}\in {D}|\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)$
92 91 eleq2d ${⊢}\left({e}={E}\wedge {u}={U}\wedge {v}={V}\right)\to \left({a}\in \left({t}\in {v}⟼\left(\iota {y}\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}|\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left(\mathrm{LSpan}\left({u}\right)\left(\left\{{e}\right\}\right)\cup \mathrm{LSpan}\left({u}\right)\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{e},\mathrm{HVMap}\left({K}\right)\left({W}\right)\left({e}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)↔{a}\in \left({t}\in {V}⟼\left(\iota {y}\in {D}|\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)\right)$
93 63 92 syl5bb
94 41 43 47 93 syl3anc
95 37 38 39 94 sbc3ie
96 36 95 syl6bb
97 96 abbi1dv
98 eqid
99 97 98 4 mptfvmpt
100 14 99 sylan9eq ${⊢}\left({K}\in {A}\wedge {W}\in {H}\right)\to {S}=\left({t}\in {V}⟼\left(\iota {y}\in {D}|\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)$
101 11 100 syl ${⊢}{\phi }\to {S}=\left({t}\in {V}⟼\left(\iota {y}\in {D}|\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{t}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)$