# Metamath Proof Explorer

## Theorem hgmaprnlem2N

Description: Lemma for hgmaprnN . Part 15 of Baer p. 50 line 20. We only require a subset relation, rather than equality, so that the case of zero z is taken care of automatically. (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 hgmaprnlem2N ${⊢}{\phi }\to {N}\left(\left\{{s}\right\}\right)\subseteq {N}\left(\left\{{t}\right\}\right)$

### 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 8 16 lcdlmod ${⊢}{\phi }\to {C}\in \mathrm{LMod}$
25 18 eldifad ${⊢}{\phi }\to {t}\in {V}$
26 1 2 3 8 9 14 16 25 hdmapcl ${⊢}{\phi }\to {S}\left({t}\right)\in {D}$
27 10 11 9 12 23 lspsnvsi
28 24 17 26 27 syl3anc
29 1 2 3 22 8 23 21 14 16 19 hdmap10 ${⊢}{\phi }\to {M}\left({N}\left(\left\{{s}\right\}\right)\right)={L}\left(\left\{{S}\left({s}\right)\right\}\right)$
30 20 sneqd
31 30 fveq2d
32 29 31 eqtrd
33 1 2 3 22 8 23 21 14 16 25 hdmap10 ${⊢}{\phi }\to {M}\left({N}\left(\left\{{t}\right\}\right)\right)={L}\left(\left\{{S}\left({t}\right)\right\}\right)$
34 28 32 33 3sstr4d ${⊢}{\phi }\to {M}\left({N}\left(\left\{{s}\right\}\right)\right)\subseteq {M}\left({N}\left(\left\{{t}\right\}\right)\right)$
35 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
36 1 2 16 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
37 3 35 22 lspsncl ${⊢}\left({U}\in \mathrm{LMod}\wedge {s}\in {V}\right)\to {N}\left(\left\{{s}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
38 36 19 37 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{s}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
39 3 35 22 lspsncl ${⊢}\left({U}\in \mathrm{LMod}\wedge {t}\in {V}\right)\to {N}\left(\left\{{t}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
40 36 25 39 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{t}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
41 1 2 35 21 16 38 40 mapdord ${⊢}{\phi }\to \left({M}\left({N}\left(\left\{{s}\right\}\right)\right)\subseteq {M}\left({N}\left(\left\{{t}\right\}\right)\right)↔{N}\left(\left\{{s}\right\}\right)\subseteq {N}\left(\left\{{t}\right\}\right)\right)$
42 34 41 mpbid ${⊢}{\phi }\to {N}\left(\left\{{s}\right\}\right)\subseteq {N}\left(\left\{{t}\right\}\right)$