# Metamath Proof Explorer

## Theorem mapdpglem5N

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)$
mapdpglem4.jt
Assertion mapdpglem5N ${⊢}{\phi }\to {t}\ne {0}_{{C}}$

### 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 mapdpglem4.jt
24 eqid ${⊢}\mathrm{LSAtoms}\left({U}\right)=\mathrm{LSAtoms}\left({U}\right)$
25 eqid ${⊢}\mathrm{LSAtoms}\left({C}\right)=\mathrm{LSAtoms}\left({C}\right)$
26 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 mapdpglem4N
27 1 3 8 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
28 4 5 lmodvsubcl
29 27 9 10 28 syl3anc
30 4 6 21 24 27 29 lsatspn0
31 26 30 mpbird
32 1 2 3 24 7 25 8 31 mapdat
33 23 32 eqeltrrd ${⊢}{\phi }\to {J}\left(\left\{{t}\right\}\right)\in \mathrm{LSAtoms}\left({C}\right)$
34 eqid ${⊢}{0}_{{C}}={0}_{{C}}$
35 1 7 8 lcdlmod ${⊢}{\phi }\to {C}\in \mathrm{LMod}$
36 1 2 3 4 5 6 7 8 9 10 11 12 13 14 mapdpglem2a ${⊢}{\phi }\to {t}\in {F}$
37 13 12 34 25 35 36 lsatspn0 ${⊢}{\phi }\to \left({J}\left(\left\{{t}\right\}\right)\in \mathrm{LSAtoms}\left({C}\right)↔{t}\ne {0}_{{C}}\right)$
38 33 37 mpbid ${⊢}{\phi }\to {t}\ne {0}_{{C}}$