Metamath Proof Explorer


Definition df-hdmap1

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

Ref Expression
Assertion df-hdmap1 HDMap1=kVwLHypka|[˙DVecHkw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch

Detailed syntax breakdown

Step Hyp Ref Expression
0 chdma1 classHDMap1
1 vk setvark
2 cvv classV
3 vw setvarw
4 clh classLHyp
5 1 cv setvark
6 5 4 cfv classLHypk
7 va setvara
8 cdvh classDVecH
9 5 8 cfv classDVecHk
10 3 cv setvarw
11 10 9 cfv classDVecHkw
12 vu setvaru
13 cbs classBase
14 12 cv setvaru
15 14 13 cfv classBaseu
16 vv setvarv
17 clspn classLSpan
18 14 17 cfv classLSpanu
19 vn setvarn
20 clcd classLCDual
21 5 20 cfv classLCDualk
22 10 21 cfv classLCDualkw
23 vc setvarc
24 23 cv setvarc
25 24 13 cfv classBasec
26 vd setvard
27 24 17 cfv classLSpanc
28 vj setvarj
29 cmpd classmapd
30 5 29 cfv classmapdk
31 10 30 cfv classmapdkw
32 vm setvarm
33 7 cv setvara
34 vx setvarx
35 16 cv setvarv
36 26 cv setvard
37 35 36 cxp classv×d
38 37 35 cxp classv×d×v
39 c2nd class2nd
40 34 cv setvarx
41 40 39 cfv class2ndx
42 c0g class0𝑔
43 14 42 cfv class0u
44 41 43 wceq wff2ndx=0u
45 24 42 cfv class0c
46 vh setvarh
47 32 cv setvarm
48 19 cv setvarn
49 41 csn class2ndx
50 49 48 cfv classn2ndx
51 50 47 cfv classmn2ndx
52 28 cv setvarj
53 46 cv setvarh
54 53 csn classh
55 54 52 cfv classjh
56 51 55 wceq wffmn2ndx=jh
57 c1st class1st
58 40 57 cfv class1stx
59 58 57 cfv class1st1stx
60 csg class-𝑔
61 14 60 cfv class-u
62 59 41 61 co class1st1stx-u2ndx
63 62 csn class1st1stx-u2ndx
64 63 48 cfv classn1st1stx-u2ndx
65 64 47 cfv classmn1st1stx-u2ndx
66 58 39 cfv class2nd1stx
67 24 60 cfv class-c
68 66 53 67 co class2nd1stx-ch
69 68 csn class2nd1stx-ch
70 69 52 cfv classj2nd1stx-ch
71 65 70 wceq wffmn1st1stx-u2ndx=j2nd1stx-ch
72 56 71 wa wffmn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
73 72 46 36 crio classιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
74 44 45 73 cif classif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
75 34 38 74 cmpt classxv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
76 33 75 wcel wffaxv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
77 76 32 31 wsbc wff[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
78 77 28 27 wsbc wff[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
79 78 26 25 wsbc wff[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
80 79 23 22 wsbc wff[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
81 80 19 18 wsbc wff[˙LSpanu/n]˙[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
82 81 16 15 wsbc wff[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
83 82 12 11 wsbc wff[˙DVecHkw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
84 83 7 cab classa|[˙DVecHkw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
85 3 6 84 cmpt classwLHypka|[˙DVecHkw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
86 1 2 85 cmpt classkVwLHypka|[˙DVecHkw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch
87 0 86 wceq wffHDMap1=kVwLHypka|[˙DVecHkw/u]˙[˙Baseu/v]˙[˙LSpanu/n]˙[˙LCDualkw/c]˙[˙Basec/d]˙[˙LSpanc/j]˙[˙mapdkw/m]˙axv×d×vif2ndx=0u0cιhd|mn2ndx=jhmn1st1stx-u2ndx=j2nd1stx-ch