Theorem hgmaprnlem5N

Description: Lemma for hgmaprnN . Eliminate t . (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$$
Assertion	hgmaprnlem5N	$$⊢\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	1 2 3 7 16	dvh1dim	$$⊢\phi \to \exists t\in Vt\ne \underset{\dot{}}{0}$$
19		eldifsn	$$⊢t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(t\in V\wedge t\ne \underset{\dot{}}{0}\right)$$
20	16	adantr	$$⊢\left(\phi \wedge t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
21	17	adantr	$$⊢\left(\phi \wedge t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to z\in A$$
22		simpr	$$⊢\left(\phi \wedge t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
23	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 20 21 22	hgmaprnlem4N	$$⊢\left(\phi \wedge t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to z\in \mathrm{ran}G$$
24	19 23	sylan2br	$$⊢\left(\phi \wedge \left(t\in V\wedge t\ne \underset{\dot{}}{0}\right)\right)\to z\in \mathrm{ran}G$$
25	18 24	rexlimddv	$$⊢\phi \to z\in \mathrm{ran}G$$