Theorem hdmaprnlem10N

Description: Lemma for hdmaprnN . Show s is in the range of S . (Contributed by NM, 29-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hdmaprnlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmaprnlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmaprnlem1.v	$$⊢V={\mathrm{Base}}_U$$
	hdmaprnlem1.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hdmaprnlem1.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmaprnlem1.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
	hdmaprnlem1.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	hdmaprnlem1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmaprnlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmaprnlem1.se	$$⊢\phi \to s\in \left(D\setminus \left\{Q\right\}\right)$$
	hdmaprnlem1.ve	$$⊢\phi \to v\in V$$
	hdmaprnlem1.e	$$⊢\phi \to M\left(N\left(\left\{v\right\}\right)\right)=L\left(\left\{s\right\}\right)$$
	hdmaprnlem1.ue	$$⊢\phi \to u\in V$$
	hdmaprnlem1.un	$$⊢\phi \to \neg u\in N\left(\left\{v\right\}\right)$$
	hdmaprnlem1.d	$$⊢D={\mathrm{Base}}_C$$
	hdmaprnlem1.q	$$⊢Q=0_C$$
	hdmaprnlem1.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmaprnlem1.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
	hdmaprnlem3e.p	$$⊢\underset{\dot{}}{+}={+}_U$$
Assertion	hdmaprnlem10N	$$⊢\phi \to \exists t\in VS\left(t\right)=s$$

Proof

Step	Hyp	Ref	Expression
1		hdmaprnlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmaprnlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmaprnlem1.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmaprnlem1.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
5		hdmaprnlem1.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		hdmaprnlem1.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
7		hdmaprnlem1.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
8		hdmaprnlem1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
9		hdmaprnlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		hdmaprnlem1.se	$$⊢\phi \to s\in \left(D\setminus \left\{Q\right\}\right)$$
11		hdmaprnlem1.ve	$$⊢\phi \to v\in V$$
12		hdmaprnlem1.e	$$⊢\phi \to M\left(N\left(\left\{v\right\}\right)\right)=L\left(\left\{s\right\}\right)$$
13		hdmaprnlem1.ue	$$⊢\phi \to u\in V$$
14		hdmaprnlem1.un	$$⊢\phi \to \neg u\in N\left(\left\{v\right\}\right)$$
15		hdmaprnlem1.d	$$⊢D={\mathrm{Base}}_C$$
16		hdmaprnlem1.q	$$⊢Q=0_C$$
17		hdmaprnlem1.o	$$⊢\underset{\dot{}}{0}=0_U$$
18		hdmaprnlem1.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
19		hdmaprnlem3e.p	$$⊢\underset{\dot{}}{+}={+}_U$$
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	hdmaprnlem3eN	$$⊢\phi \to \exists t\in \left(N\left(\left\{v\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)=M\left(N\left(\left\{u\underset{\dot{}}{+}t\right\}\right)\right)$$
21	9	adantr	$$⊢\left(\phi \wedge \left(t\in \left(N\left(\left\{v\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)=M\left(N\left(\left\{u\underset{\dot{}}{+}t\right\}\right)\right)\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
22	10	adantr	$$⊢\left(\phi \wedge \left(t\in \left(N\left(\left\{v\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)=M\left(N\left(\left\{u\underset{\dot{}}{+}t\right\}\right)\right)\right)\right)\to s\in \left(D\setminus \left\{Q\right\}\right)$$
23	11	adantr	$$⊢\left(\phi \wedge \left(t\in \left(N\left(\left\{v\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)=M\left(N\left(\left\{u\underset{\dot{}}{+}t\right\}\right)\right)\right)\right)\to v\in V$$
24	12	adantr	$$⊢\left(\phi \wedge \left(t\in \left(N\left(\left\{v\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)=M\left(N\left(\left\{u\underset{\dot{}}{+}t\right\}\right)\right)\right)\right)\to M\left(N\left(\left\{v\right\}\right)\right)=L\left(\left\{s\right\}\right)$$
25	13	adantr	$$⊢\left(\phi \wedge \left(t\in \left(N\left(\left\{v\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)=M\left(N\left(\left\{u\underset{\dot{}}{+}t\right\}\right)\right)\right)\right)\to u\in V$$
26	14	adantr	$$⊢\left(\phi \wedge \left(t\in \left(N\left(\left\{v\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)=M\left(N\left(\left\{u\underset{\dot{}}{+}t\right\}\right)\right)\right)\right)\to \neg u\in N\left(\left\{v\right\}\right)$$
27		simprl	$$⊢\left(\phi \wedge \left(t\in \left(N\left(\left\{v\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)=M\left(N\left(\left\{u\underset{\dot{}}{+}t\right\}\right)\right)\right)\right)\to t\in \left(N\left(\left\{v\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
28	1 2 3 4 5 6 7 8 21 22 23 24 25 26 15 16 17 18 27	hdmaprnlem4tN	$$⊢\left(\phi \wedge \left(t\in \left(N\left(\left\{v\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)=M\left(N\left(\left\{u\underset{\dot{}}{+}t\right\}\right)\right)\right)\right)\to t\in V$$
29		simprr	$$⊢\left(\phi \wedge \left(t\in \left(N\left(\left\{v\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)=M\left(N\left(\left\{u\underset{\dot{}}{+}t\right\}\right)\right)\right)\right)\to L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)=M\left(N\left(\left\{u\underset{\dot{}}{+}t\right\}\right)\right)$$
30	1 2 3 4 5 6 7 8 21 22 23 24 25 26 15 16 17 18 27 19 29	hdmaprnlem9N	$$⊢\left(\phi \wedge \left(t\in \left(N\left(\left\{v\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)=M\left(N\left(\left\{u\underset{\dot{}}{+}t\right\}\right)\right)\right)\right)\to s=S\left(t\right)$$
31	30	eqcomd	$$⊢\left(\phi \wedge \left(t\in \left(N\left(\left\{v\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge L\left(\left\{S\left(u\right)\underset{\dot{}}{✚}s\right\}\right)=M\left(N\left(\left\{u\underset{\dot{}}{+}t\right\}\right)\right)\right)\right)\to S\left(t\right)=s$$
32	20 28 31	reximssdv	$$⊢\phi \to \exists t\in VS\left(t\right)=s$$