Metamath Proof Explorer


Theorem hvmapffval

Description: Map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015)

Ref Expression
Hypothesis hvmapval.h H = LHyp K
Assertion hvmapffval K X HVMap K = w H x Base DVecH K w 0 DVecH K w v Base DVecH K w ι j Base Scalar DVecH K w | t ocH K w x v = t + DVecH K w j DVecH K w x

Proof

Step Hyp Ref Expression
1 hvmapval.h H = LHyp K
2 elex K X K V
3 fveq2 k = K LHyp k = LHyp K
4 3 1 eqtr4di k = K LHyp k = H
5 fveq2 k = K DVecH k = DVecH K
6 5 fveq1d k = K DVecH k w = DVecH K w
7 6 fveq2d k = K Base DVecH k w = Base DVecH K w
8 6 fveq2d k = K 0 DVecH k w = 0 DVecH K w
9 8 sneqd k = K 0 DVecH k w = 0 DVecH K w
10 7 9 difeq12d k = K Base DVecH k w 0 DVecH k w = Base DVecH K w 0 DVecH K w
11 6 fveq2d k = K Scalar DVecH k w = Scalar DVecH K w
12 11 fveq2d k = K Base Scalar DVecH k w = Base Scalar DVecH K w
13 fveq2 k = K ocH k = ocH K
14 13 fveq1d k = K ocH k w = ocH K w
15 14 fveq1d k = K ocH k w x = ocH K w x
16 6 fveq2d k = K + DVecH k w = + DVecH K w
17 eqidd k = K t = t
18 6 fveq2d k = K DVecH k w = DVecH K w
19 18 oveqd k = K j DVecH k w x = j DVecH K w x
20 16 17 19 oveq123d k = K t + DVecH k w j DVecH k w x = t + DVecH K w j DVecH K w x
21 20 eqeq2d k = K v = t + DVecH k w j DVecH k w x v = t + DVecH K w j DVecH K w x
22 15 21 rexeqbidv k = K t ocH k w x v = t + DVecH k w j DVecH k w x t ocH K w x v = t + DVecH K w j DVecH K w x
23 12 22 riotaeqbidv k = K ι j Base Scalar DVecH k w | t ocH k w x v = t + DVecH k w j DVecH k w x = ι j Base Scalar DVecH K w | t ocH K w x v = t + DVecH K w j DVecH K w x
24 7 23 mpteq12dv k = K v Base DVecH k w ι j Base Scalar DVecH k w | t ocH k w x v = t + DVecH k w j DVecH k w x = v Base DVecH K w ι j Base Scalar DVecH K w | t ocH K w x v = t + DVecH K w j DVecH K w x
25 10 24 mpteq12dv k = K x Base DVecH k w 0 DVecH k w v Base DVecH k w ι j Base Scalar DVecH k w | t ocH k w x v = t + DVecH k w j DVecH k w x = x Base DVecH K w 0 DVecH K w v Base DVecH K w ι j Base Scalar DVecH K w | t ocH K w x v = t + DVecH K w j DVecH K w x
26 4 25 mpteq12dv k = K w LHyp k x Base DVecH k w 0 DVecH k w v Base DVecH k w ι j Base Scalar DVecH k w | t ocH k w x v = t + DVecH k w j DVecH k w x = w H x Base DVecH K w 0 DVecH K w v Base DVecH K w ι j Base Scalar DVecH K w | t ocH K w x v = t + DVecH K w j DVecH K w x
27 df-hvmap HVMap = k V w LHyp k x Base DVecH k w 0 DVecH k w v Base DVecH k w ι j Base Scalar DVecH k w | t ocH k w x v = t + DVecH k w j DVecH k w x
28 26 27 1 mptfvmpt K V HVMap K = w H x Base DVecH K w 0 DVecH K w v Base DVecH K w ι j Base Scalar DVecH K w | t ocH K w x v = t + DVecH K w j DVecH K w x
29 2 28 syl K X HVMap K = w H x Base DVecH K w 0 DVecH K w v Base DVecH K w ι j Base Scalar DVecH K w | t ocH K w x v = t + DVecH K w j DVecH K w x