# Metamath Proof Explorer

## Theorem mapdpglem4N

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

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
mapdpglem3.a ${⊢}{A}=\mathrm{Scalar}\left({U}\right)$
mapdpglem3.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
mapdpglem3.t
mapdpglem3.r ${⊢}{R}={-}_{{C}}$
mapdpglem3.g ${⊢}{\phi }\to {G}\in {F}$
mapdpglem3.e ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{G}\right\}\right)$
mapdpglem4.q ${⊢}{Q}={0}_{{U}}$
mapdpglem.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
Assertion mapdpglem4N

### 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 mapdpglem3.a ${⊢}{A}=\mathrm{Scalar}\left({U}\right)$
16 mapdpglem3.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
17 mapdpglem3.t
18 mapdpglem3.r ${⊢}{R}={-}_{{C}}$
19 mapdpglem3.g ${⊢}{\phi }\to {G}\in {F}$
20 mapdpglem3.e ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{G}\right\}\right)$
21 mapdpglem4.q ${⊢}{Q}={0}_{{U}}$
22 mapdpglem.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
23 1 3 8 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
24 4 21 5 23 9 10 22 lspsnsubn0