Step | Hyp | Ref
| Expression |
1 | | chg 40749 |
. 2
class
HGMap |
2 | | vk |
. . 3
setvar π |
3 | | cvv 3474 |
. . 3
class
V |
4 | | vw |
. . . 4
setvar π€ |
5 | 2 | cv 1540 |
. . . . 5
class π |
6 | | clh 38850 |
. . . . 5
class
LHyp |
7 | 5, 6 | cfv 6543 |
. . . 4
class
(LHypβπ) |
8 | | va |
. . . . . . . . . 10
setvar π |
9 | 8 | cv 1540 |
. . . . . . . . 9
class π |
10 | | vx |
. . . . . . . . . 10
setvar π₯ |
11 | | vb |
. . . . . . . . . . 11
setvar π |
12 | 11 | cv 1540 |
. . . . . . . . . 10
class π |
13 | 10 | cv 1540 |
. . . . . . . . . . . . . . 15
class π₯ |
14 | | vv |
. . . . . . . . . . . . . . . 16
setvar π£ |
15 | 14 | cv 1540 |
. . . . . . . . . . . . . . 15
class π£ |
16 | | vu |
. . . . . . . . . . . . . . . . 17
setvar π’ |
17 | 16 | cv 1540 |
. . . . . . . . . . . . . . . 16
class π’ |
18 | | cvsca 17200 |
. . . . . . . . . . . . . . . 16
class
Β·π |
19 | 17, 18 | cfv 6543 |
. . . . . . . . . . . . . . 15
class (
Β·π βπ’) |
20 | 13, 15, 19 | co 7408 |
. . . . . . . . . . . . . 14
class (π₯(
Β·π βπ’)π£) |
21 | | vm |
. . . . . . . . . . . . . . 15
setvar π |
22 | 21 | cv 1540 |
. . . . . . . . . . . . . 14
class π |
23 | 20, 22 | cfv 6543 |
. . . . . . . . . . . . 13
class (πβ(π₯( Β·π
βπ’)π£)) |
24 | | vy |
. . . . . . . . . . . . . . 15
setvar π¦ |
25 | 24 | cv 1540 |
. . . . . . . . . . . . . 14
class π¦ |
26 | 15, 22 | cfv 6543 |
. . . . . . . . . . . . . 14
class (πβπ£) |
27 | 4 | cv 1540 |
. . . . . . . . . . . . . . . 16
class π€ |
28 | | clcd 40452 |
. . . . . . . . . . . . . . . . 17
class
LCDual |
29 | 5, 28 | cfv 6543 |
. . . . . . . . . . . . . . . 16
class
(LCDualβπ) |
30 | 27, 29 | cfv 6543 |
. . . . . . . . . . . . . . 15
class
((LCDualβπ)βπ€) |
31 | 30, 18 | cfv 6543 |
. . . . . . . . . . . . . 14
class (
Β·π β((LCDualβπ)βπ€)) |
32 | 25, 26, 31 | co 7408 |
. . . . . . . . . . . . 13
class (π¦(
Β·π β((LCDualβπ)βπ€))(πβπ£)) |
33 | 23, 32 | wceq 1541 |
. . . . . . . . . . . 12
wff (πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£)) |
34 | | cbs 17143 |
. . . . . . . . . . . . 13
class
Base |
35 | 17, 34 | cfv 6543 |
. . . . . . . . . . . 12
class
(Baseβπ’) |
36 | 33, 14, 35 | wral 3061 |
. . . . . . . . . . 11
wff
βπ£ β
(Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£)) |
37 | 36, 24, 12 | crio 7363 |
. . . . . . . . . 10
class
(β©π¦
β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£))) |
38 | 10, 12, 37 | cmpt 5231 |
. . . . . . . . 9
class (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£)))) |
39 | 9, 38 | wcel 2106 |
. . . . . . . 8
wff π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£)))) |
40 | | chdma 40658 |
. . . . . . . . . 10
class
HDMap |
41 | 5, 40 | cfv 6543 |
. . . . . . . . 9
class
(HDMapβπ) |
42 | 27, 41 | cfv 6543 |
. . . . . . . 8
class
((HDMapβπ)βπ€) |
43 | 39, 21, 42 | wsbc 3777 |
. . . . . . 7
wff
[((HDMapβπ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£)))) |
44 | | csca 17199 |
. . . . . . . . 9
class
Scalar |
45 | 17, 44 | cfv 6543 |
. . . . . . . 8
class
(Scalarβπ’) |
46 | 45, 34 | cfv 6543 |
. . . . . . 7
class
(Baseβ(Scalarβπ’)) |
47 | 43, 11, 46 | wsbc 3777 |
. . . . . 6
wff
[(Baseβ(Scalarβπ’)) / π][((HDMapβπ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£)))) |
48 | | cdvh 39944 |
. . . . . . . 8
class
DVecH |
49 | 5, 48 | cfv 6543 |
. . . . . . 7
class
(DVecHβπ) |
50 | 27, 49 | cfv 6543 |
. . . . . 6
class
((DVecHβπ)βπ€) |
51 | 47, 16, 50 | wsbc 3777 |
. . . . 5
wff
[((DVecHβπ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£)))) |
52 | 51, 8 | cab 2709 |
. . . 4
class {π β£
[((DVecHβπ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£))))} |
53 | 4, 7, 52 | cmpt 5231 |
. . 3
class (π€ β (LHypβπ) β¦ {π β£ [((DVecHβπ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£))))}) |
54 | 2, 3, 53 | cmpt 5231 |
. 2
class (π β V β¦ (π€ β (LHypβπ) β¦ {π β£ [((DVecHβπ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£))))})) |
55 | 1, 54 | wceq 1541 |
1
wff HGMap =
(π β V β¦ (π€ β (LHypβπ) β¦ {π β£ [((DVecHβπ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£))))})) |