# Metamath Proof Explorer

## Theorem hdmap1vallem

Description: Value of preliminary map from vectors to functionals in the closed kernel dual space. (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.t ${⊢}{\phi }\to {T}\in \left(\left({V}×{D}\right)×{V}\right)$
Assertion hdmap1vallem

### 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.t ${⊢}{\phi }\to {T}\in \left(\left({V}×{D}\right)×{V}\right)$
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 hdmap1fval
17 16 fveq1d
18 10 fvexi ${⊢}{Q}\in \mathrm{V}$
19 riotaex
20 18 19 ifex
21 fveqeq2
22 fveq2 ${⊢}{x}={T}\to {2}^{nd}\left({x}\right)={2}^{nd}\left({T}\right)$
23 22 sneqd ${⊢}{x}={T}\to \left\{{2}^{nd}\left({x}\right)\right\}=\left\{{2}^{nd}\left({T}\right)\right\}$
24 23 fveq2d ${⊢}{x}={T}\to {N}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)={N}\left(\left\{{2}^{nd}\left({T}\right)\right\}\right)$
25 24 fveqeq2d ${⊢}{x}={T}\to \left({M}\left({N}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)↔{M}\left({N}\left(\left\{{2}^{nd}\left({T}\right)\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)\right)$
26 2fveq3 ${⊢}{x}={T}\to {1}^{st}\left({1}^{st}\left({x}\right)\right)={1}^{st}\left({1}^{st}\left({T}\right)\right)$
27 26 22 oveq12d
28 27 sneqd
29 28 fveq2d
30 29 fveq2d
31 2fveq3 ${⊢}{x}={T}\to {2}^{nd}\left({1}^{st}\left({x}\right)\right)={2}^{nd}\left({1}^{st}\left({T}\right)\right)$
32 31 oveq1d ${⊢}{x}={T}\to {2}^{nd}\left({1}^{st}\left({x}\right)\right){R}{h}={2}^{nd}\left({1}^{st}\left({T}\right)\right){R}{h}$
33 32 sneqd ${⊢}{x}={T}\to \left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){R}{h}\right\}=\left\{{2}^{nd}\left({1}^{st}\left({T}\right)\right){R}{h}\right\}$
34 33 fveq2d ${⊢}{x}={T}\to {J}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){R}{h}\right\}\right)={J}\left(\left\{{2}^{nd}\left({1}^{st}\left({T}\right)\right){R}{h}\right\}\right)$
35 30 34 eqeq12d
36 25 35 anbi12d
37 36 riotabidv
38 21 37 ifbieq2d
39 eqid
40 38 39 fvmptg
41 15 20 40 sylancl
42 17 41 eqtrd