Theorem hdmaprnlem15N

Description: Lemma for hdmaprnN . Eliminate u . (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)$$
	hdmaprnlem15.se	$$⊢\phi \to s\in \left(D\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmaprnlem15.ve	$$⊢\phi \to v\in V$$
	hdmaprnlem15.e	$$⊢\phi \to M\left(N\left(\left\{v\right\}\right)\right)=L\left(\left\{s\right\}\right)$$
Assertion	hdmaprnlem15N	$$⊢\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		hdmaprnlem15.se	$$⊢\phi \to s\in \left(D\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
13		hdmaprnlem15.ve	$$⊢\phi \to v\in V$$
14		hdmaprnlem15.e	$$⊢\phi \to M\left(N\left(\left\{v\right\}\right)\right)=L\left(\left\{s\right\}\right)$$
15	1 2 3 4 11 13	dvh2dim	$$⊢\phi \to \exists t\in V\neg t\in N\left(\left\{v\right\}\right)$$
16	11	3ad2ant1	$$⊢\left(\phi \wedge t\in V\wedge \neg t\in N\left(\left\{v\right\}\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
17	12	3ad2ant1	$$⊢\left(\phi \wedge t\in V\wedge \neg t\in N\left(\left\{v\right\}\right)\right)\to s\in \left(D\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
18	13	3ad2ant1	$$⊢\left(\phi \wedge t\in V\wedge \neg t\in N\left(\left\{v\right\}\right)\right)\to v\in V$$
19	14	3ad2ant1	$$⊢\left(\phi \wedge t\in V\wedge \neg t\in N\left(\left\{v\right\}\right)\right)\to M\left(N\left(\left\{v\right\}\right)\right)=L\left(\left\{s\right\}\right)$$
20		simp2	$$⊢\left(\phi \wedge t\in V\wedge \neg t\in N\left(\left\{v\right\}\right)\right)\to t\in V$$
21		simp3	$$⊢\left(\phi \wedge t\in V\wedge \neg t\in N\left(\left\{v\right\}\right)\right)\to \neg t\in N\left(\left\{v\right\}\right)$$
22		eqid	$$⊢0_U=0_U$$
23		eqid	$$⊢{+}_C={+}_C$$
24		eqid	$$⊢{+}_U={+}_U$$
25	1 2 3 4 5 8 9 10 16 17 18 19 20 21 6 7 22 23 24	hdmaprnlem11N	$$⊢\left(\phi \wedge t\in V\wedge \neg t\in N\left(\left\{v\right\}\right)\right)\to s\in \mathrm{ran}S$$
26	25	rexlimdv3a	$$⊢\phi \to \left(\exists t\in V\neg t\in N\left(\left\{v\right\}\right)\to s\in \mathrm{ran}S\right)$$
27	15 26	mpd	$$⊢\phi \to s\in \mathrm{ran}S$$