# Metamath Proof Explorer

## Theorem hdmap1val

Description: Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval .) TODO: change I = ( x e. _V |-> ... to ( ph -> ( I<. X , F , Y > ) = ... in e.g. mapdh8 to shorten proofs with no \$d on x . (Contributed by NM, 15-May-2015)

Ref Expression
Hypotheses hdmap1val.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmap1fval.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmap1fval.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmap1fval.s
hdmap1fval.o
hdmap1fval.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
hdmap1fval.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
hdmap1fval.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
hdmap1fval.r ${⊢}{R}={-}_{{C}}$
hdmap1fval.q ${⊢}{Q}={0}_{{C}}$
hdmap1fval.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
hdmap1fval.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
hdmap1fval.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
hdmap1fval.k ${⊢}{\phi }\to \left({K}\in {A}\wedge {W}\in {H}\right)$
hdmap1val.x ${⊢}{\phi }\to {X}\in {V}$
hdmap1val.f ${⊢}{\phi }\to {F}\in {D}$
hdmap1val.y ${⊢}{\phi }\to {Y}\in {V}$
Assertion hdmap1val

### Proof

Step Hyp Ref Expression
1 hdmap1val.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmap1fval.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hdmap1fval.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 hdmap1fval.s
5 hdmap1fval.o
6 hdmap1fval.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
7 hdmap1fval.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
8 hdmap1fval.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
9 hdmap1fval.r ${⊢}{R}={-}_{{C}}$
10 hdmap1fval.q ${⊢}{Q}={0}_{{C}}$
11 hdmap1fval.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
12 hdmap1fval.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
13 hdmap1fval.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
14 hdmap1fval.k ${⊢}{\phi }\to \left({K}\in {A}\wedge {W}\in {H}\right)$
15 hdmap1val.x ${⊢}{\phi }\to {X}\in {V}$
16 hdmap1val.f ${⊢}{\phi }\to {F}\in {D}$
17 hdmap1val.y ${⊢}{\phi }\to {Y}\in {V}$
18 df-ot ${⊢}⟨{X},{F},{Y}⟩=⟨⟨{X},{F}⟩,{Y}⟩$
19 opelxp ${⊢}⟨{X},{F}⟩\in \left({V}×{D}\right)↔\left({X}\in {V}\wedge {F}\in {D}\right)$
20 15 16 19 sylanbrc ${⊢}{\phi }\to ⟨{X},{F}⟩\in \left({V}×{D}\right)$
21 opelxp ${⊢}⟨⟨{X},{F}⟩,{Y}⟩\in \left(\left({V}×{D}\right)×{V}\right)↔\left(⟨{X},{F}⟩\in \left({V}×{D}\right)\wedge {Y}\in {V}\right)$
22 20 17 21 sylanbrc ${⊢}{\phi }\to ⟨⟨{X},{F}⟩,{Y}⟩\in \left(\left({V}×{D}\right)×{V}\right)$
23 18 22 eqeltrid ${⊢}{\phi }\to ⟨{X},{F},{Y}⟩\in \left(\left({V}×{D}\right)×{V}\right)$
24 1 2 3 4 5 6 7 8 9 10 11 12 13 14 23 hdmap1vallem
25 ot3rdg ${⊢}{Y}\in {V}\to {2}^{nd}\left(⟨{X},{F},{Y}⟩\right)={Y}$
26 17 25 syl ${⊢}{\phi }\to {2}^{nd}\left(⟨{X},{F},{Y}⟩\right)={Y}$
27 26 eqeq1d
28 26 sneqd ${⊢}{\phi }\to \left\{{2}^{nd}\left(⟨{X},{F},{Y}⟩\right)\right\}=\left\{{Y}\right\}$
29 28 fveq2d ${⊢}{\phi }\to {N}\left(\left\{{2}^{nd}\left(⟨{X},{F},{Y}⟩\right)\right\}\right)={N}\left(\left\{{Y}\right\}\right)$
30 29 fveqeq2d ${⊢}{\phi }\to \left({M}\left({N}\left(\left\{{2}^{nd}\left(⟨{X},{F},{Y}⟩\right)\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)↔{M}\left({N}\left(\left\{{Y}\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)\right)$
31 ot1stg ${⊢}\left({X}\in {V}\wedge {F}\in {D}\wedge {Y}\in {V}\right)\to {1}^{st}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right)={X}$
32 15 16 17 31 syl3anc ${⊢}{\phi }\to {1}^{st}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right)={X}$
33 32 26 oveq12d
34 33 sneqd
35 34 fveq2d
36 35 fveq2d
37 ot2ndg ${⊢}\left({X}\in {V}\wedge {F}\in {D}\wedge {Y}\in {V}\right)\to {2}^{nd}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right)={F}$
38 15 16 17 37 syl3anc ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right)={F}$
39 38 oveq1d ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right){R}{h}={F}{R}{h}$
40 39 sneqd ${⊢}{\phi }\to \left\{{2}^{nd}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right){R}{h}\right\}=\left\{{F}{R}{h}\right\}$
41 40 fveq2d ${⊢}{\phi }\to {J}\left(\left\{{2}^{nd}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right){R}{h}\right\}\right)={J}\left(\left\{{F}{R}{h}\right\}\right)$
42 36 41 eqeq12d
43 30 42 anbi12d
44 43 riotabidv
45 27 44 ifbieq2d
46 24 45 eqtrd