Theorem hdmapnzcl

Description: Nonzero vector closure of map from vectors to functionals with closed kernels. (Contributed by NM, 27-May-2015)

	Ref	Expression
Hypotheses	hdmapnzcl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmapnzcl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmapnzcl.v	$$⊢V={\mathrm{Base}}_U$$
	hdmapnzcl.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmapnzcl.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmapnzcl.q	$$⊢Q=0_C$$
	hdmapnzcl.d	$$⊢D={\mathrm{Base}}_C$$
	hdmapnzcl.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmapnzcl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmapnzcl.t	$$⊢\phi \to T\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	hdmapnzcl	$$⊢\phi \to S\left(T\right)\in \left(D\setminus \left\{Q\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmapnzcl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapnzcl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmapnzcl.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmapnzcl.o	$$⊢\underset{\dot{}}{0}=0_U$$
5		hdmapnzcl.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		hdmapnzcl.q	$$⊢Q=0_C$$
7		hdmapnzcl.d	$$⊢D={\mathrm{Base}}_C$$
8		hdmapnzcl.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
9		hdmapnzcl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		hdmapnzcl.t	$$⊢\phi \to T\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
11	10	eldifad	$$⊢\phi \to T\in V$$
12	1 2 3 5 7 8 9 11	hdmapcl	$$⊢\phi \to S\left(T\right)\in D$$
13		eldifsni	$$⊢T\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to T\ne \underset{\dot{}}{0}$$
14	10 13	syl	$$⊢\phi \to T\ne \underset{\dot{}}{0}$$
15	1 2 3 4 5 6 8 9 11	hdmapeq0	$$⊢\phi \to \left(S\left(T\right)=Q\leftrightarrow T=\underset{\dot{}}{0}\right)$$
16	15	necon3bid	$$⊢\phi \to \left(S\left(T\right)\ne Q\leftrightarrow T\ne \underset{\dot{}}{0}\right)$$
17	14 16	mpbird	$$⊢\phi \to S\left(T\right)\ne Q$$
18		eldifsn	$$⊢S\left(T\right)\in \left(D\setminus \left\{Q\right\}\right)\leftrightarrow \left(S\left(T\right)\in D\wedge S\left(T\right)\ne Q\right)$$
19	12 17 18	sylanbrc	$$⊢\phi \to S\left(T\right)\in \left(D\setminus \left\{Q\right\}\right)$$