# Metamath Proof Explorer

## Theorem hdmapeveclem

Description: Lemma for hdmapevec . TODO: combine with hdmapevec if it shortens overall. (Contributed by NM, 16-May-2015)

Ref Expression
Hypotheses hdmapevec.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmapevec.e ${⊢}{E}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩$
hdmapevec.j ${⊢}{J}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
hdmapevec.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
hdmapevec.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hdmapevec.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmapevec.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmapevec.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
hdmapevec.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
hdmapevec.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
hdmapevec.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
hdmapevec.x ${⊢}{\phi }\to {X}\in {V}$
hdmapevec.ne ${⊢}{\phi }\to ¬{X}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{E}\right\}\right)\right)$
Assertion hdmapeveclem ${⊢}{\phi }\to {S}\left({E}\right)={J}\left({E}\right)$

### Proof

Step Hyp Ref Expression
1 hdmapevec.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmapevec.e ${⊢}{E}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩$
3 hdmapevec.j ${⊢}{J}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
4 hdmapevec.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
5 hdmapevec.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
6 hdmapevec.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
7 hdmapevec.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
8 hdmapevec.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
9 hdmapevec.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
10 hdmapevec.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
11 hdmapevec.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
12 hdmapevec.x ${⊢}{\phi }\to {X}\in {V}$
13 hdmapevec.ne ${⊢}{\phi }\to ¬{X}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{E}\right\}\right)\right)$
14 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
15 eqid ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
16 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
17 1 14 15 6 7 16 2 5 dvheveccl ${⊢}{\phi }\to {E}\in \left({V}\setminus \left\{{0}_{{U}}\right\}\right)$
18 17 eldifad ${⊢}{\phi }\to {E}\in {V}$
19 1 2 6 7 8 9 10 3 11 4 5 18 12 13 hdmapval2 ${⊢}{\phi }\to {S}\left({E}\right)={I}\left(⟨{X},{I}\left(⟨{E},{J}\left({E}\right),{X}⟩\right),{E}⟩\right)$
20 eqid ${⊢}\mathrm{LSpan}\left({C}\right)=\mathrm{LSpan}\left({C}\right)$
21 eqid ${⊢}\mathrm{mapd}\left({K}\right)\left({W}\right)=\mathrm{mapd}\left({K}\right)\left({W}\right)$
22 eqid ${⊢}{0}_{{C}}={0}_{{C}}$
23 1 6 7 16 9 10 22 3 5 17 hvmapcl2 ${⊢}{\phi }\to {J}\left({E}\right)\in \left({D}\setminus \left\{{0}_{{C}}\right\}\right)$
24 23 eldifad ${⊢}{\phi }\to {J}\left({E}\right)\in {D}$
25 1 6 7 16 8 9 20 21 3 5 17 mapdhvmap ${⊢}{\phi }\to \mathrm{mapd}\left({K}\right)\left({W}\right)\left({N}\left(\left\{{E}\right\}\right)\right)=\mathrm{LSpan}\left({C}\right)\left(\left\{{J}\left({E}\right)\right\}\right)$
26 1 6 5 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
27 7 8 26 12 13 18 hdmaplem1 ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{E}\right\}\right)$
28 27 necomd ${⊢}{\phi }\to {N}\left(\left\{{E}\right\}\right)\ne {N}\left(\left\{{X}\right\}\right)$
29 7 8 26 12 13 18 16 hdmaplem3 ${⊢}{\phi }\to {X}\in \left({V}\setminus \left\{{0}_{{U}}\right\}\right)$
30 eqidd ${⊢}{\phi }\to {I}\left(⟨{E},{J}\left({E}\right),{X}⟩\right)={I}\left(⟨{E},{J}\left({E}\right),{X}⟩\right)$
31 1 6 7 16 8 9 10 20 21 11 5 24 25 28 17 29 30 hdmap1eq2 ${⊢}{\phi }\to {I}\left(⟨{X},{I}\left(⟨{E},{J}\left({E}\right),{X}⟩\right),{E}⟩\right)={J}\left({E}\right)$
32 19 31 eqtrd ${⊢}{\phi }\to {S}\left({E}\right)={J}\left({E}\right)$