# Metamath Proof Explorer

## Theorem hdmap1eq2

Description: Convert mapdheq2 to use HDMap1 function. (Contributed by NM, 16-May-2015)

Ref Expression
Hypotheses hdmap1eq2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmap1eq2.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmap1eq2.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmap1eq2.o
hdmap1eq2.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
hdmap1eq2.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
hdmap1eq2.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
hdmap1eq2.l ${⊢}{L}=\mathrm{LSpan}\left({C}\right)$
hdmap1eq2.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
hdmap1eq2.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
hdmap1eq2.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hdmap1eq2.f ${⊢}{\phi }\to {F}\in {D}$
hdmap1eq2.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={L}\left(\left\{{F}\right\}\right)$
hdmap1eq2.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
hdmap1eq2.x
hdmap1eq2.y
hdmap1eq2.e ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Y}⟩\right)={G}$
Assertion hdmap1eq2 ${⊢}{\phi }\to {I}\left(⟨{Y},{G},{X}⟩\right)={F}$

### Proof

Step Hyp Ref Expression
1 hdmap1eq2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmap1eq2.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hdmap1eq2.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 hdmap1eq2.o
5 hdmap1eq2.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
6 hdmap1eq2.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
7 hdmap1eq2.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
8 hdmap1eq2.l ${⊢}{L}=\mathrm{LSpan}\left({C}\right)$
9 hdmap1eq2.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
10 hdmap1eq2.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
11 hdmap1eq2.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
12 hdmap1eq2.f ${⊢}{\phi }\to {F}\in {D}$
13 hdmap1eq2.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={L}\left(\left\{{F}\right\}\right)$
14 hdmap1eq2.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
15 hdmap1eq2.x
16 hdmap1eq2.y
17 hdmap1eq2.e ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Y}⟩\right)={G}$
18 eqid ${⊢}{-}_{{U}}={-}_{{U}}$
19 eqid ${⊢}{-}_{{C}}={-}_{{C}}$
20 eqid ${⊢}{0}_{{C}}={0}_{{C}}$
21 16 eldifad ${⊢}{\phi }\to {Y}\in {V}$
22 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 21 hdmap1cl ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Y}⟩\right)\in {D}$
23 17 22 eqeltrrd ${⊢}{\phi }\to {G}\in {D}$
24 15 eldifad ${⊢}{\phi }\to {X}\in {V}$
25 eqid
26 1 2 3 18 4 5 6 7 19 20 8 9 10 11 16 23 24 25 hdmap1valc
27 1 2 3 18 4 5 6 7 19 20 8 9 10 11 15 12 21 25 hdmap1valc
28 27 17 eqtr3d
29 1 2 3 18 4 5 6 7 19 20 8 9 25 11 12 13 28 14 15 16 mapdh75e
30 26 29 eqtrd ${⊢}{\phi }\to {I}\left(⟨{Y},{G},{X}⟩\right)={F}$