# Metamath Proof Explorer

## 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
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.k2 ${⊢}{\phi }\to {k}\in {B}$
hgmaprnlem1.sk
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
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.k2 ${⊢}{\phi }\to {k}\in {B}$
22 hgmaprnlem1.sk
23 22 fveq2d
24 18 eldifad ${⊢}{\phi }\to {t}\in {V}$
25 1 2 3 6 4 5 8 12 14 15 16 24 21 hgmapvs
26 23 20 25 3eqtr3d
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
31 18 30 syl
32 1 2 3 7 8 13 14 16 24 hdmapeq0
33 32 necon3bid
34 31 33 mpbird ${⊢}{\phi }\to {S}\left({t}\right)\ne {Q}$
35 9 12 10 11 13 27 17 28 29 34 lvecvscan2
36 26 35 mpbid ${⊢}{\phi }\to {z}={G}\left({k}\right)$
37 1 2 4 5 15 16 hgmapfnN ${⊢}{\phi }\to {G}Fn{B}$
38 fnfvelrn ${⊢}\left({G}Fn{B}\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}$