Detailed syntax breakdown of Definition df-hvmap
Step | Hyp | Ref
| Expression |
1 | | chvm 39425 |
. 2
class
HVMap |
2 | | vk |
. . 3
setvar 𝑘 |
3 | | cvv 3400 |
. . 3
class
V |
4 | | vw |
. . . 4
setvar 𝑤 |
5 | 2 | cv 1541 |
. . . . 5
class 𝑘 |
6 | | clh 37653 |
. . . . 5
class
LHyp |
7 | 5, 6 | cfv 6349 |
. . . 4
class
(LHyp‘𝑘) |
8 | | vx |
. . . . 5
setvar 𝑥 |
9 | 4 | cv 1541 |
. . . . . . . 8
class 𝑤 |
10 | | cdvh 38747 |
. . . . . . . . 9
class
DVecH |
11 | 5, 10 | cfv 6349 |
. . . . . . . 8
class
(DVecH‘𝑘) |
12 | 9, 11 | cfv 6349 |
. . . . . . 7
class
((DVecH‘𝑘)‘𝑤) |
13 | | cbs 16598 |
. . . . . . 7
class
Base |
14 | 12, 13 | cfv 6349 |
. . . . . 6
class
(Base‘((DVecH‘𝑘)‘𝑤)) |
15 | | c0g 16828 |
. . . . . . . 8
class
0g |
16 | 12, 15 | cfv 6349 |
. . . . . . 7
class
(0g‘((DVecH‘𝑘)‘𝑤)) |
17 | 16 | csn 4526 |
. . . . . 6
class
{(0g‘((DVecH‘𝑘)‘𝑤))} |
18 | 14, 17 | cdif 3850 |
. . . . 5
class
((Base‘((DVecH‘𝑘)‘𝑤)) ∖
{(0g‘((DVecH‘𝑘)‘𝑤))}) |
19 | | vv |
. . . . . 6
setvar 𝑣 |
20 | 19 | cv 1541 |
. . . . . . . . 9
class 𝑣 |
21 | | vt |
. . . . . . . . . . 11
setvar 𝑡 |
22 | 21 | cv 1541 |
. . . . . . . . . 10
class 𝑡 |
23 | | vj |
. . . . . . . . . . . 12
setvar 𝑗 |
24 | 23 | cv 1541 |
. . . . . . . . . . 11
class 𝑗 |
25 | 8 | cv 1541 |
. . . . . . . . . . 11
class 𝑥 |
26 | | cvsca 16684 |
. . . . . . . . . . . 12
class
·𝑠 |
27 | 12, 26 | cfv 6349 |
. . . . . . . . . . 11
class (
·𝑠 ‘((DVecH‘𝑘)‘𝑤)) |
28 | 24, 25, 27 | co 7182 |
. . . . . . . . . 10
class (𝑗(
·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥) |
29 | | cplusg 16680 |
. . . . . . . . . . 11
class
+g |
30 | 12, 29 | cfv 6349 |
. . . . . . . . . 10
class
(+g‘((DVecH‘𝑘)‘𝑤)) |
31 | 22, 28, 30 | co 7182 |
. . . . . . . . 9
class (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝑘)‘𝑤))𝑥)) |
32 | 20, 31 | wceq 1542 |
. . . . . . . 8
wff 𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝑘)‘𝑤))𝑥)) |
33 | 25 | csn 4526 |
. . . . . . . . 9
class {𝑥} |
34 | | coch 39016 |
. . . . . . . . . . 11
class
ocH |
35 | 5, 34 | cfv 6349 |
. . . . . . . . . 10
class
(ocH‘𝑘) |
36 | 9, 35 | cfv 6349 |
. . . . . . . . 9
class
((ocH‘𝑘)‘𝑤) |
37 | 33, 36 | cfv 6349 |
. . . . . . . 8
class
(((ocH‘𝑘)‘𝑤)‘{𝑥}) |
38 | 32, 21, 37 | wrex 3055 |
. . . . . . 7
wff
∃𝑡 ∈
(((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝑘)‘𝑤))𝑥)) |
39 | | csca 16683 |
. . . . . . . . 9
class
Scalar |
40 | 12, 39 | cfv 6349 |
. . . . . . . 8
class
(Scalar‘((DVecH‘𝑘)‘𝑤)) |
41 | 40, 13 | cfv 6349 |
. . . . . . 7
class
(Base‘(Scalar‘((DVecH‘𝑘)‘𝑤))) |
42 | 38, 23, 41 | crio 7138 |
. . . . . 6
class
(℩𝑗
∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝑘)‘𝑤))𝑥))) |
43 | 19, 14, 42 | cmpt 5120 |
. . . . 5
class (𝑣 ∈
(Base‘((DVecH‘𝑘)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝑘)‘𝑤))𝑥)))) |
44 | 8, 18, 43 | cmpt 5120 |
. . . 4
class (𝑥 ∈
((Base‘((DVecH‘𝑘)‘𝑤)) ∖
{(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝑘)‘𝑤))𝑥))))) |
45 | 4, 7, 44 | cmpt 5120 |
. . 3
class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖
{(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝑘)‘𝑤))𝑥)))))) |
46 | 2, 3, 45 | cmpt 5120 |
. 2
class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖
{(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝑘)‘𝑤))𝑥))))))) |
47 | 1, 46 | wceq 1542 |
1
wff HVMap =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖
{(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝑘)‘𝑤))𝑥))))))) |