Detailed syntax breakdown of Definition df-lkr
Step | Hyp | Ref
| Expression |
1 | | clk 37078 |
. 2
class
LKer |
2 | | vw |
. . 3
setvar 𝑤 |
3 | | cvv 3430 |
. . 3
class
V |
4 | | vf |
. . . 4
setvar 𝑓 |
5 | 2 | cv 1540 |
. . . . 5
class 𝑤 |
6 | | clfn 37050 |
. . . . 5
class
LFnl |
7 | 5, 6 | cfv 6430 |
. . . 4
class
(LFnl‘𝑤) |
8 | 4 | cv 1540 |
. . . . . 6
class 𝑓 |
9 | 8 | ccnv 5587 |
. . . . 5
class ◡𝑓 |
10 | | csca 16946 |
. . . . . . . 8
class
Scalar |
11 | 5, 10 | cfv 6430 |
. . . . . . 7
class
(Scalar‘𝑤) |
12 | | c0g 17131 |
. . . . . . 7
class
0g |
13 | 11, 12 | cfv 6430 |
. . . . . 6
class
(0g‘(Scalar‘𝑤)) |
14 | 13 | csn 4566 |
. . . . 5
class
{(0g‘(Scalar‘𝑤))} |
15 | 9, 14 | cima 5591 |
. . . 4
class (◡𝑓 “
{(0g‘(Scalar‘𝑤))}) |
16 | 4, 7, 15 | cmpt 5161 |
. . 3
class (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “
{(0g‘(Scalar‘𝑤))})) |
17 | 2, 3, 16 | cmpt 5161 |
. 2
class (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “
{(0g‘(Scalar‘𝑤))}))) |
18 | 1, 17 | wceq 1541 |
1
wff LKer =
(𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “
{(0g‘(Scalar‘𝑤))}))) |