Definition df-hvmap 37046

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 36840, dochfl1 36765- should we update those to use this definition? (Contributed by NM, 23-Mar-2015.)

Assertion

Ref	Expression
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 ) ) ) ) ) ) )

Distinct variable group:   w, k, x, v, j, t

Detailed syntax breakdown of Definition df-hvmap

Step	Hyp	Ref	Expression
1		chvm 37045	. 2 class HVMap
2		vk	. . 3 setvar k
3		cvv 3200	. . 3 class _V
4		vw	. . . 4 setvar w
5	2	cv 1482	. . . . 5 class k
6		clh 35270	. . . . 5 class LHyp
7	5, 6	cfv 5888	. . . 4 class ( LHyp ` k )
8		vx	. . . . 5 setvar x
9	4	cv 1482	. . . . . . . 8 class w
10		cdvh 36367	. . . . . . . . 9 class DVecH
11	5, 10	cfv 5888	. . . . . . . 8 class ( DVecH ` k )
12	9, 11	cfv 5888	. . . . . . 7 class ( ( DVecH ` k ) ` w )
13		cbs 15857	. . . . . . 7 class Base
14	12, 13	cfv 5888	. . . . . 6 class ( Base ` ( ( DVecH ` k ) ` w ) )
15		c0g 16100	. . . . . . . 8 class 0g
16	12, 15	cfv 5888	. . . . . . 7 class ( 0g ` ( ( DVecH ` k ) ` w ) )
17	16	csn 4177	. . . . . 6 class { ( 0g ` ( ( DVecH ` k ) ` w ) ) }
18	14, 17	cdif 3571	. . . . 5 class ( ( Base ` ( ( DVecH ` k ) ` w ) ) \ { ( 0g ` ( ( DVecH ` k ) ` w ) ) } )
19		vv	. . . . . 6 setvar v
20	19	cv 1482	. . . . . . . . 9 class v
21		vt	. . . . . . . . . . 11 setvar t
22	21	cv 1482	. . . . . . . . . 10 class t
23		vj	. . . . . . . . . . . 12 setvar j
24	23	cv 1482	. . . . . . . . . . 11 class j
25	8	cv 1482	. . . . . . . . . . 11 class x
26		cvsca 15945	. . . . . . . . . . . 12 class .s
27	12, 26	cfv 5888	. . . . . . . . . . 11 class ( .s ` ( ( DVecH ` k ) ` w ) )
28	24, 25, 27	co 6650	. . . . . . . . . 10 class ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x )
29		cplusg 15941	. . . . . . . . . . 11 class +g
30	12, 29	cfv 5888	. . . . . . . . . 10 class ( +g ` ( ( DVecH ` k ) ` w ) )
31	22, 28, 30	co 6650	. . . . . . . . 9 class ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) )
32	20, 31	wceq 1483	. . . . . . . 8 wff v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) )
33	25	csn 4177	. . . . . . . . 9 class { x }
34		coch 36636	. . . . . . . . . . 11 class ocH
35	5, 34	cfv 5888	. . . . . . . . . 10 class ( ocH ` k )
36	9, 35	cfv 5888	. . . . . . . . 9 class ( ( ocH ` k ) ` w )
37	33, 36	cfv 5888	. . . . . . . 8 class ( ( ( ocH ` k ) ` w ) ` { x } )
38	32, 21, 37	wrex 2913	. . . . . . 7 wff E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) )
39		csca 15944	. . . . . . . . 9 class Scalar
40	12, 39	cfv 5888	. . . . . . . 8 class (Scalar ` ( ( DVecH ` k ) ` w ) )
41	40, 13	cfv 5888	. . . . . . 7 class ( Base ` (Scalar ` ( ( DVecH ` k ) ` w ) ) )
42	38, 23, 41	crio 6610	. . . . . 6 class ( 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	19, 14, 42	cmpt 4729	. . . . 5 class ( 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	8, 18, 43	cmpt 4729	. . . 4 class ( 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	4, 7, 44	cmpt 4729	. . 3 class ( 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	2, 3, 45	cmpt 4729	. 2 class ( 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 ) ) ) ) ) ) )
47	1, 46	wceq 1483	1 wff 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 ) ) ) ) ) ) )

This definition is referenced by:  hvmapffval  37047