# Metamath Proof Explorer

## 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
hgmaprnlem1.o
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
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
7 hgmaprnlem1.o
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
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
19 eldifsn
25 18 24 rexlimddv ${⊢}{\phi }\to {z}\in \mathrm{ran}{G}$