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	$$⊢\mathrm{HGMap}=\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chg	$$class\mathrm{HGMap}$$
1		vk	$$setvark$$
2		cvv	$$class\mathrm{V}$$
3		vw	$$setvarw$$
4		clh	$$class\mathrm{LHyp}$$
5	1	cv	$$setvark$$
6	5 4	cfv	$$class\mathrm{LHyp}\left(k\right)$$
7		va	$$setvara$$
8		cdvh	$$class\mathrm{DVecH}$$
9	5 8	cfv	$$class\mathrm{DVecH}\left(k\right)$$
10	3	cv	$$setvarw$$
11	10 9	cfv	$$class\mathrm{DVecH}\left(k\right)\left(w\right)$$
12		vu	$$setvaru$$
13		cbs	$$class\mathrm{Base}$$
14		csca	$$class\mathrm{Scalar}$$
15	12	cv	$$setvaru$$
16	15 14	cfv	$$class\mathrm{Scalar}\left(u\right)$$
17	16 13	cfv	$$class{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}$$
18		vb	$$setvarb$$
19		chdma	$$class\mathrm{HDMap}$$
20	5 19	cfv	$$class\mathrm{HDMap}\left(k\right)$$
21	10 20	cfv	$$class\mathrm{HDMap}\left(k\right)\left(w\right)$$
22		vm	$$setvarm$$
23	7	cv	$$setvara$$
24		vx	$$setvarx$$
25	18	cv	$$setvarb$$
26		vy	$$setvary$$
27		vv	$$setvarv$$
28	15 13	cfv	$$class{\mathrm{Base}}_u$$
29	22	cv	$$setvarm$$
30	24	cv	$$setvarx$$
31		cvsca	$$class{\cdot }_{𝑠}$$
32	15 31	cfv	$$class{\cdot }_u$$
33	27	cv	$$setvarv$$
34	30 33 32	co	$$class\left(x{\cdot }_{u}v\right)$$
35	34 29	cfv	$$classm\left(x{\cdot }_{u}v\right)$$
36	26	cv	$$setvary$$
37		clcd	$$class\mathrm{LCDual}$$
38	5 37	cfv	$$class\mathrm{LCDual}\left(k\right)$$
39	10 38	cfv	$$class\mathrm{LCDual}\left(k\right)\left(w\right)$$
40	39 31	cfv	$$class{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}$$
41	33 29	cfv	$$classm\left(v\right)$$
42	36 41 40	co	$$class\left(y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)$$
43	35 42	wceq	$$wffm\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)$$
44	43 27 28	wral	$$wff\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)$$
45	44 26 25	crio	$$class\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)$$
46	24 25 45	cmpt	$$class\left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)$$
47	23 46	wcel	$$wffa\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)$$
48	47 22 21	wsbc	$$wff\underset{\dot{}}{[}\mathrm{HDMap}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)$$
49	48 18 17	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)$$
50	49 12 11	wsbc	$$wff\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)$$
51	50 7	cab	$$class\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)\right\}$$
52	3 6 51	cmpt	$$class\left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)$$
53	1 2 52	cmpt	$$class\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)\right)$$
54	0 53	wceq	$$wff\mathrm{HGMap}=\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)\right)$$