Definition df-hgmap

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)

	Ref	Expression
Assertion	df-hgmap	⊢ HGMap = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chg	⊢ HGMap
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vw	⊢ 𝑤
4		clh	⊢ LHyp
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( LHyp ‘ 𝑘 )
7		va	⊢ 𝑎
8		cdvh	⊢ DVecH
9	5 8	cfv	⊢ ( DVecH ‘ 𝑘 )
10	3	cv	⊢ 𝑤
11	10 9	cfv	⊢ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 )
12		vu	⊢ 𝑢
13		cbs	⊢ Base
14		csca	⊢ Scalar
15	12	cv	⊢ 𝑢
16	15 14	cfv	⊢ ( Scalar ‘ 𝑢 )
17	16 13	cfv	⊢ ( Base ‘ ( Scalar ‘ 𝑢 ) )
18		vb	⊢ 𝑏
19		chdma	⊢ HDMap
20	5 19	cfv	⊢ ( HDMap ‘ 𝑘 )
21	10 20	cfv	⊢ ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 )
22		vm	⊢ 𝑚
23	7	cv	⊢ 𝑎
24		vx	⊢ 𝑥
25	18	cv	⊢ 𝑏
26		vy	⊢ 𝑦
27		vv	⊢ 𝑣
28	15 13	cfv	⊢ ( Base ‘ 𝑢 )
29	22	cv	⊢ 𝑚
30	24	cv	⊢ 𝑥
31		cvsca	⊢ ·𝑠
32	15 31	cfv	⊢ ( ·𝑠 ‘ 𝑢 )
33	27	cv	⊢ 𝑣
34	30 33 32	co	⊢ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 )
35	34 29	cfv	⊢ ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) )
36	26	cv	⊢ 𝑦
37		clcd	⊢ LCDual
38	5 37	cfv	⊢ ( LCDual ‘ 𝑘 )
39	10 38	cfv	⊢ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 )
40	39 31	cfv	⊢ ( ·𝑠 ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) )
41	33 29	cfv	⊢ ( 𝑚 ‘ 𝑣 )
42	36 41 40	co	⊢ ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) )
43	35 42	wceq	⊢ ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) )
44	43 27 28	wral	⊢ ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) )
45	44 26 25	crio	⊢ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) )
46	24 25 45	cmpt	⊢ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) )
47	23 46	wcel	⊢ 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) )
48	47 22 21	wsbc	⊢ [ ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) )
49	48 18 17	wsbc	⊢ [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) )
50	49 12 11	wsbc	⊢ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) )
51	50 7	cab	⊢ { 𝑎 ∣ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) }
52	3 6 51	cmpt	⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } )
53	1 2 52	cmpt	⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } ) )
54	0 53	wceq	⊢ HGMap = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } ) )