# Metamath Proof Explorer

## Theorem mapdhvmap

Description: Relationship between mapd and HVMap , which can be used to satisfy the last hypothesis of mapdpg . Equation 10 of Baer p. 48. (Contributed by NM, 29-Mar-2015)

Ref Expression
Hypotheses mapdhvmap.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
mapdhvmap.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
mapdhvmap.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
mapdhvmap.z
mapdhvmap.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
mapdhvmap.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
mapdhvmap.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
mapdhvmap.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
mapdhvmap.p ${⊢}{P}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
mapdhvmap.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
mapdhvmap.x
Assertion mapdhvmap ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{P}\left({X}\right)\right\}\right)$

### Proof

Step Hyp Ref Expression
1 mapdhvmap.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 mapdhvmap.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 mapdhvmap.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 mapdhvmap.z
5 mapdhvmap.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
6 mapdhvmap.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
7 mapdhvmap.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
8 mapdhvmap.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
9 mapdhvmap.p ${⊢}{P}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
10 mapdhvmap.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
11 mapdhvmap.x
12 eqid ${⊢}\mathrm{ocH}\left({K}\right)\left({W}\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)$
13 eqid ${⊢}\mathrm{LFnl}\left({U}\right)=\mathrm{LFnl}\left({U}\right)$
14 eqid ${⊢}\mathrm{LKer}\left({U}\right)=\mathrm{LKer}\left({U}\right)$
15 eqid ${⊢}\mathrm{LDual}\left({U}\right)=\mathrm{LDual}\left({U}\right)$
16 eqid ${⊢}\mathrm{LSpan}\left(\mathrm{LDual}\left({U}\right)\right)=\mathrm{LSpan}\left(\mathrm{LDual}\left({U}\right)\right)$
17 11 eldifad ${⊢}{\phi }\to {X}\in {V}$
18 1 2 3 4 13 9 10 11 hvmaplfl ${⊢}{\phi }\to {P}\left({X}\right)\in \mathrm{LFnl}\left({U}\right)$
19 1 12 2 3 4 14 9 10 11 hvmaplkr ${⊢}{\phi }\to \mathrm{LKer}\left({U}\right)\left({P}\left({X}\right)\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\left\{{X}\right\}\right)$
20 1 12 8 2 3 5 13 14 15 16 10 17 18 19 mapdsn3 ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)=\mathrm{LSpan}\left(\mathrm{LDual}\left({U}\right)\right)\left(\left\{{P}\left({X}\right)\right\}\right)$
21 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
22 eqid ${⊢}{0}_{{C}}={0}_{{C}}$
23 1 2 3 4 6 21 22 9 10 11 hvmapcl2 ${⊢}{\phi }\to {P}\left({X}\right)\in \left({\mathrm{Base}}_{{C}}\setminus \left\{{0}_{{C}}\right\}\right)$
24 23 eldifad ${⊢}{\phi }\to {P}\left({X}\right)\in {\mathrm{Base}}_{{C}}$
25 24 snssd ${⊢}{\phi }\to \left\{{P}\left({X}\right)\right\}\subseteq {\mathrm{Base}}_{{C}}$
26 1 2 15 16 6 21 7 10 25 lcdlsp ${⊢}{\phi }\to {J}\left(\left\{{P}\left({X}\right)\right\}\right)=\mathrm{LSpan}\left(\mathrm{LDual}\left({U}\right)\right)\left(\left\{{P}\left({X}\right)\right\}\right)$
27 20 26 eqtr4d ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{P}\left({X}\right)\right\}\right)$