Theorem hgmaprnlem1N

Description: Lemma for hgmaprnN . (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.k2	$$⊢\phi \to k\in B$$
	hgmaprnlem1.sk	$$⊢\phi \to s=k\underset{\dot{}}{·}t$$
Assertion	hgmaprnlem1N	$$⊢\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.k2	$$⊢\phi \to k\in B$$
22		hgmaprnlem1.sk	$$⊢\phi \to s=k\underset{\dot{}}{·}t$$
23	22	fveq2d	$$⊢\phi \to S\left(s\right)=S\left(k\underset{\dot{}}{·}t\right)$$
24	18	eldifad	$$⊢\phi \to t\in V$$
25	1 2 3 6 4 5 8 12 14 15 16 24 21	hgmapvs	$$⊢\phi \to S\left(k\underset{\dot{}}{·}t\right)=G\left(k\right)\underset{\dot{}}{\bullet }S\left(t\right)$$
26	23 20 25	3eqtr3d	$$⊢\phi \to z\underset{\dot{}}{\bullet }S\left(t\right)=G\left(k\right)\underset{\dot{}}{\bullet }S\left(t\right)$$
27	1 8 16	lcdlvec	$$⊢\phi \to C\in \mathrm{LVec}$$
28	1 2 4 5 8 10 11 15 16 21	hgmapdcl	$$⊢\phi \to G\left(k\right)\in A$$
29	1 2 3 8 9 14 16 24	hdmapcl	$$⊢\phi \to S\left(t\right)\in D$$
30		eldifsni	$$⊢t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to t\ne \underset{\dot{}}{0}$$
31	18 30	syl	$$⊢\phi \to t\ne \underset{\dot{}}{0}$$
32	1 2 3 7 8 13 14 16 24	hdmapeq0	$$⊢\phi \to \left(S\left(t\right)=Q\leftrightarrow t=\underset{\dot{}}{0}\right)$$
33	32	necon3bid	$$⊢\phi \to \left(S\left(t\right)\ne Q\leftrightarrow t\ne \underset{\dot{}}{0}\right)$$
34	31 33	mpbird	$$⊢\phi \to S\left(t\right)\ne Q$$
35	9 12 10 11 13 27 17 28 29 34	lvecvscan2	$$⊢\phi \to \left(z\underset{\dot{}}{\bullet }S\left(t\right)=G\left(k\right)\underset{\dot{}}{\bullet }S\left(t\right)\leftrightarrow z=G\left(k\right)\right)$$
36	26 35	mpbid	$$⊢\phi \to z=G\left(k\right)$$
37	1 2 4 5 15 16	hgmapfnN	$$⊢\phi \to GFnB$$
38		fnfvelrn	$$⊢\left(GFnB\wedge k\in B\right)\to G\left(k\right)\in \mathrm{ran}G$$
39	37 21 38	syl2anc	$$⊢\phi \to G\left(k\right)\in \mathrm{ran}G$$
40	36 39	eqeltrd	$$⊢\phi \to z\in \mathrm{ran}G$$