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 39108
 Description: Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 39111 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
StepHypRef Expression
1 chdma1 39106 . 2 class HDMap1
2 vk . . 3 setvar 𝑘
3 cvv 3441 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1537 . . . . 5 class 𝑘
6 clh 37299 . . . . 5 class LHyp
75, 6cfv 6325 . . . 4 class (LHyp‘𝑘)
8 va . . . . . . . . . . . . . 14 setvar 𝑎
98cv 1537 . . . . . . . . . . . . 13 class 𝑎
10 vx . . . . . . . . . . . . . 14 setvar 𝑥
11 vv . . . . . . . . . . . . . . . . 17 setvar 𝑣
1211cv 1537 . . . . . . . . . . . . . . . 16 class 𝑣
13 vd . . . . . . . . . . . . . . . . 17 setvar 𝑑
1413cv 1537 . . . . . . . . . . . . . . . 16 class 𝑑
1512, 14cxp 5518 . . . . . . . . . . . . . . 15 class (𝑣 × 𝑑)
1615, 12cxp 5518 . . . . . . . . . . . . . 14 class ((𝑣 × 𝑑) × 𝑣)
1710cv 1537 . . . . . . . . . . . . . . . . 17 class 𝑥
18 c2nd 7673 . . . . . . . . . . . . . . . . 17 class 2nd
1917, 18cfv 6325 . . . . . . . . . . . . . . . 16 class (2nd𝑥)
20 vu . . . . . . . . . . . . . . . . . 18 setvar 𝑢
2120cv 1537 . . . . . . . . . . . . . . . . 17 class 𝑢
22 c0g 16708 . . . . . . . . . . . . . . . . 17 class 0g
2321, 22cfv 6325 . . . . . . . . . . . . . . . 16 class (0g𝑢)
2419, 23wceq 1538 . . . . . . . . . . . . . . 15 wff (2nd𝑥) = (0g𝑢)
25 vc . . . . . . . . . . . . . . . . 17 setvar 𝑐
2625cv 1537 . . . . . . . . . . . . . . . 16 class 𝑐
2726, 22cfv 6325 . . . . . . . . . . . . . . 15 class (0g𝑐)
2819csn 4525 . . . . . . . . . . . . . . . . . . . 20 class {(2nd𝑥)}
29 vn . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑛
3029cv 1537 . . . . . . . . . . . . . . . . . . . 20 class 𝑛
3128, 30cfv 6325 . . . . . . . . . . . . . . . . . . 19 class (𝑛‘{(2nd𝑥)})
32 vm . . . . . . . . . . . . . . . . . . . 20 setvar 𝑚
3332cv 1537 . . . . . . . . . . . . . . . . . . 19 class 𝑚
3431, 33cfv 6325 . . . . . . . . . . . . . . . . . 18 class (𝑚‘(𝑛‘{(2nd𝑥)}))
35 vh . . . . . . . . . . . . . . . . . . . . 21 setvar
3635cv 1537 . . . . . . . . . . . . . . . . . . . 20 class
3736csn 4525 . . . . . . . . . . . . . . . . . . 19 class {}
38 vj . . . . . . . . . . . . . . . . . . . 20 setvar 𝑗
3938cv 1537 . . . . . . . . . . . . . . . . . . 19 class 𝑗
4037, 39cfv 6325 . . . . . . . . . . . . . . . . . 18 class (𝑗‘{})
4134, 40wceq 1538 . . . . . . . . . . . . . . . . 17 wff (𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{})
42 c1st 7672 . . . . . . . . . . . . . . . . . . . . . . . 24 class 1st
4317, 42cfv 6325 . . . . . . . . . . . . . . . . . . . . . . 23 class (1st𝑥)
4443, 42cfv 6325 . . . . . . . . . . . . . . . . . . . . . 22 class (1st ‘(1st𝑥))
45 csg 18100 . . . . . . . . . . . . . . . . . . . . . . 23 class -g
4621, 45cfv 6325 . . . . . . . . . . . . . . . . . . . . . 22 class (-g𝑢)
4744, 19, 46co 7136 . . . . . . . . . . . . . . . . . . . . 21 class ((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))
4847csn 4525 . . . . . . . . . . . . . . . . . . . 20 class {((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))}
4948, 30cfv 6325 . . . . . . . . . . . . . . . . . . 19 class (𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})
5049, 33cfv 6325 . . . . . . . . . . . . . . . . . 18 class (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))}))
5143, 18cfv 6325 . . . . . . . . . . . . . . . . . . . . 21 class (2nd ‘(1st𝑥))
5226, 45cfv 6325 . . . . . . . . . . . . . . . . . . . . 21 class (-g𝑐)
5351, 36, 52co 7136 . . . . . . . . . . . . . . . . . . . 20 class ((2nd ‘(1st𝑥))(-g𝑐))
5453csn 4525 . . . . . . . . . . . . . . . . . . 19 class {((2nd ‘(1st𝑥))(-g𝑐))}
5554, 39cfv 6325 . . . . . . . . . . . . . . . . . 18 class (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})
5650, 55wceq 1538 . . . . . . . . . . . . . . . . 17 wff (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})
5741, 56wa 399 . . . . . . . . . . . . . . . 16 wff ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))}))
5857, 35, 14crio 7093 . . . . . . . . . . . . . . 15 class (𝑑 ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})))
5924, 27, 58cif 4425 . . . . . . . . . . . . . 14 class if((2nd𝑥) = (0g𝑢), (0g𝑐), (𝑑 ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))}))))
6010, 16, 59cmpt 5111 . . . . . . . . . . . . 13 class (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd𝑥) = (0g𝑢), (0g𝑐), (𝑑 ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})))))
619, 60wcel 2111 . . . . . . . . . . . 12 wff 𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd𝑥) = (0g𝑢), (0g𝑐), (𝑑 ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})))))
624cv 1537 . . . . . . . . . . . . 13 class 𝑤
63 cmpd 38939 . . . . . . . . . . . . . 14 class mapd
645, 63cfv 6325 . . . . . . . . . . . . 13 class (mapd‘𝑘)
6562, 64cfv 6325 . . . . . . . . . . . 12 class ((mapd‘𝑘)‘𝑤)
6661, 32, 65wsbc 3720 . . . . . . . . . . 11 wff [((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd𝑥) = (0g𝑢), (0g𝑐), (𝑑 ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})))))
67 clspn 19740 . . . . . . . . . . . 12 class LSpan
6826, 67cfv 6325 . . . . . . . . . . 11 class (LSpan‘𝑐)
6966, 38, 68wsbc 3720 . . . . . . . . . 10 wff [(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd𝑥) = (0g𝑢), (0g𝑐), (𝑑 ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})))))
70 cbs 16478 . . . . . . . . . . 11 class Base
7126, 70cfv 6325 . . . . . . . . . 10 class (Base‘𝑐)
7269, 13, 71wsbc 3720 . . . . . . . . 9 wff [(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd𝑥) = (0g𝑢), (0g𝑐), (𝑑 ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})))))
73 clcd 38901 . . . . . . . . . . 11 class LCDual
745, 73cfv 6325 . . . . . . . . . 10 class (LCDual‘𝑘)
7562, 74cfv 6325 . . . . . . . . 9 class ((LCDual‘𝑘)‘𝑤)
7672, 25, 75wsbc 3720 . . . . . . . 8 wff [((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd𝑥) = (0g𝑢), (0g𝑐), (𝑑 ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})))))
7721, 67cfv 6325 . . . . . . . 8 class (LSpan‘𝑢)
7876, 29, 77wsbc 3720 . . . . . . 7 wff [(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd𝑥) = (0g𝑢), (0g𝑐), (𝑑 ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})))))
7921, 70cfv 6325 . . . . . . 7 class (Base‘𝑢)
8078, 11, 79wsbc 3720 . . . . . 6 wff [(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd𝑥) = (0g𝑢), (0g𝑐), (𝑑 ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})))))
81 cdvh 38393 . . . . . . . 8 class DVecH
825, 81cfv 6325 . . . . . . 7 class (DVecH‘𝑘)
8362, 82cfv 6325 . . . . . 6 class ((DVecH‘𝑘)‘𝑤)
8480, 20, 83wsbc 3720 . . . . 5 wff [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd𝑥) = (0g𝑢), (0g𝑐), (𝑑 ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})))))
8584, 8cab 2776 . . . 4 class {𝑎[((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd𝑥) = (0g𝑢), (0g𝑐), (𝑑 ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})))))}
864, 7, 85cmpt 5111 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎[((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd𝑥) = (0g𝑢), (0g𝑐), (𝑑 ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})))))})
872, 3, 86cmpt 5111 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎[((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd𝑥) = (0g𝑢), (0g𝑐), (𝑑 ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})))))}))
881, 87wceq 1538 1 wff HDMap1 = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎[((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][(LSpan‘𝑢) / 𝑛][((LCDual‘𝑘)‘𝑤) / 𝑐][(Base‘𝑐) / 𝑑][(LSpan‘𝑐) / 𝑗][((mapd‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ if((2nd𝑥) = (0g𝑢), (0g𝑐), (𝑑 ((𝑚‘(𝑛‘{(2nd𝑥)})) = (𝑗‘{}) ∧ (𝑚‘(𝑛‘{((1st ‘(1st𝑥))(-g𝑢)(2nd𝑥))})) = (𝑗‘{((2nd ‘(1st𝑥))(-g𝑐))})))))}))
 Colors of variables: wff setvar class This definition is referenced by:  hdmap1ffval  39110
 Copyright terms: Public domain W3C validator