Metamath Proof Explorer

Definition df-hvmap

Description: Extend class notation with a map from each nonzero vector x to a unique nonzero functional in the closed kernel dual space. (We could extend it to include the zero vector, but that is unnecessary for our purposes.) TODO: This pattern is used several times earlier, e.g., lcf1o , dochfl1 - should we update those to use this definition? (Contributed by NM, 23-Mar-2015)

Ref Expression
Assertion df-hvmap 
|- HVMap = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ( ( Base ` ( ( DVecH ` k ) ` w ) ) \ { ( 0g ` ( ( DVecH ` k ) ` w ) ) } ) |-> ( v e. ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` k ) ` w ) ) ) E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chvm 
 |-  HVMap
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vw 
 |-  w
4 clh 
 |-  LHyp
5 1 cv 
 |-  k
6 5 4 cfv 
 |-  ( LHyp ` k )
7 vx 
 |-  x
8 cbs 
 |-  Base
9 cdvh 
 |-  DVecH
10 5 9 cfv 
 |-  ( DVecH ` k )
11 3 cv 
 |-  w
12 11 10 cfv 
 |-  ( ( DVecH ` k ) ` w )
13 12 8 cfv 
 |-  ( Base ` ( ( DVecH ` k ) ` w ) )
14 c0g 
 |-  0g
15 12 14 cfv 
 |-  ( 0g ` ( ( DVecH ` k ) ` w ) )
16 15 csn 
 |-  { ( 0g ` ( ( DVecH ` k ) ` w ) ) }
17 13 16 cdif 
 |-  ( ( Base ` ( ( DVecH ` k ) ` w ) ) \ { ( 0g ` ( ( DVecH ` k ) ` w ) ) } )
18 vv 
 |-  v
19 vj 
 |-  j
20 csca 
 |-  Scalar
21 12 20 cfv 
 |-  ( Scalar ` ( ( DVecH ` k ) ` w ) )
22 21 8 cfv 
 |-  ( Base ` ( Scalar ` ( ( DVecH ` k ) ` w ) ) )
23 vt 
 |-  t
24 coch 
 |-  ocH
25 5 24 cfv 
 |-  ( ocH ` k )
26 11 25 cfv 
 |-  ( ( ocH ` k ) ` w )
27 7 cv 
 |-  x
28 27 csn 
 |-  { x }
29 28 26 cfv 
 |-  ( ( ( ocH ` k ) ` w ) ` { x } )
30 18 cv 
 |-  v
31 23 cv 
 |-  t
32 cplusg 
 |-  +g
33 12 32 cfv 
 |-  ( +g ` ( ( DVecH ` k ) ` w ) )
34 19 cv 
 |-  j
35 cvsca 
 |-  .s
36 12 35 cfv 
 |-  ( .s ` ( ( DVecH ` k ) ` w ) )
37 34 27 36 co 
 |-  ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x )
38 31 37 33 co 
 |-  ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) )
39 30 38 wceq 
 |-  v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) )
40 39 23 29 wrex 
 |-  E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) )
41 40 19 22 crio 
 |-  ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` k ) ` w ) ) ) E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) )
42 18 13 41 cmpt 
 |-  ( v e. ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` k ) ` w ) ) ) E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) ) )
43 7 17 42 cmpt 
 |-  ( x e. ( ( Base ` ( ( DVecH ` k ) ` w ) ) \ { ( 0g ` ( ( DVecH ` k ) ` w ) ) } ) |-> ( v e. ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` k ) ` w ) ) ) E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) ) ) )
44 3 6 43 cmpt 
 |-  ( w e. ( LHyp ` k ) |-> ( x e. ( ( Base ` ( ( DVecH ` k ) ` w ) ) \ { ( 0g ` ( ( DVecH ` k ) ` w ) ) } ) |-> ( v e. ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` k ) ` w ) ) ) E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) ) ) ) )
45 1 2 44 cmpt 
 |-  ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ( ( Base ` ( ( DVecH ` k ) ` w ) ) \ { ( 0g ` ( ( DVecH ` k ) ` w ) ) } ) |-> ( v e. ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` k ) ` w ) ) ) E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) ) ) ) ) )
46 0 45 wceq 
 |-  HVMap = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ( ( Base ` ( ( DVecH ` k ) ` w ) ) \ { ( 0g ` ( ( DVecH ` k ) ` w ) ) } ) |-> ( v e. ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` k ) ` w ) ) ) E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) ) ) ) ) )