# Metamath Proof Explorer

## Theorem hgmaprnlem3N

Description: Lemma for hgmaprnN . Eliminate k . (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}$
hgmaprnlem1.t2
hgmaprnlem1.s2 ${⊢}{\phi }\to {s}\in {V}$
hgmaprnlem1.sz
hgmaprnlem1.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
hgmaprnlem1.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
hgmaprnlem1.l ${⊢}{L}=\mathrm{LSpan}\left({C}\right)$
Assertion hgmaprnlem3N ${⊢}{\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 hgmaprnlem1.t2
19 hgmaprnlem1.s2 ${⊢}{\phi }\to {s}\in {V}$
20 hgmaprnlem1.sz
21 hgmaprnlem1.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
22 hgmaprnlem1.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
23 hgmaprnlem1.l ${⊢}{L}=\mathrm{LSpan}\left({C}\right)$
24 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 hgmaprnlem2N ${⊢}{\phi }\to {N}\left(\left\{{s}\right\}\right)\subseteq {N}\left(\left\{{t}\right\}\right)$
25 1 2 16 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
26 18 eldifad ${⊢}{\phi }\to {t}\in {V}$
27 3 4 5 6 22 25 19 26 lspsnss2
28 24 27 mpbid
38 28 37 mpd ${⊢}{\phi }\to {z}\in \mathrm{ran}{G}$