Detailed syntax breakdown of Definition df-ldual
Step | Hyp | Ref
| Expression |
1 | | cld 34410 |
. 2
LDual |
2 | | vv |
. . 3
|
3 | | cvv 3200 |
. . 3
|
4 | | cnx 15854 |
. . . . . . 7
|
5 | | cbs 15857 |
. . . . . . 7
|
6 | 4, 5 | cfv 5888 |
. . . . . 6
|
7 | 2 | cv 1482 |
. . . . . . 7
|
8 | | clfn 34344 |
. . . . . . 7
LFnl |
9 | 7, 8 | cfv 5888 |
. . . . . 6
LFnl |
10 | 6, 9 | cop 4183 |
. . . . 5
LFnl |
11 | | cplusg 15941 |
. . . . . . 7
|
12 | 4, 11 | cfv 5888 |
. . . . . 6
|
13 | | csca 15944 |
. . . . . . . . . 10
Scalar |
14 | 7, 13 | cfv 5888 |
. . . . . . . . 9
Scalar |
15 | 14, 11 | cfv 5888 |
. . . . . . . 8
Scalar |
16 | 15 | cof 6895 |
. . . . . . 7
Scalar |
17 | 9, 9 | cxp 5112 |
. . . . . . 7
LFnl LFnl |
18 | 16, 17 | cres 5116 |
. . . . . 6
Scalar LFnl LFnl |
19 | 12, 18 | cop 4183 |
. . . . 5
Scalar LFnl LFnl |
20 | 4, 13 | cfv 5888 |
. . . . . 6
Scalar |
21 | | coppr 18622 |
. . . . . . 7
oppr |
22 | 14, 21 | cfv 5888 |
. . . . . 6
opprScalar |
23 | 20, 22 | cop 4183 |
. . . . 5
Scalar opprScalar |
24 | 10, 19, 23 | ctp 4181 |
. . . 4
LFnl
Scalar LFnl LFnl Scalar opprScalar |
25 | | cvsca 15945 |
. . . . . . 7
|
26 | 4, 25 | cfv 5888 |
. . . . . 6
|
27 | | vk |
. . . . . . 7
|
28 | | vf |
. . . . . . 7
|
29 | 14, 5 | cfv 5888 |
. . . . . . 7
Scalar |
30 | 28 | cv 1482 |
. . . . . . . 8
|
31 | 7, 5 | cfv 5888 |
. . . . . . . . 9
|
32 | 27 | cv 1482 |
. . . . . . . . . 10
|
33 | 32 | csn 4177 |
. . . . . . . . 9
|
34 | 31, 33 | cxp 5112 |
. . . . . . . 8
|
35 | | cmulr 15942 |
. . . . . . . . . 10
|
36 | 14, 35 | cfv 5888 |
. . . . . . . . 9
Scalar |
37 | 36 | cof 6895 |
. . . . . . . 8
Scalar |
38 | 30, 34, 37 | co 6650 |
. . . . . . 7
Scalar |
39 | 27, 28, 29, 9, 38 | cmpt2 6652 |
. . . . . 6
Scalar LFnl Scalar |
40 | 26, 39 | cop 4183 |
. . . . 5
Scalar LFnl Scalar |
41 | 40 | csn 4177 |
. . . 4
Scalar LFnl Scalar |
42 | 24, 41 | cun 3572 |
. . 3
LFnl Scalar LFnl LFnl Scalar opprScalar Scalar LFnl Scalar |
43 | 2, 3, 42 | cmpt 4729 |
. 2
LFnl Scalar LFnl LFnl Scalar opprScalar Scalar LFnl Scalar |
44 | 1, 43 | wceq 1483 |
1
LDual
LFnl Scalar LFnl LFnl Scalar opprScalar Scalar LFnl Scalar |