Metamath Proof Explorer

Definition df-hdmap1

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

Ref Expression
Assertion df-hdmap1 
|- HDMap1 = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chdma1 
 |-  HDMap1
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 cdvh 
 |-  DVecH
9 5 8 cfv 
 |-  ( DVecH ` k )
10 3 cv 
 |-  w
11 10 9 cfv 
 |-  ( ( DVecH ` k ) ` w )
12 vu 
 |-  u
13 cbs 
 |-  Base
14 12 cv 
 |-  u
15 14 13 cfv 
 |-  ( Base ` u )
16 vv 
 |-  v
17 clspn 
 |-  LSpan
18 14 17 cfv 
 |-  ( LSpan ` u )
19 vn 
 |-  n
20 clcd 
 |-  LCDual
21 5 20 cfv 
 |-  ( LCDual ` k )
22 10 21 cfv 
 |-  ( ( LCDual ` k ) ` w )
23 vc 
 |-  c
24 23 cv 
 |-  c
25 24 13 cfv 
 |-  ( Base ` c )
26 vd 
 |-  d
27 24 17 cfv 
 |-  ( LSpan ` c )
28 vj 
 |-  j
29 cmpd 
 |-  mapd
30 5 29 cfv 
 |-  ( mapd ` k )
31 10 30 cfv 
 |-  ( ( mapd ` k ) ` w )
32 vm 
 |-  m
33 7 cv 
 |-  a
34 vx 
 |-  x
35 16 cv 
 |-  v
36 26 cv 
 |-  d
37 35 36 cxp 
 |-  ( v X. d )
38 37 35 cxp 
 |-  ( ( v X. d ) X. v )
39 c2nd 
 |-  2nd
40 34 cv 
 |-  x
41 40 39 cfv 
 |-  ( 2nd ` x )
42 c0g 
 |-  0g
43 14 42 cfv 
 |-  ( 0g ` u )
44 41 43 wceq 
 |-  ( 2nd ` x ) = ( 0g ` u )
45 24 42 cfv 
 |-  ( 0g ` c )
46 vh 
 |-  h
47 32 cv 
 |-  m
48 19 cv 
 |-  n
49 41 csn 
 |-  { ( 2nd ` x ) }
50 49 48 cfv 
 |-  ( n ` { ( 2nd ` x ) } )
51 50 47 cfv 
 |-  ( m ` ( n ` { ( 2nd ` x ) } ) )
52 28 cv 
 |-  j
53 46 cv 
 |-  h
54 53 csn 
 |-  { h }
55 54 52 cfv 
 |-  ( j ` { h } )
56 51 55 wceq 
 |-  ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } )
57 c1st 
 |-  1st
58 40 57 cfv 
 |-  ( 1st ` x )
59 58 57 cfv 
 |-  ( 1st ` ( 1st ` x ) )
60 csg 
 |-  -g
61 14 60 cfv 
 |-  ( -g ` u )
62 59 41 61 co 
 |-  ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) )
63 62 csn 
 |-  { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) }
64 63 48 cfv 
 |-  ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } )
65 64 47 cfv 
 |-  ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) )
66 58 39 cfv 
 |-  ( 2nd ` ( 1st ` x ) )
67 24 60 cfv 
 |-  ( -g ` c )
68 66 53 67 co 
 |-  ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h )
69 68 csn 
 |-  { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) }
70 69 52 cfv 
 |-  ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } )
71 65 70 wceq 
 |-  ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } )
72 56 71 wa 
 |-  ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) )
73 72 46 36 crio 
 |-  ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) )
74 44 45 73 cif 
 |-  if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) )
75 34 38 74 cmpt 
 |-  ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) )
76 33 75 wcel 
 |-  a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) )
77 76 32 31 wsbc 
 |-  [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) )
78 77 28 27 wsbc 
 |-  [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) )
79 78 26 25 wsbc 
 |-  [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) )
80 79 23 22 wsbc 
 |-  [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) )
81 80 19 18 wsbc 
 |-  [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) )
82 81 16 15 wsbc 
 |-  [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) )
83 82 12 11 wsbc 
 |-  [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) )
84 83 7 cab 
 |-  { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) }
85 3 6 84 cmpt 
 |-  ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } )
86 1 2 85 cmpt 
 |-  ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) )
87 0 86 wceq 
 |-  HDMap1 = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) )