# Metamath Proof Explorer

## Theorem mapdh8a

Description: Part of Part (8) in Baer p. 48. (Contributed by NM, 5-May-2015)

Ref Expression
Hypotheses mapdh8a.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
mapdh8a.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
mapdh8a.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
mapdh8a.s
mapdh8a.o
mapdh8a.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
mapdh8a.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
mapdh8a.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
mapdh8a.r ${⊢}{R}={-}_{{C}}$
mapdh8a.q ${⊢}{Q}={0}_{{C}}$
mapdh8a.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
mapdh8a.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
mapdh8a.i
mapdh8a.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
mapdh8a.f ${⊢}{\phi }\to {F}\in {D}$
mapdh8a.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{F}\right\}\right)$
mapdh8a.a ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Y}⟩\right)={G}$
mapdh8a.x
mapdh8a.y
mapdh8a.yz ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{T}\right\}\right)$
mapdh8a.xt
mapdh8a.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{T}\right\}\right)$
Assertion mapdh8a ${⊢}{\phi }\to {I}\left(⟨{Y},{G},{T}⟩\right)={I}\left(⟨{X},{F},{T}⟩\right)$

### Proof

Step Hyp Ref Expression
1 mapdh8a.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 mapdh8a.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 mapdh8a.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 mapdh8a.s
5 mapdh8a.o
6 mapdh8a.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
7 mapdh8a.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
8 mapdh8a.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
9 mapdh8a.r ${⊢}{R}={-}_{{C}}$
10 mapdh8a.q ${⊢}{Q}={0}_{{C}}$
11 mapdh8a.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
12 mapdh8a.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
13 mapdh8a.i
14 mapdh8a.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
15 mapdh8a.f ${⊢}{\phi }\to {F}\in {D}$
16 mapdh8a.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{F}\right\}\right)$
17 mapdh8a.a ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Y}⟩\right)={G}$
18 mapdh8a.x
19 mapdh8a.y
20 mapdh8a.yz ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{T}\right\}\right)$
21 mapdh8a.xt
22 mapdh8a.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{T}\right\}\right)$
23 eqidd ${⊢}{\phi }\to {I}\left(⟨{X},{F},{T}⟩\right)={I}\left(⟨{X},{F},{T}⟩\right)$
24 10 13 1 12 2 3 4 5 6 7 8 9 11 14 15 16 18 19 21 22 20 17 23 mapdheq4 ${⊢}{\phi }\to {I}\left(⟨{Y},{G},{T}⟩\right)={I}\left(⟨{X},{F},{T}⟩\right)$