# Metamath Proof Explorer

## Theorem mapdpglem2a

Description: Lemma for mapdpg . (Contributed by NM, 20-Mar-2015)

Ref Expression
Hypotheses mapdpglem.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
mapdpglem.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
mapdpglem.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
mapdpglem.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
mapdpglem.s
mapdpglem.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
mapdpglem.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
mapdpglem.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
mapdpglem.x ${⊢}{\phi }\to {X}\in {V}$
mapdpglem.y ${⊢}{\phi }\to {Y}\in {V}$
mapdpglem1.p
mapdpglem2.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
mapdpglem3.f ${⊢}{F}={\mathrm{Base}}_{{C}}$
mapdpglem3.te
Assertion mapdpglem2a ${⊢}{\phi }\to {t}\in {F}$

### Proof

Step Hyp Ref Expression
1 mapdpglem.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 mapdpglem.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
3 mapdpglem.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 mapdpglem.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 mapdpglem.s
6 mapdpglem.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
7 mapdpglem.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
8 mapdpglem.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
9 mapdpglem.x ${⊢}{\phi }\to {X}\in {V}$
10 mapdpglem.y ${⊢}{\phi }\to {Y}\in {V}$
11 mapdpglem1.p
12 mapdpglem2.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
13 mapdpglem3.f ${⊢}{F}={\mathrm{Base}}_{{C}}$
14 mapdpglem3.te
15 1 7 8 lcdlmod ${⊢}{\phi }\to {C}\in \mathrm{LMod}$
16 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
17 eqid ${⊢}\mathrm{LSubSp}\left({C}\right)=\mathrm{LSubSp}\left({C}\right)$
18 1 3 8 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
19 4 16 6 lspsncl ${⊢}\left({U}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
20 18 9 19 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
21 1 2 3 16 7 17 8 20 mapdcl2 ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)\in \mathrm{LSubSp}\left({C}\right)$
22 4 16 6 lspsncl ${⊢}\left({U}\in \mathrm{LMod}\wedge {Y}\in {V}\right)\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
23 18 10 22 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
24 1 2 3 16 7 17 8 23 mapdcl2 ${⊢}{\phi }\to {M}\left({N}\left(\left\{{Y}\right\}\right)\right)\in \mathrm{LSubSp}\left({C}\right)$
25 17 11 lsmcl
26 15 21 24 25 syl3anc
27 13 17 lssel
28 26 14 27 syl2anc ${⊢}{\phi }\to {t}\in {F}$