Theorem hgmaprnN

Description: Part of proof of part 16 in Baer p. 50 line 23, Fs=G, except that we use the original vector space scalars for the range. (Contributed by NM, 7-Jun-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hgmaprn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hgmaprn.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hgmaprn.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hgmaprn.b	$$⊢B={\mathrm{Base}}_R$$
	hgmaprn.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
	hgmaprn.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	hgmaprnN	$$⊢\phi \to \mathrm{ran}G=B$$

Proof

Step	Hyp	Ref	Expression
1		hgmaprn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hgmaprn.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hgmaprn.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
4		hgmaprn.b	$$⊢B={\mathrm{Base}}_R$$
5		hgmaprn.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
6		hgmaprn.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7	1 2 3 4 5 6	hgmapfnN	$$⊢\phi \to GFnB$$
8		eqid	$$⊢\mathrm{LCDual}\left(K\right)\left(W\right)=\mathrm{LCDual}\left(K\right)\left(W\right)$$
9		eqid	$$⊢\mathrm{Scalar}\left(\mathrm{LCDual}\left(K\right)\left(W\right)\right)=\mathrm{Scalar}\left(\mathrm{LCDual}\left(K\right)\left(W\right)\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left(K\right)\left(W\right)\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left(K\right)\left(W\right)\right)}$$
11	6	adantr	$$⊢\left(\phi \wedge z\in B\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		simpr	$$⊢\left(\phi \wedge z\in B\right)\to z\in B$$
13	1 2 3 4 8 9 10 5 11 12	hgmapdcl	$$⊢\left(\phi \wedge z\in B\right)\to G\left(z\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left(K\right)\left(W\right)\right)}$$
14	13	ralrimiva	$$⊢\phi \to \forall z\in BG\left(z\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left(K\right)\left(W\right)\right)}$$
15		fnfvrnss	$$⊢\left(GFnB\wedge \forall z\in BG\left(z\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left(K\right)\left(W\right)\right)}\right)\to \mathrm{ran}G\subseteq {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left(K\right)\left(W\right)\right)}$$
16	7 14 15	syl2anc	$$⊢\phi \to \mathrm{ran}G\subseteq {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left(K\right)\left(W\right)\right)}$$
17		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
18		eqid	$$⊢{\cdot }_U={\cdot }_U$$
19		eqid	$$⊢0_U=0_U$$
20		eqid	$$⊢{\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}={\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
21		eqid	$$⊢{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}={\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
22		eqid	$$⊢0_{\mathrm{LCDual}\left(K\right)\left(W\right)}=0_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
23		eqid	$$⊢\mathrm{HDMap}\left(K\right)\left(W\right)=\mathrm{HDMap}\left(K\right)\left(W\right)$$
24	6	adantr	$$⊢\left(\phi \wedge z\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left(K\right)\left(W\right)\right)}\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
25		simpr	$$⊢\left(\phi \wedge z\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left(K\right)\left(W\right)\right)}\right)\to z\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left(K\right)\left(W\right)\right)}$$
26	1 2 17 3 4 18 19 8 20 9 10 21 22 23 5 24 25	hgmaprnlem5N	$$⊢\left(\phi \wedge z\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left(K\right)\left(W\right)\right)}\right)\to z\in \mathrm{ran}G$$
27	16 26	eqelssd	$$⊢\phi \to \mathrm{ran}G={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left(K\right)\left(W\right)\right)}$$
28	1 2 3 4 8 9 10 6	lcdsbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left(K\right)\left(W\right)\right)}=B$$
29	27 28	eqtrd	$$⊢\phi \to \mathrm{ran}G=B$$