Definition df-hdmap 37084

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

Assertion

Ref

Expression

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 >. ) ) ) ) } ) )

Distinct variable group:   e, a, i, k, t, u, v, w, y, z

Detailed syntax breakdown of Definition df-hdmap

Step	Hyp	Ref	Expression
1		chdma 37082	. 2 class HDMap
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		va	. . . . . . . . . . 11 setvar a
9	8	cv 1482	. . . . . . . . . 10 class a
10		vt	. . . . . . . . . . 11 setvar t
11		vv	. . . . . . . . . . . 12 setvar v
12	11	cv 1482	. . . . . . . . . . 11 class v
13		vz	. . . . . . . . . . . . . . . . 17 setvar z
14	13	cv 1482	. . . . . . . . . . . . . . . 16 class z
15		ve	. . . . . . . . . . . . . . . . . . . 20 setvar e
16	15	cv 1482	. . . . . . . . . . . . . . . . . . 19 class e
17	16	csn 4177	. . . . . . . . . . . . . . . . . 18 class { e }
18		vu	. . . . . . . . . . . . . . . . . . . 20 setvar u
19	18	cv 1482	. . . . . . . . . . . . . . . . . . 19 class u
20		clspn 18971	. . . . . . . . . . . . . . . . . . 19 class LSpan
21	19, 20	cfv 5888	. . . . . . . . . . . . . . . . . 18 class ( LSpan ` u )
22	17, 21	cfv 5888	. . . . . . . . . . . . . . . . 17 class ( ( LSpan ` u ) ` { e } )
23	10	cv 1482	. . . . . . . . . . . . . . . . . . 19 class t
24	23	csn 4177	. . . . . . . . . . . . . . . . . 18 class { t }
25	24, 21	cfv 5888	. . . . . . . . . . . . . . . . 17 class ( ( LSpan ` u ) ` { t } )
26	22, 25	cun 3572	. . . . . . . . . . . . . . . 16 class ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) )
27	14, 26	wcel 1990	. . . . . . . . . . . . . . 15 wff z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) )
28	27	wn 3	. . . . . . . . . . . . . 14 wff -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) )
29		vy	. . . . . . . . . . . . . . . 16 setvar y
30	29	cv 1482	. . . . . . . . . . . . . . 15 class y
31	4	cv 1482	. . . . . . . . . . . . . . . . . . . . 21 class w
32		chvm 37045	. . . . . . . . . . . . . . . . . . . . . 22 class HVMap
33	5, 32	cfv 5888	. . . . . . . . . . . . . . . . . . . . 21 class (HVMap ` k )
34	31, 33	cfv 5888	. . . . . . . . . . . . . . . . . . . 20 class ( (HVMap ` k ) ` w )
35	16, 34	cfv 5888	. . . . . . . . . . . . . . . . . . 19 class ( ( (HVMap ` k ) ` w ) ` e )
36	16, 35, 14	cotp 4185	. . . . . . . . . . . . . . . . . 18 class <. e , ( ( (HVMap ` k ) ` w ) ` e ) , z >.
37		vi	. . . . . . . . . . . . . . . . . . 19 setvar i
38	37	cv 1482	. . . . . . . . . . . . . . . . . 18 class i
39	36, 38	cfv 5888	. . . . . . . . . . . . . . . . 17 class ( i ` <. e , ( ( (HVMap ` k ) ` w ) ` e ) , z >. )
40	14, 39, 23	cotp 4185	. . . . . . . . . . . . . . . 16 class <. z , ( i ` <. e , ( ( (HVMap ` k ) ` w ) ` e ) , z >. ) , t >.
41	40, 38	cfv 5888	. . . . . . . . . . . . . . 15 class ( i ` <. z , ( i ` <. e , ( ( (HVMap ` k ) ` w ) ` e ) , z >. ) , t >. )
42	30, 41	wceq 1483	. . . . . . . . . . . . . 14 wff y = ( i ` <. z , ( i ` <. e , ( ( (HVMap ` k ) ` w ) ` e ) , z >. ) , t >. )
43	28, 42	wi 4	. . . . . . . . . . . . 13 wff ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( (HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) )
44	43, 13, 12	wral 2912	. . . . . . . . . . . 12 wff A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( (HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) )
45		clcd 36875	. . . . . . . . . . . . . . 15 class LCDual
46	5, 45	cfv 5888	. . . . . . . . . . . . . 14 class (LCDual ` k )
47	31, 46	cfv 5888	. . . . . . . . . . . . 13 class ( (LCDual ` k ) ` w )
48		cbs 15857	. . . . . . . . . . . . 13 class Base
49	47, 48	cfv 5888	. . . . . . . . . . . 12 class ( Base ` ( (LCDual ` k ) ` w ) )
50	44, 29, 49	crio 6610	. . . . . . . . . . 11 class ( 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 >. ) ) )
51	10, 12, 50	cmpt 4729	. . . . . . . . . 10 class ( 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 >. ) ) ) )
52	9, 51	wcel 1990	. . . . . . . . 9 wff 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 >. ) ) ) )
53		chdma1 37081	. . . . . . . . . . 11 class HDMap1
54	5, 53	cfv 5888	. . . . . . . . . 10 class (HDMap1 ` k )
55	31, 54	cfv 5888	. . . . . . . . 9 class ( (HDMap1 ` k ) ` w )
56	52, 37, 55	wsbc 3435	. . . . . . . 8 wff [. ( (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 >. ) ) ) )
57	19, 48	cfv 5888	. . . . . . . 8 class ( Base ` u )
58	56, 11, 57	wsbc 3435	. . . . . . 7 wff [. ( 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 >. ) ) ) )
59		cdvh 36367	. . . . . . . . 9 class DVecH
60	5, 59	cfv 5888	. . . . . . . 8 class ( DVecH ` k )
61	31, 60	cfv 5888	. . . . . . 7 class ( ( DVecH ` k ) ` w )
62	58, 18, 61	wsbc 3435	. . . . . 6 wff [. ( ( 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 >. ) ) ) )
63		cid 5023	. . . . . . . 8 class _I
64	5, 48	cfv 5888	. . . . . . . 8 class ( Base ` k )
65	63, 64	cres 5116	. . . . . . 7 class ( _I |` ( Base ` k ) )
66		cltrn 35387	. . . . . . . . . 10 class LTrn
67	5, 66	cfv 5888	. . . . . . . . 9 class ( LTrn ` k )
68	31, 67	cfv 5888	. . . . . . . 8 class ( ( LTrn ` k ) ` w )
69	63, 68	cres 5116	. . . . . . 7 class ( _I |` ( ( LTrn ` k ) ` w ) )
70	65, 69	cop 4183	. . . . . 6 class <. ( _I |` ( Base ` k ) ) , ( _I |` ( ( LTrn ` k ) ` w ) ) >.
71	62, 15, 70	wsbc 3435	. . . . 5 wff [. <. ( _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	71, 8	cab 2608	. . . 4 class { 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	4, 7, 72	cmpt 4729	. . 3 class ( 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	2, 3, 73	cmpt 4729	. 2 class ( 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 >. ) ) ) ) } ) )
75	1, 74	wceq 1483	1 wff 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 >. ) ) ) ) } ) )

This definition is referenced by:  hdmapffval  37118