# Metamath Proof Explorer

## Theorem hdmapval2

Description: Value of map from vectors to functionals with a specific auxiliary vector. TODO: Would shorter proofs result if the .ne hypothesis were changed to two =/= hypothesis? Consider hdmaplem1 through hdmaplem4 , which would become obsolete. (Contributed by NM, 15-May-2015)

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

### Proof

Step Hyp Ref Expression
1 hdmapval2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmapval2.e ${⊢}{E}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩$
3 hdmapval2.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 hdmapval2.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 hdmapval2.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
6 hdmapval2.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
7 hdmapval2.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
8 hdmapval2.j ${⊢}{J}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
9 hdmapval2.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
10 hdmapval2.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
11 hdmapval2.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
12 hdmapval2.t ${⊢}{\phi }\to {T}\in {V}$
13 hdmapval2.x ${⊢}{\phi }\to {X}\in {V}$
14 hdmapval2.ne ${⊢}{\phi }\to ¬{X}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)$
15 eqidd ${⊢}{\phi }\to {S}\left({T}\right)={S}\left({T}\right)$
16 1 3 4 6 7 10 11 12 hdmapcl ${⊢}{\phi }\to {S}\left({T}\right)\in {D}$
17 1 2 3 4 5 6 7 8 9 10 11 12 16 hdmapval2lem ${⊢}{\phi }\to \left({S}\left({T}\right)={S}\left({T}\right)↔\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to {S}\left({T}\right)={I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{T}⟩\right)\right)\right)$
18 15 17 mpbid ${⊢}{\phi }\to \forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to {S}\left({T}\right)={I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{T}⟩\right)\right)$
19 eleq1 ${⊢}{z}={X}\to \left({z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)↔{X}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\right)$
20 19 notbid ${⊢}{z}={X}\to \left(¬{z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)↔¬{X}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\right)$
21 oteq1 ${⊢}{z}={X}\to ⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{T}⟩=⟨{X},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{T}⟩$
22 oteq3 ${⊢}{z}={X}\to ⟨{E},{J}\left({E}\right),{z}⟩=⟨{E},{J}\left({E}\right),{X}⟩$
23 22 fveq2d ${⊢}{z}={X}\to {I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right)={I}\left(⟨{E},{J}\left({E}\right),{X}⟩\right)$
24 23 oteq2d ${⊢}{z}={X}\to ⟨{X},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{T}⟩=⟨{X},{I}\left(⟨{E},{J}\left({E}\right),{X}⟩\right),{T}⟩$
25 21 24 eqtrd ${⊢}{z}={X}\to ⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{T}⟩=⟨{X},{I}\left(⟨{E},{J}\left({E}\right),{X}⟩\right),{T}⟩$
26 25 fveq2d ${⊢}{z}={X}\to {I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{T}⟩\right)={I}\left(⟨{X},{I}\left(⟨{E},{J}\left({E}\right),{X}⟩\right),{T}⟩\right)$
27 26 eqeq2d ${⊢}{z}={X}\to \left({S}\left({T}\right)={I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{T}⟩\right)↔{S}\left({T}\right)={I}\left(⟨{X},{I}\left(⟨{E},{J}\left({E}\right),{X}⟩\right),{T}⟩\right)\right)$
28 20 27 imbi12d ${⊢}{z}={X}\to \left(\left(¬{z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to {S}\left({T}\right)={I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{T}⟩\right)\right)↔\left(¬{X}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to {S}\left({T}\right)={I}\left(⟨{X},{I}\left(⟨{E},{J}\left({E}\right),{X}⟩\right),{T}⟩\right)\right)\right)$
29 28 rspccv ${⊢}\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to {S}\left({T}\right)={I}\left(⟨{z},{I}\left(⟨{E},{J}\left({E}\right),{z}⟩\right),{T}⟩\right)\right)\to \left({X}\in {V}\to \left(¬{X}\in \left({N}\left(\left\{{E}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to {S}\left({T}\right)={I}\left(⟨{X},{I}\left(⟨{E},{J}\left({E}\right),{X}⟩\right),{T}⟩\right)\right)\right)$
30 18 13 14 29 syl3c ${⊢}{\phi }\to {S}\left({T}\right)={I}\left(⟨{X},{I}\left(⟨{E},{J}\left({E}\right),{X}⟩\right),{T}⟩\right)$