Definition df-hdmap1 42850

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

Assertion

Ref	Expression
df-hdmap1	⊢ HDMap1 = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))}))

Distinct variable group:   𝑎,𝑐,𝑑,ℎ,𝑗,𝑘,𝑚,𝑛,𝑢,𝑣,𝑤,𝑥

Detailed syntax breakdown of Definition df-hdmap1

Step	Hyp	Ref	Expression
1		chdma1 42848	. 2 class HDMap1
2		vk	. . 3 setvar 𝑘
3		cvv 3451	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1569	. . . . 5 class 𝑘
6		clh 41041	. . . . 5 class LHyp
7	5, 6	cfv 6538	. . . 4 class (LHyp‘𝑘)
8		va	. . . . . . . . . . . . . 14 setvar 𝑎
9	8	cv 1569	. . . . . . . . . . . . 13 class 𝑎
10		vx	. . . . . . . . . . . . . 14 setvar 𝑥
11		vv	. . . . . . . . . . . . . . . . 17 setvar 𝑣
12	11	cv 1569	. . . . . . . . . . . . . . . 16 class 𝑣
13		vd	. . . . . . . . . . . . . . . . 17 setvar 𝑑
14	13	cv 1569	. . . . . . . . . . . . . . . 16 class 𝑑
15	12, 14	cxp 5649	. . . . . . . . . . . . . . 15 class (𝑣 × 𝑑)
16	15, 12	cxp 5649	. . . . . . . . . . . . . 14 class ((𝑣 × 𝑑) × 𝑣)
17	10	cv 1569	. . . . . . . . . . . . . . . . 17 class 𝑥
18		c2nd 8000	. . . . . . . . . . . . . . . . 17 class 2nd
19	17, 18	cfv 6538	. . . . . . . . . . . . . . . 16 class (2nd ‘𝑥)
20		vu	. . . . . . . . . . . . . . . . . 18 setvar 𝑢
21	20	cv 1569	. . . . . . . . . . . . . . . . 17 class 𝑢
22		c0g 17610	. . . . . . . . . . . . . . . . 17 class 0g
23	21, 22	cfv 6538	. . . . . . . . . . . . . . . 16 class (0g‘𝑢)
24	19, 23	wceq 1570	. . . . . . . . . . . . . . 15 wff (2nd ‘𝑥) = (0g‘𝑢)
25		vc	. . . . . . . . . . . . . . . . 17 setvar 𝑐
26	25	cv 1569	. . . . . . . . . . . . . . . 16 class 𝑐
27	26, 22	cfv 6538	. . . . . . . . . . . . . . 15 class (0g‘𝑐)
28	19	csn 4584	. . . . . . . . . . . . . . . . . . . 20 class {(2nd ‘𝑥)}
29		vn	. . . . . . . . . . . . . . . . . . . . 21 setvar 𝑛
30	29	cv 1569	. . . . . . . . . . . . . . . . . . . 20 class 𝑛
31	28, 30	cfv 6538	. . . . . . . . . . . . . . . . . . 19 class (𝑛‘{(2nd ‘𝑥)})
32		vm	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑚
33	32	cv 1569	. . . . . . . . . . . . . . . . . . 19 class 𝑚
34	31, 33	cfv 6538	. . . . . . . . . . . . . . . . . 18 class (𝑚‘(𝑛‘{(2nd ‘𝑥)}))
35		vh	. . . . . . . . . . . . . . . . . . . . 21 setvar ℎ
36	35	cv 1569	. . . . . . . . . . . . . . . . . . . 20 class ℎ
37	36	csn 4584	. . . . . . . . . . . . . . . . . . 19 class {ℎ}
38		vj	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑗
39	38	cv 1569	. . . . . . . . . . . . . . . . . . 19 class 𝑗
40	37, 39	cfv 6538	. . . . . . . . . . . . . . . . . 18 class (𝑗‘{ℎ})
41	34, 40	wceq 1570	. . . . . . . . . . . . . . . . 17 wff (𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ})
42		c1st 7999	. . . . . . . . . . . . . . . . . . . . . . . 24 class 1st
43	17, 42	cfv 6538	. . . . . . . . . . . . . . . . . . . . . . 23 class (1st ‘𝑥)
44	43, 42	cfv 6538	. . . . . . . . . . . . . . . . . . . . . 22 class (1st ‘(1st ‘𝑥))
45		csg 19146	. . . . . . . . . . . . . . . . . . . . . . 23 class -g
46	21, 45	cfv 6538	. . . . . . . . . . . . . . . . . . . . . 22 class (-g‘𝑢)
47	44, 19, 46	co 7420	. . . . . . . . . . . . . . . . . . . . 21 class ((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))
48	47	csn 4584	. . . . . . . . . . . . . . . . . . . 20 class {((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))}
49	48, 30	cfv 6538	. . . . . . . . . . . . . . . . . . 19 class (𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})
50	49, 33	cfv 6538	. . . . . . . . . . . . . . . . . 18 class (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))}))
51	43, 18	cfv 6538	. . . . . . . . . . . . . . . . . . . . 21 class (2nd ‘(1st ‘𝑥))
52	26, 45	cfv 6538	. . . . . . . . . . . . . . . . . . . . 21 class (-g‘𝑐)
53	51, 36, 52	co 7420	. . . . . . . . . . . . . . . . . . . 20 class ((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)
54	53	csn 4584	. . . . . . . . . . . . . . . . . . 19 class {((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)}
55	54, 39	cfv 6538	. . . . . . . . . . . . . . . . . 18 class (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})
56	50, 55	wceq 1570	. . . . . . . . . . . . . . . . 17 wff (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})
57	41, 56	wa 401	. . . . . . . . . . . . . . . 16 wff ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))
58	57, 35, 14	crio 7376	. . . . . . . . . . . . . . 15 class (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))
59	24, 27, 58	cif 4482	. . . . . . . . . . . . . 14 class if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)}))))
60	10, 16, 59	cmpt 5186	. . . . . . . . . . . . 13 class (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))
61	9, 60	wcel 2145	. . . . . . . . . . . 12 wff 𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))
62	4	cv 1569	. . . . . . . . . . . . 13 class 𝑤
63		cmpd 42681	. . . . . . . . . . . . . 14 class mapd
64	5, 63	cfv 6538	. . . . . . . . . . . . 13 class (mapd‘𝑘)
65	62, 64	cfv 6538	. . . . . . . . . . . 12 class ((mapd‘𝑘)‘𝑤)
66	61, 32, 65	wsbc 3739	. . . . . . . . . . 11 wff [((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))
67		clspn 21246	. . . . . . . . . . . 12 class LSpan
68	26, 67	cfv 6538	. . . . . . . . . . 11 class (LSpan‘𝑐)
69	66, 38, 68	wsbc 3739	. . . . . . . . . 10 wff [(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))
70		cbs 17387	. . . . . . . . . . 11 class Base
71	26, 70	cfv 6538	. . . . . . . . . 10 class (Base‘𝑐)
72	69, 13, 71	wsbc 3739	. . . . . . . . 9 wff [(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))
73		clcd 42643	. . . . . . . . . . 11 class LCDual
74	5, 73	cfv 6538	. . . . . . . . . 10 class (LCDual‘𝑘)
75	62, 74	cfv 6538	. . . . . . . . 9 class ((LCDual‘𝑘)‘𝑤)
76	72, 25, 75	wsbc 3739	. . . . . . . 8 wff [((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))
77	21, 67	cfv 6538	. . . . . . . 8 class (LSpan‘𝑢)
78	76, 29, 77	wsbc 3739	. . . . . . 7 wff [(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))
79	21, 70	cfv 6538	. . . . . . 7 class (Base‘𝑢)
80	78, 11, 79	wsbc 3739	. . . . . 6 wff [(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))
81		cdvh 42135	. . . . . . . 8 class DVecH
82	5, 81	cfv 6538	. . . . . . 7 class (DVecH‘𝑘)
83	62, 82	cfv 6538	. . . . . 6 class ((DVecH‘𝑘)‘𝑤)
84	80, 20, 83	wsbc 3739	. . . . 5 wff [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))
85	84, 8	cab 2739	. . . 4 class {𝑎 ∣ [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))}
86	4, 7, 85	cmpt 5186	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))})
87	2, 3, 86	cmpt 5186	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))}))
88	1, 87	wceq 1570	1 wff HDMap1 = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd ‘𝑥) = (0g‘𝑢), (0g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st ‘𝑥))(-g‘𝑢)(2nd ‘𝑥))})) = (𝑗‘{((2nd ‘(1st ‘𝑥))(-g‘𝑐)ℎ)})))))}))

This definition is used by:  hdmap1ffval  42852