Metamath Proof Explorer

Theorem hgmaprnlem4N

Description: Lemma for hgmaprnN . Eliminate s . (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
Assertion hgmaprnlem4N ${⊢}{\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 1 8 16 lcdlmod ${⊢}{\phi }\to {C}\in \mathrm{LMod}$
20 18 eldifad ${⊢}{\phi }\to {t}\in {V}$
21 1 2 3 8 9 14 16 20 hdmapcl ${⊢}{\phi }\to {S}\left({t}\right)\in {D}$
22 9 10 12 11 lmodvscl
23 19 17 21 22 syl3anc
24 1 8 9 14 16 hdmaprnN ${⊢}{\phi }\to \mathrm{ran}{S}={D}$
25 23 24 eleqtrrd
26 1 2 3 14 16 hdmapfnN ${⊢}{\phi }\to {S}Fn{V}$
27 fvelrnb
28 26 27 syl
29 25 28 mpbid
35 eqid ${⊢}\mathrm{mapd}\left({K}\right)\left({W}\right)=\mathrm{mapd}\left({K}\right)\left({W}\right)$
36 eqid ${⊢}\mathrm{LSpan}\left({U}\right)=\mathrm{LSpan}\left({U}\right)$
37 eqid ${⊢}\mathrm{LSpan}\left({C}\right)=\mathrm{LSpan}\left({C}\right)$
40 29 39 mpd ${⊢}{\phi }\to {z}\in \mathrm{ran}{G}$