Theorem hgmaprnlem4N

Description: Lemma for hgmaprnN . Eliminate s . (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)$$
Assertion	hgmaprnlem4N	$$⊢\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	1 8 16	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
20	18	eldifad	$$⊢\phi \to t\in V$$
21	1 2 3 8 9 14 16 20	hdmapcl	$$⊢\phi \to S\left(t\right)\in D$$
22	9 10 12 11	lmodvscl	$$⊢\left(C\in \mathrm{LMod}\wedge z\in A\wedge S\left(t\right)\in D\right)\to z\underset{\dot{}}{\bullet }S\left(t\right)\in D$$
23	19 17 21 22	syl3anc	$$⊢\phi \to z\underset{\dot{}}{\bullet }S\left(t\right)\in D$$
24	1 8 9 14 16	hdmaprnN	$$⊢\phi \to \mathrm{ran}S=D$$
25	23 24	eleqtrrd	$$⊢\phi \to z\underset{\dot{}}{\bullet }S\left(t\right)\in \mathrm{ran}S$$
26	1 2 3 14 16	hdmapfnN	$$⊢\phi \to SFnV$$
27		fvelrnb	$$⊢SFnV\to \left(z\underset{\dot{}}{\bullet }S\left(t\right)\in \mathrm{ran}S\leftrightarrow \exists s\in VS\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)\right)$$
28	26 27	syl	$$⊢\phi \to \left(z\underset{\dot{}}{\bullet }S\left(t\right)\in \mathrm{ran}S\leftrightarrow \exists s\in VS\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)\right)$$
29	25 28	mpbid	$$⊢\phi \to \exists s\in VS\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)$$
30	16	3ad2ant1	$$⊢\left(\phi \wedge s\in V\wedge S\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
31	17	3ad2ant1	$$⊢\left(\phi \wedge s\in V\wedge S\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)\right)\to z\in A$$
32	18	3ad2ant1	$$⊢\left(\phi \wedge s\in V\wedge S\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)\right)\to t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
33		simp2	$$⊢\left(\phi \wedge s\in V\wedge S\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)\right)\to s\in V$$
34		simp3	$$⊢\left(\phi \wedge s\in V\wedge S\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)\right)\to S\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)$$
35		eqid	$$⊢\mathrm{mapd}\left(K\right)\left(W\right)=\mathrm{mapd}\left(K\right)\left(W\right)$$
36		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
37		eqid	$$⊢\mathrm{LSpan}\left(C\right)=\mathrm{LSpan}\left(C\right)$$
38	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 30 31 32 33 34 35 36 37	hgmaprnlem3N	$$⊢\left(\phi \wedge s\in V\wedge S\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)\right)\to z\in \mathrm{ran}G$$
39	38	rexlimdv3a	$$⊢\phi \to \left(\exists s\in VS\left(s\right)=z\underset{\dot{}}{\bullet }S\left(t\right)\to z\in \mathrm{ran}G\right)$$
40	29 39	mpd	$$⊢\phi \to z\in \mathrm{ran}G$$