Metamath Proof Explorer

Definition df-hdmap

Description: Define map from vectors to functionals in the closed kernel dual space. See hdmapfval description for more details. (Contributed by NM, 15-May-2015)

Ref Expression
Assertion df-hdmap 
|- HDMap = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. <. ( _I |` ( Base ` k ) ) , ( _I |` ( ( LTrn ` k ) ` w ) ) >. / e ]. [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` k ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` k ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chdma 
 |-  HDMap
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vw 
 |-  w
4 clh 
 |-  LHyp
5 1 cv 
 |-  k
6 5 4 cfv 
 |-  ( LHyp ` k )
7 va 
 |-  a
8 cid 
 |-  _I
9 cbs 
 |-  Base
10 5 9 cfv 
 |-  ( Base ` k )
11 8 10 cres 
 |-  ( _I |` ( Base ` k ) )
12 cltrn 
 |-  LTrn
13 5 12 cfv 
 |-  ( LTrn ` k )
14 3 cv 
 |-  w
15 14 13 cfv 
 |-  ( ( LTrn ` k ) ` w )
16 8 15 cres 
 |-  ( _I |` ( ( LTrn ` k ) ` w ) )
17 11 16 cop 
 |-  <. ( _I |` ( Base ` k ) ) , ( _I |` ( ( LTrn ` k ) ` w ) ) >.
18 ve 
 |-  e
19 cdvh 
 |-  DVecH
20 5 19 cfv 
 |-  ( DVecH ` k )
21 14 20 cfv 
 |-  ( ( DVecH ` k ) ` w )
22 vu 
 |-  u
23 22 cv 
 |-  u
24 23 9 cfv 
 |-  ( Base ` u )
25 vv 
 |-  v
26 chdma1 
 |-  HDMap1
27 5 26 cfv 
 |-  ( HDMap1 ` k )
28 14 27 cfv 
 |-  ( ( HDMap1 ` k ) ` w )
29 vi 
 |-  i
30 7 cv 
 |-  a
31 vt 
 |-  t
32 25 cv 
 |-  v
33 vy 
 |-  y
34 clcd 
 |-  LCDual
35 5 34 cfv 
 |-  ( LCDual ` k )
36 14 35 cfv 
 |-  ( ( LCDual ` k ) ` w )
37 36 9 cfv 
 |-  ( Base ` ( ( LCDual ` k ) ` w ) )
38 vz 
 |-  z
39 38 cv 
 |-  z
40 clspn 
 |-  LSpan
41 23 40 cfv 
 |-  ( LSpan ` u )
42 18 cv 
 |-  e
43 42 csn 
 |-  { e }
44 43 41 cfv 
 |-  ( ( LSpan ` u ) ` { e } )
45 31 cv 
 |-  t
46 45 csn 
 |-  { t }
47 46 41 cfv 
 |-  ( ( LSpan ` u ) ` { t } )
48 44 47 cun 
 |-  ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) )
49 39 48 wcel 
 |-  z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) )
50 49 wn 
 |-  -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) )
51 33 cv 
 |-  y
52 29 cv 
 |-  i
53 chvm 
 |-  HVMap
54 5 53 cfv 
 |-  ( HVMap ` k )
55 14 54 cfv 
 |-  ( ( HVMap ` k ) ` w )
56 42 55 cfv 
 |-  ( ( ( HVMap ` k ) ` w ) ` e )
57 42 56 39 cotp 
 |-  <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >.
58 57 52 cfv 
 |-  ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. )
59 39 58 45 cotp 
 |-  <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >.
60 59 52 cfv 
 |-  ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. )
61 51 60 wceq 
 |-  y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. )
62 50 61 wi 
 |-  ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) )
63 62 38 32 wral 
 |-  A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) )
64 63 33 37 crio 
 |-  ( iota_ y e. ( Base ` ( ( LCDual ` k ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) ) )
65 31 32 64 cmpt 
 |-  ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` k ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) ) ) )
66 30 65 wcel 
 |-  a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` k ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) ) ) )
67 66 29 28 wsbc 
 |-  [. ( ( HDMap1 ` k ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` k ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) ) ) )
68 67 25 24 wsbc 
 |-  [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` k ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` k ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) ) ) )
69 68 22 21 wsbc 
 |-  [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` k ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` k ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) ) ) )
70 69 18 17 wsbc 
 |-  [. <. ( _I |` ( Base ` k ) ) , ( _I |` ( ( LTrn ` k ) ` w ) ) >. / e ]. [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` k ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` k ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) ) ) )
71 70 7 cab 
 |-  { a | [. <. ( _I |` ( Base ` k ) ) , ( _I |` ( ( LTrn ` k ) ` w ) ) >. / e ]. [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` k ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` k ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) }
72 3 6 71 cmpt 
 |-  ( w e. ( LHyp ` k ) |-> { a | [. <. ( _I |` ( Base ` k ) ) , ( _I |` ( ( LTrn ` k ) ` w ) ) >. / e ]. [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` k ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` k ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) } )
73 1 2 72 cmpt 
 |-  ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. <. ( _I |` ( Base ` k ) ) , ( _I |` ( ( LTrn ` k ) ` w ) ) >. / e ]. [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` k ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` k ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) } ) )
74 0 73 wceq 
 |-  HDMap = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. <. ( _I |` ( Base ` k ) ) , ( _I |` ( ( LTrn ` k ) ` w ) ) >. / e ]. [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` k ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` k ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) } ) )