Metamath Proof Explorer


Theorem hvmapfval

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

Ref Expression
Hypotheses hvmapval.h H = LHyp K
hvmapval.u U = DVecH K W
hvmapval.o O = ocH K W
hvmapval.v V = Base U
hvmapval.p + ˙ = + U
hvmapval.t · ˙ = U
hvmapval.z 0 ˙ = 0 U
hvmapval.s S = Scalar U
hvmapval.r R = Base S
hvmapval.m M = HVMap K W
hvmapval.k φ K A W H
Assertion hvmapfval φ M = x V 0 ˙ v V ι j R | t O x v = t + ˙ j · ˙ x

Proof

Step Hyp Ref Expression
1 hvmapval.h H = LHyp K
2 hvmapval.u U = DVecH K W
3 hvmapval.o O = ocH K W
4 hvmapval.v V = Base U
5 hvmapval.p + ˙ = + U
6 hvmapval.t · ˙ = U
7 hvmapval.z 0 ˙ = 0 U
8 hvmapval.s S = Scalar U
9 hvmapval.r R = Base S
10 hvmapval.m M = HVMap K W
11 hvmapval.k φ K A W H
12 1 hvmapffval K A 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
13 12 fveq1d K A HVMap K W = 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 W
14 10 13 syl5eq K A M = 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 W
15 fveq2 w = W DVecH K w = DVecH K W
16 15 2 syl6eqr w = W DVecH K w = U
17 16 fveq2d w = W Base DVecH K w = Base U
18 17 4 syl6eqr w = W Base DVecH K w = V
19 16 fveq2d w = W 0 DVecH K w = 0 U
20 19 7 syl6eqr w = W 0 DVecH K w = 0 ˙
21 20 sneqd w = W 0 DVecH K w = 0 ˙
22 18 21 difeq12d w = W Base DVecH K w 0 DVecH K w = V 0 ˙
23 16 fveq2d w = W Scalar DVecH K w = Scalar U
24 23 8 syl6eqr w = W Scalar DVecH K w = S
25 24 fveq2d w = W Base Scalar DVecH K w = Base S
26 25 9 syl6eqr w = W Base Scalar DVecH K w = R
27 fveq2 w = W ocH K w = ocH K W
28 27 3 syl6eqr w = W ocH K w = O
29 28 fveq1d w = W ocH K w x = O x
30 16 fveq2d w = W + DVecH K w = + U
31 30 5 syl6eqr w = W + DVecH K w = + ˙
32 eqidd w = W t = t
33 16 fveq2d w = W DVecH K w = U
34 33 6 syl6eqr w = W DVecH K w = · ˙
35 34 oveqd w = W j DVecH K w x = j · ˙ x
36 31 32 35 oveq123d w = W t + DVecH K w j DVecH K w x = t + ˙ j · ˙ x
37 36 eqeq2d w = W v = t + DVecH K w j DVecH K w x v = t + ˙ j · ˙ x
38 29 37 rexeqbidv w = W t ocH K w x v = t + DVecH K w j DVecH K w x t O x v = t + ˙ j · ˙ x
39 26 38 riotaeqbidv w = W ι j Base Scalar DVecH K w | t ocH K w x v = t + DVecH K w j DVecH K w x = ι j R | t O x v = t + ˙ j · ˙ x
40 18 39 mpteq12dv w = 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 = v V ι j R | t O x v = t + ˙ j · ˙ x
41 22 40 mpteq12dv w = W 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 V 0 ˙ v V ι j R | t O x v = t + ˙ j · ˙ x
42 eqid 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 = 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
43 4 fvexi V V
44 43 difexi V 0 ˙ V
45 44 mptex x V 0 ˙ v V ι j R | t O x v = t + ˙ j · ˙ x V
46 41 42 45 fvmpt W H 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 W = x V 0 ˙ v V ι j R | t O x v = t + ˙ j · ˙ x
47 14 46 sylan9eq K A W H M = x V 0 ˙ v V ι j R | t O x v = t + ˙ j · ˙ x
48 11 47 syl φ M = x V 0 ˙ v V ι j R | t O x v = t + ˙ j · ˙ x