# Metamath Proof Explorer

## 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 {G}Fn{B}$
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 {B}\phantom{\rule{.4em}{0ex}}{G}\left({z}\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left({K}\right)\left({W}\right)\right)}$
15 fnfvrnss ${⊢}\left({G}Fn{B}\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{G}\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}$