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}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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\left(\neg y\in \left(\mathrm{LSpan}\left(U\right)\left(\left\{⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩,\mathrm{HVMap}\left(K\right)\left(W\right)\left(⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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\forall y\in V\left(\neg y\in \left(\mathrm{LSpan}\left(U\right)\left(\left\{⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩,\mathrm{HVMap}\left(K\right)\left(W\right)\left(⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩\right),y⟩\right),T⟩\right)\right)$$
25		riotacl	$$⊢\exists !h\in D\forall y\in V\left(\neg y\in \left(\mathrm{LSpan}\left(U\right)\left(\left\{⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩,\mathrm{HVMap}\left(K\right)\left(W\right)\left(⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩\right),y⟩\right),T⟩\right)\right)\to \left(\iota h\in D|\forall y\in V\left(\neg y\in \left(\mathrm{LSpan}\left(U\right)\left(\left\{⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩,\mathrm{HVMap}\left(K\right)\left(W\right)\left(⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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\left(\neg y\in \left(\mathrm{LSpan}\left(U\right)\left(\left\{⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩,\mathrm{HVMap}\left(K\right)\left(W\right)\left(⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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$$