Metamath Proof Explorer


Theorem hdmapfval

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

Ref Expression
Hypotheses hdmapval.h H = LHyp K
hdmapfval.e E = I Base K I LTrn K W
hdmapfval.u U = DVecH K W
hdmapfval.v V = Base U
hdmapfval.n N = LSpan U
hdmapfval.c C = LCDual K W
hdmapfval.d D = Base C
hdmapfval.j J = HVMap K W
hdmapfval.i I = HDMap1 K W
hdmapfval.s S = HDMap K W
hdmapfval.k φ K A W H
Assertion hdmapfval φ S = t V ι y D | z V ¬ z N E N t y = I z I E J E z t

Proof

Step Hyp Ref Expression
1 hdmapval.h H = LHyp K
2 hdmapfval.e E = I Base K I LTrn K W
3 hdmapfval.u U = DVecH K W
4 hdmapfval.v V = Base U
5 hdmapfval.n N = LSpan U
6 hdmapfval.c C = LCDual K W
7 hdmapfval.d D = Base C
8 hdmapfval.j J = HVMap K W
9 hdmapfval.i I = HDMap1 K W
10 hdmapfval.s S = HDMap K W
11 hdmapfval.k φ K A W H
12 1 hdmapffval K A HDMap K = w H a | [˙ I Base K I LTrn K w / e]˙ [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ HDMap1 K w / i]˙ a t v ι y Base LCDual K w | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t
13 12 fveq1d K A HDMap K W = w H a | [˙ I Base K I LTrn K w / e]˙ [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ HDMap1 K w / i]˙ a t v ι y Base LCDual K w | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t W
14 10 13 syl5eq K A S = w H a | [˙ I Base K I LTrn K w / e]˙ [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ HDMap1 K w / i]˙ a t v ι y Base LCDual K w | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t W
15 fveq2 w = W LTrn K w = LTrn K W
16 15 reseq2d w = W I LTrn K w = I LTrn K W
17 16 opeq2d w = W I Base K I LTrn K w = I Base K I LTrn K W
18 fveq2 w = W DVecH K w = DVecH K W
19 fveq2 w = W HDMap1 K w = HDMap1 K W
20 2fveq3 w = W Base LCDual K w = Base LCDual K W
21 fveq2 w = W HVMap K w = HVMap K W
22 21 fveq1d w = W HVMap K w e = HVMap K W e
23 22 oteq2d w = W e HVMap K w e z = e HVMap K W e z
24 23 fveq2d w = W i e HVMap K w e z = i e HVMap K W e z
25 24 oteq2d w = W z i e HVMap K w e z t = z i e HVMap K W e z t
26 25 fveq2d w = W i z i e HVMap K w e z t = i z i e HVMap K W e z t
27 26 eqeq2d w = W y = i z i e HVMap K w e z t y = i z i e HVMap K W e z t
28 27 imbi2d w = W ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t
29 28 ralbidv w = W z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t
30 20 29 riotaeqbidv w = W ι y Base LCDual K w | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t = ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t
31 30 mpteq2dv w = W t v ι y Base LCDual K w | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t = t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t
32 31 eleq2d w = W a t v ι y Base LCDual K w | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t a t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t
33 19 32 sbceqbid w = W [˙ HDMap1 K w / i]˙ a t v ι y Base LCDual K w | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t [˙ HDMap1 K W / i]˙ a t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t
34 33 sbcbidv w = W [˙Base u / v]˙ [˙ HDMap1 K w / i]˙ a t v ι y Base LCDual K w | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t [˙Base u / v]˙ [˙ HDMap1 K W / i]˙ a t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t
35 18 34 sbceqbid w = W [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ HDMap1 K w / i]˙ a t v ι y Base LCDual K w | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t [˙ DVecH K W / u]˙ [˙Base u / v]˙ [˙ HDMap1 K W / i]˙ a t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t
36 17 35 sbceqbid w = W [˙ I Base K I LTrn K w / e]˙ [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ HDMap1 K w / i]˙ a t v ι y Base LCDual K w | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t [˙ I Base K I LTrn K W / e]˙ [˙ DVecH K W / u]˙ [˙Base u / v]˙ [˙ HDMap1 K W / i]˙ a t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t
37 opex I Base K I LTrn K W V
38 fvex DVecH K W V
39 fvex Base u V
40 simp1 e = I Base K I LTrn K W u = DVecH K W v = Base u e = I Base K I LTrn K W
41 40 2 syl6eqr e = I Base K I LTrn K W u = DVecH K W v = Base u e = E
42 simp2 e = I Base K I LTrn K W u = DVecH K W v = Base u u = DVecH K W
43 42 3 syl6eqr e = I Base K I LTrn K W u = DVecH K W v = Base u u = U
44 simp3 e = I Base K I LTrn K W u = DVecH K W v = Base u v = Base u
45 43 fveq2d e = I Base K I LTrn K W u = DVecH K W v = Base u Base u = Base U
46 44 45 eqtrd e = I Base K I LTrn K W u = DVecH K W v = Base u v = Base U
47 46 4 syl6eqr e = I Base K I LTrn K W u = DVecH K W v = Base u v = V
48 fvex HDMap1 K W V
49 id i = HDMap1 K W i = HDMap1 K W
50 49 9 syl6eqr i = HDMap1 K W i = I
51 fveq1 i = I i z i e HVMap K W e z t = I z i e HVMap K W e z t
52 fveq1 i = I i e HVMap K W e z = I e HVMap K W e z
53 52 oteq2d i = I z i e HVMap K W e z t = z I e HVMap K W e z t
54 53 fveq2d i = I I z i e HVMap K W e z t = I z I e HVMap K W e z t
55 51 54 eqtrd i = I i z i e HVMap K W e z t = I z I e HVMap K W e z t
56 55 eqeq2d i = I y = i z i e HVMap K W e z t y = I z I e HVMap K W e z t
57 56 imbi2d i = I ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t ¬ z LSpan u e LSpan u t y = I z I e HVMap K W e z t
58 57 ralbidv i = I z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t z v ¬ z LSpan u e LSpan u t y = I z I e HVMap K W e z t
59 58 riotabidv i = I ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t = ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = I z I e HVMap K W e z t
60 59 mpteq2dv i = I t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t = t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = I z I e HVMap K W e z t
61 60 eleq2d i = I a t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t a t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = I z I e HVMap K W e z t
62 50 61 syl i = HDMap1 K W a t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t a t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = I z I e HVMap K W e z t
63 48 62 sbcie [˙ HDMap1 K W / i]˙ a t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t a t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = I z I e HVMap K W e z t
64 simp3 e = E u = U v = V v = V
65 6 fveq2i Base C = Base LCDual K W
66 7 65 eqtr2i Base LCDual K W = D
67 66 a1i e = E u = U v = V Base LCDual K W = D
68 simp2 e = E u = U v = V u = U
69 68 fveq2d e = E u = U v = V LSpan u = LSpan U
70 69 5 syl6eqr e = E u = U v = V LSpan u = N
71 simp1 e = E u = U v = V e = E
72 71 sneqd e = E u = U v = V e = E
73 70 72 fveq12d e = E u = U v = V LSpan u e = N E
74 70 fveq1d e = E u = U v = V LSpan u t = N t
75 73 74 uneq12d e = E u = U v = V LSpan u e LSpan u t = N E N t
76 75 eleq2d e = E u = U v = V z LSpan u e LSpan u t z N E N t
77 76 notbid e = E u = U v = V ¬ z LSpan u e LSpan u t ¬ z N E N t
78 71 oteq1d e = E u = U v = V e HVMap K W e z = E HVMap K W e z
79 71 fveq2d e = E u = U v = V HVMap K W e = HVMap K W E
80 8 fveq1i J E = HVMap K W E
81 79 80 syl6eqr e = E u = U v = V HVMap K W e = J E
82 81 oteq2d e = E u = U v = V E HVMap K W e z = E J E z
83 78 82 eqtrd e = E u = U v = V e HVMap K W e z = E J E z
84 83 fveq2d e = E u = U v = V I e HVMap K W e z = I E J E z
85 84 oteq2d e = E u = U v = V z I e HVMap K W e z t = z I E J E z t
86 85 fveq2d e = E u = U v = V I z I e HVMap K W e z t = I z I E J E z t
87 86 eqeq2d e = E u = U v = V y = I z I e HVMap K W e z t y = I z I E J E z t
88 77 87 imbi12d e = E u = U v = V ¬ z LSpan u e LSpan u t y = I z I e HVMap K W e z t ¬ z N E N t y = I z I E J E z t
89 64 88 raleqbidv e = E u = U v = V z v ¬ z LSpan u e LSpan u t y = I z I e HVMap K W e z t z V ¬ z N E N t y = I z I E J E z t
90 67 89 riotaeqbidv e = E u = U v = V ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = I z I e HVMap K W e z t = ι y D | z V ¬ z N E N t y = I z I E J E z t
91 64 90 mpteq12dv e = E u = U v = V t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = I z I e HVMap K W e z t = t V ι y D | z V ¬ z N E N t y = I z I E J E z t
92 91 eleq2d e = E u = U v = V a t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = I z I e HVMap K W e z t a t V ι y D | z V ¬ z N E N t y = I z I E J E z t
93 63 92 syl5bb e = E u = U v = V [˙ HDMap1 K W / i]˙ a t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t a t V ι y D | z V ¬ z N E N t y = I z I E J E z t
94 41 43 47 93 syl3anc e = I Base K I LTrn K W u = DVecH K W v = Base u [˙ HDMap1 K W / i]˙ a t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t a t V ι y D | z V ¬ z N E N t y = I z I E J E z t
95 37 38 39 94 sbc3ie [˙ I Base K I LTrn K W / e]˙ [˙ DVecH K W / u]˙ [˙Base u / v]˙ [˙ HDMap1 K W / i]˙ a t v ι y Base LCDual K W | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K W e z t a t V ι y D | z V ¬ z N E N t y = I z I E J E z t
96 36 95 syl6bb w = W [˙ I Base K I LTrn K w / e]˙ [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ HDMap1 K w / i]˙ a t v ι y Base LCDual K w | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t a t V ι y D | z V ¬ z N E N t y = I z I E J E z t
97 96 abbi1dv w = W a | [˙ I Base K I LTrn K w / e]˙ [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ HDMap1 K w / i]˙ a t v ι y Base LCDual K w | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t = t V ι y D | z V ¬ z N E N t y = I z I E J E z t
98 eqid w H a | [˙ I Base K I LTrn K w / e]˙ [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ HDMap1 K w / i]˙ a t v ι y Base LCDual K w | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t = w H a | [˙ I Base K I LTrn K w / e]˙ [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ HDMap1 K w / i]˙ a t v ι y Base LCDual K w | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t
99 97 98 4 mptfvmpt W H w H a | [˙ I Base K I LTrn K w / e]˙ [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ HDMap1 K w / i]˙ a t v ι y Base LCDual K w | z v ¬ z LSpan u e LSpan u t y = i z i e HVMap K w e z t W = t V ι y D | z V ¬ z N E N t y = I z I E J E z t
100 14 99 sylan9eq K A W H S = t V ι y D | z V ¬ z N E N t y = I z I E J E z t
101 11 100 syl φ S = t V ι y D | z V ¬ z N E N t y = I z I E J E z t