# Metamath Proof Explorer

## Theorem hdmapfnN

Description: Functionality of map from vectors to functionals with closed kernels. (Contributed by NM, 30-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hdmapfn.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmapfn.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmapfn.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmapfn.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
hdmapfn.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
Assertion hdmapfnN ${⊢}{\phi }\to {S}Fn{V}$

### Proof

Step Hyp Ref Expression
1 hdmapfn.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmapfn.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hdmapfn.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 hdmapfn.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
5 hdmapfn.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
6 riotaex ${⊢}\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\{⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\right\}\right)\cup \mathrm{LSpan}\left({U}\right)\left(\left\{{t}\right\}\right)\right)\to {y}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨{z},\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩,\mathrm{HVMap}\left({K}\right)\left({W}\right)\left(⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\right),{z}⟩\right),{t}⟩\right)\right)\right)\in \mathrm{V}$
7 eqid ${⊢}\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\{⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\right\}\right)\cup \mathrm{LSpan}\left({U}\right)\left(\left\{{t}\right\}\right)\right)\to {y}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨{z},\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩,\mathrm{HVMap}\left({K}\right)\left({W}\right)\left(⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\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\{⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\right\}\right)\cup \mathrm{LSpan}\left({U}\right)\left(\left\{{t}\right\}\right)\right)\to {y}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨{z},\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩,\mathrm{HVMap}\left({K}\right)\left({W}\right)\left(⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)$
8 6 7 fnmpti ${⊢}\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\{⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\right\}\right)\cup \mathrm{LSpan}\left({U}\right)\left(\left\{{t}\right\}\right)\right)\to {y}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨{z},\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩,\mathrm{HVMap}\left({K}\right)\left({W}\right)\left(⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)Fn{V}$
9 eqid ${⊢}⟨{\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)}⟩$
10 eqid ${⊢}\mathrm{LSpan}\left({U}\right)=\mathrm{LSpan}\left({U}\right)$
11 eqid ${⊢}\mathrm{LCDual}\left({K}\right)\left({W}\right)=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
12 eqid ${⊢}{\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}={\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
13 eqid ${⊢}\mathrm{HVMap}\left({K}\right)\left({W}\right)=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
14 eqid ${⊢}\mathrm{HDMap1}\left({K}\right)\left({W}\right)=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
15 1 9 2 3 10 11 12 13 14 4 5 hdmapfval ${⊢}{\phi }\to {S}=\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\{⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\right\}\right)\cup \mathrm{LSpan}\left({U}\right)\left(\left\{{t}\right\}\right)\right)\to {y}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨{z},\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩,\mathrm{HVMap}\left({K}\right)\left({W}\right)\left(⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)$
16 15 fneq1d ${⊢}{\phi }\to \left({S}Fn{V}↔\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\{⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\right\}\right)\cup \mathrm{LSpan}\left({U}\right)\left(\left\{{t}\right\}\right)\right)\to {y}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨{z},\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩,\mathrm{HVMap}\left({K}\right)\left({W}\right)\left(⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\right),{z}⟩\right),{t}⟩\right)\right)\right)\right)Fn{V}\right)$
17 8 16 mpbiri ${⊢}{\phi }\to {S}Fn{V}$