Theorem hgmaprnlem3N

Description: Lemma for hgmaprnN . Eliminate k . (Contributed by NM, 7-Jun-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hgmaprnlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hgmaprnlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hgmaprnlem1.v	$$⊢V={\mathrm{Base}}_U$$
	hgmaprnlem1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hgmaprnlem1.b	$$⊢B={\mathrm{Base}}_R$$
	hgmaprnlem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hgmaprnlem1.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hgmaprnlem1.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hgmaprnlem1.d	$$⊢D={\mathrm{Base}}_C$$
	hgmaprnlem1.p	$$⊢P=\mathrm{Scalar}\left(C\right)$$
	hgmaprnlem1.a	$$⊢A={\mathrm{Base}}_P$$
	hgmaprnlem1.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
	hgmaprnlem1.q	$$⊢Q=0_C$$
	hgmaprnlem1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hgmaprnlem1.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
	hgmaprnlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hgmaprnlem1.z	$$⊢\phi \to z\in A$$
	hgmaprnlem1.t2	$$⊢\phi \to t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hgmaprnlem1.s2	$$⊢\phi \to s\in V$$
	hgmaprnlem1.sz	$$⊢\phi \to S\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)$$
	hgmaprnlem1.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	hgmaprnlem1.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hgmaprnlem1.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
Assertion	hgmaprnlem3N	$$⊢\phi \to z\in \mathrm{ran}G$$

Proof

Step	Hyp	Ref	Expression
1		hgmaprnlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hgmaprnlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hgmaprnlem1.v	$$⊢V={\mathrm{Base}}_U$$
4		hgmaprnlem1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
5		hgmaprnlem1.b	$$⊢B={\mathrm{Base}}_R$$
6		hgmaprnlem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
7		hgmaprnlem1.o	$$⊢\underset{\dot{}}{0}=0_U$$
8		hgmaprnlem1.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
9		hgmaprnlem1.d	$$⊢D={\mathrm{Base}}_C$$
10		hgmaprnlem1.p	$$⊢P=\mathrm{Scalar}\left(C\right)$$
11		hgmaprnlem1.a	$$⊢A={\mathrm{Base}}_P$$
12		hgmaprnlem1.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
13		hgmaprnlem1.q	$$⊢Q=0_C$$
14		hgmaprnlem1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
15		hgmaprnlem1.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
16		hgmaprnlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
17		hgmaprnlem1.z	$$⊢\phi \to z\in A$$
18		hgmaprnlem1.t2	$$⊢\phi \to t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
19		hgmaprnlem1.s2	$$⊢\phi \to s\in V$$
20		hgmaprnlem1.sz	$$⊢\phi \to S\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)$$
21		hgmaprnlem1.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
22		hgmaprnlem1.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
23		hgmaprnlem1.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
24	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23	hgmaprnlem2N	$$⊢\phi \to N\left(\left\{s\right\}\right)\subseteq N\left(\left\{t\right\}\right)$$
25	1 2 16	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
26	18	eldifad	$$⊢\phi \to t\in V$$
27	3 4 5 6 22 25 19 26	lspsnss2	$$⊢\phi \to \left(N\left(\left\{s\right\}\right)\subseteq N\left(\left\{t\right\}\right)\leftrightarrow \exists k\in Bs=k\underset{\dot{}}{·}t\right)$$
28	24 27	mpbid	$$⊢\phi \to \exists k\in Bs=k\underset{\dot{}}{·}t$$
29	16	3ad2ant1	$$⊢\left(\phi \wedge k\in B\wedge s=k\underset{\dot{}}{·}t\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
30	17	3ad2ant1	$$⊢\left(\phi \wedge k\in B\wedge s=k\underset{\dot{}}{·}t\right)\to z\in A$$
31	18	3ad2ant1	$$⊢\left(\phi \wedge k\in B\wedge s=k\underset{\dot{}}{·}t\right)\to t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
32	19	3ad2ant1	$$⊢\left(\phi \wedge k\in B\wedge s=k\underset{\dot{}}{·}t\right)\to s\in V$$
33	20	3ad2ant1	$$⊢\left(\phi \wedge k\in B\wedge s=k\underset{\dot{}}{·}t\right)\to S\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)$$
34		simp2	$$⊢\left(\phi \wedge k\in B\wedge s=k\underset{\dot{}}{·}t\right)\to k\in B$$
35		simp3	$$⊢\left(\phi \wedge k\in B\wedge s=k\underset{\dot{}}{·}t\right)\to s=k\underset{\dot{}}{·}t$$
36	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 29 30 31 32 33 34 35	hgmaprnlem1N	$$⊢\left(\phi \wedge k\in B\wedge s=k\underset{\dot{}}{·}t\right)\to z\in \mathrm{ran}G$$
37	36	rexlimdv3a	$$⊢\phi \to \left(\exists k\in Bs=k\underset{\dot{}}{·}t\to z\in \mathrm{ran}G\right)$$
38	28 37	mpd	$$⊢\phi \to z\in \mathrm{ran}G$$