df-hdmap1 - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-hdmap1		Structured version Visualization version GIF version

Definition df-hdmap1 40750

Description: Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 40753 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((2^nd ‘𝑥) = (0_g‘𝑢), (0_g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))))}))

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

**Detailed syntax breakdown of Definition df-hdmap1**
Step	Hyp	Ref	Expression
1		chdma1 40748	. 2 class HDMap1
2		vk	. . 3 setvar 𝑘
3		cvv 3474	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1540	. . . . 5 class 𝑘
6		clh 38941	. . . . 5 class LHyp
7	5, 6	cfv 6543	. . . 4 class (LHyp‘𝑘)
8		va	. . . . . . . . . . . . . 14 setvar 𝑎
9	8	cv 1540	. . . . . . . . . . . . 13 class 𝑎
10		vx	. . . . . . . . . . . . . 14 setvar 𝑥
11		vv	. . . . . . . . . . . . . . . . 17 setvar 𝑣
12	11	cv 1540	. . . . . . . . . . . . . . . 16 class 𝑣
13		vd	. . . . . . . . . . . . . . . . 17 setvar 𝑑
14	13	cv 1540	. . . . . . . . . . . . . . . 16 class 𝑑
15	12, 14	cxp 5674	. . . . . . . . . . . . . . 15 class (𝑣 × 𝑑)
16	15, 12	cxp 5674	. . . . . . . . . . . . . 14 class ((𝑣 × 𝑑) × 𝑣)
17	10	cv 1540	. . . . . . . . . . . . . . . . 17 class 𝑥
18		c2nd 7976	. . . . . . . . . . . . . . . . 17 class 2^nd
19	17, 18	cfv 6543	. . . . . . . . . . . . . . . 16 class (2^nd ‘𝑥)
20		vu	. . . . . . . . . . . . . . . . . 18 setvar 𝑢
21	20	cv 1540	. . . . . . . . . . . . . . . . 17 class 𝑢
22		c0g 17387	. . . . . . . . . . . . . . . . 17 class 0_g
23	21, 22	cfv 6543	. . . . . . . . . . . . . . . 16 class (0_g‘𝑢)
24	19, 23	wceq 1541	. . . . . . . . . . . . . . 15 wff (2^nd ‘𝑥) = (0_g‘𝑢)
25		vc	. . . . . . . . . . . . . . . . 17 setvar 𝑐
26	25	cv 1540	. . . . . . . . . . . . . . . 16 class 𝑐
27	26, 22	cfv 6543	. . . . . . . . . . . . . . 15 class (0_g‘𝑐)
28	19	csn 4628	. . . . . . . . . . . . . . . . . . . 20 class {(2^nd ‘𝑥)}
29		vn	. . . . . . . . . . . . . . . . . . . . 21 setvar 𝑛
30	29	cv 1540	. . . . . . . . . . . . . . . . . . . 20 class 𝑛
31	28, 30	cfv 6543	. . . . . . . . . . . . . . . . . . 19 class (𝑛‘{(2^nd ‘𝑥)})
32		vm	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑚
33	32	cv 1540	. . . . . . . . . . . . . . . . . . 19 class 𝑚
34	31, 33	cfv 6543	. . . . . . . . . . . . . . . . . 18 class (𝑚‘(𝑛‘{(2^nd ‘𝑥)}))
35		vh	. . . . . . . . . . . . . . . . . . . . 21 setvar ℎ
36	35	cv 1540	. . . . . . . . . . . . . . . . . . . 20 class ℎ
37	36	csn 4628	. . . . . . . . . . . . . . . . . . 19 class {ℎ}
38		vj	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑗
39	38	cv 1540	. . . . . . . . . . . . . . . . . . 19 class 𝑗
40	37, 39	cfv 6543	. . . . . . . . . . . . . . . . . 18 class (𝑗‘{ℎ})
41	34, 40	wceq 1541	. . . . . . . . . . . . . . . . 17 wff (𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ})
42		c1st 7975	. . . . . . . . . . . . . . . . . . . . . . . 24 class 1^st
43	17, 42	cfv 6543	. . . . . . . . . . . . . . . . . . . . . . 23 class (1^st ‘𝑥)
44	43, 42	cfv 6543	. . . . . . . . . . . . . . . . . . . . . 22 class (1^st ‘(1^st ‘𝑥))
45		csg 18823	. . . . . . . . . . . . . . . . . . . . . . 23 class -_g
46	21, 45	cfv 6543	. . . . . . . . . . . . . . . . . . . . . 22 class (-_g‘𝑢)
47	44, 19, 46	co 7411	. . . . . . . . . . . . . . . . . . . . 21 class ((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))
48	47	csn 4628	. . . . . . . . . . . . . . . . . . . 20 class {((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))}
49	48, 30	cfv 6543	. . . . . . . . . . . . . . . . . . 19 class (𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})
50	49, 33	cfv 6543	. . . . . . . . . . . . . . . . . 18 class (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))}))
51	43, 18	cfv 6543	. . . . . . . . . . . . . . . . . . . . 21 class (2^nd ‘(1^st ‘𝑥))
52	26, 45	cfv 6543	. . . . . . . . . . . . . . . . . . . . 21 class (-_g‘𝑐)
53	51, 36, 52	co 7411	. . . . . . . . . . . . . . . . . . . 20 class ((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)
54	53	csn 4628	. . . . . . . . . . . . . . . . . . 19 class {((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)}
55	54, 39	cfv 6543	. . . . . . . . . . . . . . . . . 18 class (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})
56	50, 55	wceq 1541	. . . . . . . . . . . . . . . . 17 wff (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})
57	41, 56	wa 396	. . . . . . . . . . . . . . . 16 wff ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)}))
58	57, 35, 14	crio 7366	. . . . . . . . . . . . . . 15 class (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))
59	24, 27, 58	cif 4528	. . . . . . . . . . . . . 14 class if((2^nd ‘𝑥) = (0_g‘𝑢), (0_g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)}))))
60	10, 16, 59	cmpt 5231	. . . . . . . . . . . . 13 class (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2^nd ‘𝑥) = (0_g‘𝑢), (0_g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))))
61	9, 60	wcel 2106	. . . . . . . . . . . 12 wff 𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2^nd ‘𝑥) = (0_g‘𝑢), (0_g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))))
62	4	cv 1540	. . . . . . . . . . . . 13 class 𝑤
63		cmpd 40581	. . . . . . . . . . . . . 14 class mapd
64	5, 63	cfv 6543	. . . . . . . . . . . . 13 class (mapd‘𝑘)
65	62, 64	cfv 6543	. . . . . . . . . . . 12 class ((mapd‘𝑘)‘𝑤)
66	61, 32, 65	wsbc 3777	. . . . . . . . . . 11 wff [((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2^nd ‘𝑥) = (0_g‘𝑢), (0_g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))))
67		clspn 20587	. . . . . . . . . . . 12 class LSpan
68	26, 67	cfv 6543	. . . . . . . . . . 11 class (LSpan‘𝑐)
69	66, 38, 68	wsbc 3777	. . . . . . . . . 10 wff [(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2^nd ‘𝑥) = (0_g‘𝑢), (0_g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))))
70		cbs 17146	. . . . . . . . . . 11 class Base
71	26, 70	cfv 6543	. . . . . . . . . 10 class (Base‘𝑐)
72	69, 13, 71	wsbc 3777	. . . . . . . . 9 wff [(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2^nd ‘𝑥) = (0_g‘𝑢), (0_g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))))
73		clcd 40543	. . . . . . . . . . 11 class LCDual
74	5, 73	cfv 6543	. . . . . . . . . 10 class (LCDual‘𝑘)
75	62, 74	cfv 6543	. . . . . . . . 9 class ((LCDual‘𝑘)‘𝑤)
76	72, 25, 75	wsbc 3777	. . . . . . . 8 wff [((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2^nd ‘𝑥) = (0_g‘𝑢), (0_g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))))
77	21, 67	cfv 6543	. . . . . . . 8 class (LSpan‘𝑢)
78	76, 29, 77	wsbc 3777	. . . . . . 7 wff [(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2^nd ‘𝑥) = (0_g‘𝑢), (0_g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))))
79	21, 70	cfv 6543	. . . . . . 7 class (Base‘𝑢)
80	78, 11, 79	wsbc 3777	. . . . . 6 wff [(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2^nd ‘𝑥) = (0_g‘𝑢), (0_g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))))
81		cdvh 40035	. . . . . . . 8 class DVecH
82	5, 81	cfv 6543	. . . . . . 7 class (DVecH‘𝑘)
83	62, 82	cfv 6543	. . . . . 6 class ((DVecH‘𝑘)‘𝑤)
84	80, 20, 83	wsbc 3777	. . . . 5 wff [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2^nd ‘𝑥) = (0_g‘𝑢), (0_g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))))
85	84, 8	cab 2709	. . . 4 class {𝑎 ∣ [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2^nd ‘𝑥) = (0_g‘𝑢), (0_g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))))}
86	4, 7, 85	cmpt 5231	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2^nd ‘𝑥) = (0_g‘𝑢), (0_g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))))})
87	2, 3, 86	cmpt 5231	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2^nd ‘𝑥) = (0_g‘𝑢), (0_g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))))}))
88	1, 87	wceq 1541	1 wff HDMap1 = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2^nd ‘𝑥) = (0_g‘𝑢), (0_g‘𝑐), (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ∧ (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))))}))

Colors of variables: wff setvar class

This definition is referenced by: hdmap1ffval 40752

W3C validator