# Metamath Proof Explorer

## Theorem hdmapcl

Description: Closure of map from vectors to functionals with closed kernels. (Contributed by NM, 15-May-2015)

Ref Expression
Hypotheses hdmapcl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmapcl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmapcl.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmapcl.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
hdmapcl.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
hdmapcl.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
hdmapcl.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hdmapcl.t ${⊢}{\phi }\to {T}\in {V}$
Assertion hdmapcl ${⊢}{\phi }\to {S}\left({T}\right)\in {D}$

### Proof

Step Hyp Ref Expression
1 hdmapcl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmapcl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hdmapcl.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 hdmapcl.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
5 hdmapcl.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
6 hdmapcl.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
7 hdmapcl.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
8 hdmapcl.t ${⊢}{\phi }\to {T}\in {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{HVMap}\left({K}\right)\left({W}\right)=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
12 eqid ${⊢}\mathrm{HDMap1}\left({K}\right)\left({W}\right)=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
13 1 9 2 3 10 4 5 11 12 6 7 8 hdmapval ${⊢}{\phi }\to {S}\left({T}\right)=\left(\iota {h}\in {D}|\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{y}\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 {h}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨{y},\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),{y}⟩\right),{T}⟩\right)\right)\right)$
14 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
15 eqid ${⊢}\mathrm{LSpan}\left({C}\right)=\mathrm{LSpan}\left({C}\right)$
16 eqid ${⊢}\mathrm{mapd}\left({K}\right)\left({W}\right)=\mathrm{mapd}\left({K}\right)\left({W}\right)$
17 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
18 eqid ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
19 1 17 18 2 3 14 9 7 dvheveccl ${⊢}{\phi }\to ⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩\in \left({V}\setminus \left\{{0}_{{U}}\right\}\right)$
20 1 2 3 14 10 4 15 16 11 7 19 mapdhvmap ${⊢}{\phi }\to \mathrm{mapd}\left({K}\right)\left({W}\right)\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)\right)=\mathrm{LSpan}\left({C}\right)\left(\left\{\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)\right\}\right)$
21 eqid ${⊢}{0}_{{C}}={0}_{{C}}$
22 1 2 3 14 4 5 21 11 7 19 hvmapcl2 ${⊢}{\phi }\to \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)\in \left({D}\setminus \left\{{0}_{{C}}\right\}\right)$
23 22 eldifad ${⊢}{\phi }\to \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)\in {D}$
24 1 2 3 14 10 4 5 15 16 12 7 20 19 23 8 hdmap1eu ${⊢}{\phi }\to \exists !{h}\in {D}\phantom{\rule{.4em}{0ex}}\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{y}\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 {h}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨{y},\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),{y}⟩\right),{T}⟩\right)\right)$
25 riotacl ${⊢}\exists !{h}\in {D}\phantom{\rule{.4em}{0ex}}\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{y}\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 {h}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨{y},\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),{y}⟩\right),{T}⟩\right)\right)\to \left(\iota {h}\in {D}|\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{y}\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 {h}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨{y},\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),{y}⟩\right),{T}⟩\right)\right)\right)\in {D}$
26 24 25 syl ${⊢}{\phi }\to \left(\iota {h}\in {D}|\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{y}\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 {h}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)\left(⟨{y},\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),{y}⟩\right),{T}⟩\right)\right)\right)\in {D}$
27 13 26 eqeltrd ${⊢}{\phi }\to {S}\left({T}\right)\in {D}$