Theorem hdmaprnlem17N

Description: Lemma for hdmaprnN . Include zero. (Contributed by NM, 30-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hdmaprnlem15.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmaprnlem15.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmaprnlem15.v	$$⊢V={\mathrm{Base}}_U$$
	hdmaprnlem15.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hdmaprnlem15.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmaprnlem15.d	$$⊢D={\mathrm{Base}}_C$$
	hdmaprnlem15.q	$$⊢\underset{\dot{}}{0}=0_C$$
	hdmaprnlem15.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
	hdmaprnlem15.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	hdmaprnlem15.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmaprnlem15.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmaprnlem17.se	$$⊢\phi \to s\in D$$
Assertion	hdmaprnlem17N	$$⊢\phi \to s\in \mathrm{ran}S$$

Proof

Step	Hyp	Ref	Expression
1		hdmaprnlem15.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmaprnlem15.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmaprnlem15.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmaprnlem15.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
5		hdmaprnlem15.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		hdmaprnlem15.d	$$⊢D={\mathrm{Base}}_C$$
7		hdmaprnlem15.q	$$⊢\underset{\dot{}}{0}=0_C$$
8		hdmaprnlem15.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
9		hdmaprnlem15.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
10		hdmaprnlem15.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
11		hdmaprnlem15.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		hdmaprnlem17.se	$$⊢\phi \to s\in D$$
13		eleq1	$$⊢s=\underset{\dot{}}{0}\to \left(s\in \mathrm{ran}S\leftrightarrow \underset{\dot{}}{0}\in \mathrm{ran}S\right)$$
14	11	adantr	$$⊢\left(\phi \wedge s\ne \underset{\dot{}}{0}\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
15	12	anim1i	$$⊢\left(\phi \wedge s\ne \underset{\dot{}}{0}\right)\to \left(s\in D\wedge s\ne \underset{\dot{}}{0}\right)$$
16		eldifsn	$$⊢s\in \left(D\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(s\in D\wedge s\ne \underset{\dot{}}{0}\right)$$
17	15 16	sylibr	$$⊢\left(\phi \wedge s\ne \underset{\dot{}}{0}\right)\to s\in \left(D\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
18	1 2 3 4 5 6 7 8 9 10 14 17	hdmaprnlem16N	$$⊢\left(\phi \wedge s\ne \underset{\dot{}}{0}\right)\to s\in \mathrm{ran}S$$
19		eqid	$$⊢0_U=0_U$$
20	1 2 19 5 7 10 11	hdmapval0	$$⊢\phi \to S\left(0_U\right)=\underset{\dot{}}{0}$$
21	1 2 3 10 11	hdmapfnN	$$⊢\phi \to SFnV$$
22	1 2 11	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
23	3 19	lmod0vcl	$$⊢U\in \mathrm{LMod}\to 0_U\in V$$
24	22 23	syl	$$⊢\phi \to 0_U\in V$$
25		fnfvelrn	$$⊢\left(SFnV\wedge 0_U\in V\right)\to S\left(0_U\right)\in \mathrm{ran}S$$
26	21 24 25	syl2anc	$$⊢\phi \to S\left(0_U\right)\in \mathrm{ran}S$$
27	20 26	eqeltrrd	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{ran}S$$
28	13 18 27	pm2.61ne	$$⊢\phi \to s\in \mathrm{ran}S$$