Definition df-hgmap 40755

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 = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 ∀𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠 ‘𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚‘𝑣))))}))

Distinct variable group:   𝑎,𝑏,𝑘,𝑚,𝑢,𝑣,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-hgmap

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

This definition is referenced by:  hgmapffval  40756