Definition df-hgmap 37176

Description: Define map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.)

Assertion

Ref	Expression
df-hgmap	|- HGMap = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` (Scalar ` u ) ) / b ]. [. ( (HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( (LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) } ) )

Distinct variable group:   a, b, k, m, u, v, w, x, y

Detailed syntax breakdown of Definition df-hgmap

Step	Hyp	Ref	Expression
1		chg 37175	. 2 class HGMap
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	. . . . . . . . . 10 setvar a
9	8	cv 1482	. . . . . . . . 9 class a
10		vx	. . . . . . . . . 10 setvar x
11		vb	. . . . . . . . . . 11 setvar b
12	11	cv 1482	. . . . . . . . . 10 class b
13	10	cv 1482	. . . . . . . . . . . . . . 15 class x
14		vv	. . . . . . . . . . . . . . . 16 setvar v
15	14	cv 1482	. . . . . . . . . . . . . . 15 class v
16		vu	. . . . . . . . . . . . . . . . 17 setvar u
17	16	cv 1482	. . . . . . . . . . . . . . . 16 class u
18		cvsca 15945	. . . . . . . . . . . . . . . 16 class .s
19	17, 18	cfv 5888	. . . . . . . . . . . . . . 15 class ( .s ` u )
20	13, 15, 19	co 6650	. . . . . . . . . . . . . 14 class ( x ( .s ` u ) v )
21		vm	. . . . . . . . . . . . . . 15 setvar m
22	21	cv 1482	. . . . . . . . . . . . . 14 class m
23	20, 22	cfv 5888	. . . . . . . . . . . . 13 class ( m ` ( x ( .s ` u ) v ) )
24		vy	. . . . . . . . . . . . . . 15 setvar y
25	24	cv 1482	. . . . . . . . . . . . . 14 class y
26	15, 22	cfv 5888	. . . . . . . . . . . . . 14 class ( m ` v )
27	4	cv 1482	. . . . . . . . . . . . . . . 16 class w
28		clcd 36875	. . . . . . . . . . . . . . . . 17 class LCDual
29	5, 28	cfv 5888	. . . . . . . . . . . . . . . 16 class (LCDual ` k )
30	27, 29	cfv 5888	. . . . . . . . . . . . . . 15 class ( (LCDual ` k ) ` w )
31	30, 18	cfv 5888	. . . . . . . . . . . . . 14 class ( .s ` ( (LCDual ` k ) ` w ) )
32	25, 26, 31	co 6650	. . . . . . . . . . . . 13 class ( y ( .s ` ( (LCDual ` k ) ` w ) ) ( m ` v ) )
33	23, 32	wceq 1483	. . . . . . . . . . . 12 wff ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( (LCDual ` k ) ` w ) ) ( m ` v ) )
34		cbs 15857	. . . . . . . . . . . . 13 class Base
35	17, 34	cfv 5888	. . . . . . . . . . . 12 class ( Base ` u )
36	33, 14, 35	wral 2912	. . . . . . . . . . 11 wff A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( (LCDual ` k ) ` w ) ) ( m ` v ) )
37	36, 24, 12	crio 6610	. . . . . . . . . 10 class ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( (LCDual ` k ) ` w ) ) ( m ` v ) ) )
38	10, 12, 37	cmpt 4729	. . . . . . . . 9 class ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( (LCDual ` k ) ` w ) ) ( m ` v ) ) ) )
39	9, 38	wcel 1990	. . . . . . . 8 wff a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( (LCDual ` k ) ` w ) ) ( m ` v ) ) ) )
40		chdma 37082	. . . . . . . . . 10 class HDMap
41	5, 40	cfv 5888	. . . . . . . . 9 class (HDMap ` k )
42	27, 41	cfv 5888	. . . . . . . 8 class ( (HDMap ` k ) ` w )
43	39, 21, 42	wsbc 3435	. . . . . . 7 wff [. ( (HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( (LCDual ` k ) ` w ) ) ( m ` v ) ) ) )
44		csca 15944	. . . . . . . . 9 class Scalar
45	17, 44	cfv 5888	. . . . . . . 8 class (Scalar ` u )
46	45, 34	cfv 5888	. . . . . . 7 class ( Base ` (Scalar ` u ) )
47	43, 11, 46	wsbc 3435	. . . . . 6 wff [. ( Base ` (Scalar ` u ) ) / b ]. [. ( (HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( (LCDual ` k ) ` w ) ) ( m ` v ) ) ) )
48		cdvh 36367	. . . . . . . 8 class DVecH
49	5, 48	cfv 5888	. . . . . . 7 class ( DVecH ` k )
50	27, 49	cfv 5888	. . . . . 6 class ( ( DVecH ` k ) ` w )
51	47, 16, 50	wsbc 3435	. . . . 5 wff [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` (Scalar ` u ) ) / b ]. [. ( (HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( (LCDual ` k ) ` w ) ) ( m ` v ) ) ) )
52	51, 8	cab 2608	. . . 4 class { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` (Scalar ` u ) ) / b ]. [. ( (HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( (LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) }
53	4, 7, 52	cmpt 4729	. . 3 class ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` (Scalar ` u ) ) / b ]. [. ( (HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( (LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) } )
54	2, 3, 53	cmpt 4729	. 2 class ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` (Scalar ` u ) ) / b ]. [. ( (HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( (LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) } ) )
55	1, 54	wceq 1483	1 wff HGMap = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` (Scalar ` u ) ) / b ]. [. ( (HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( (LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) } ) )

This definition is referenced by:  hgmapffval  37177