Detailed syntax breakdown of Definition df-ldual
Step | Hyp | Ref
| Expression |
1 | | cld 32760 |
. 2
LDual |
2 | | vv |
. . 3
 |
3 | | cvv 3031 |
. . 3
 |
4 | | cnx 15196 |
. . . . . . 7
 |
5 | | cbs 15199 |
. . . . . . 7
 |
6 | 4, 5 | cfv 5589 |
. . . . . 6
     |
7 | 2 | cv 1451 |
. . . . . . 7
 |
8 | | clfn 32694 |
. . . . . . 7
LFnl |
9 | 7, 8 | cfv 5589 |
. . . . . 6
LFnl   |
10 | 6, 9 | cop 3965 |
. . . . 5
      LFnl    |
11 | | cplusg 15268 |
. . . . . . 7
 |
12 | 4, 11 | cfv 5589 |
. . . . . 6
    |
13 | | csca 15271 |
. . . . . . . . . 10
Scalar |
14 | 7, 13 | cfv 5589 |
. . . . . . . . 9
Scalar   |
15 | 14, 11 | cfv 5589 |
. . . . . . . 8
  Scalar    |
16 | 15 | cof 6548 |
. . . . . . 7
    Scalar    |
17 | 9, 9 | cxp 4837 |
. . . . . . 7
 LFnl  LFnl    |
18 | 16, 17 | cres 4841 |
. . . . . 6
    Scalar    LFnl  LFnl     |
19 | 12, 18 | cop 3965 |
. . . . 5
         Scalar    LFnl  LFnl      |
20 | 4, 13 | cfv 5589 |
. . . . . 6
Scalar   |
21 | | coppr 17928 |
. . . . . . 7
oppr |
22 | 14, 21 | cfv 5589 |
. . . . . 6
oppr Scalar    |
23 | 20, 22 | cop 3965 |
. . . . 5
 Scalar   oppr Scalar     |
24 | 10, 19, 23 | ctp 3963 |
. . . 4
       LFnl        
    Scalar    LFnl  LFnl       Scalar   oppr Scalar      |
25 | | cvsca 15272 |
. . . . . . 7
 |
26 | 4, 25 | cfv 5589 |
. . . . . 6
     |
27 | | vk |
. . . . . . 7
 |
28 | | vf |
. . . . . . 7
 |
29 | 14, 5 | cfv 5589 |
. . . . . . 7
   Scalar    |
30 | 28 | cv 1451 |
. . . . . . . 8
 |
31 | 7, 5 | cfv 5589 |
. . . . . . . . 9
     |
32 | 27 | cv 1451 |
. . . . . . . . . 10
 |
33 | 32 | csn 3959 |
. . . . . . . . 9
   |
34 | 31, 33 | cxp 4837 |
. . . . . . . 8
         |
35 | | cmulr 15269 |
. . . . . . . . . 10
 |
36 | 14, 35 | cfv 5589 |
. . . . . . . . 9
   Scalar    |
37 | 36 | cof 6548 |
. . . . . . . 8
     Scalar    |
38 | 30, 34, 37 | co 6308 |
. . . . . . 7
      Scalar              |
39 | 27, 28, 29, 9, 38 | cmpt2 6310 |
. . . . . 6
    Scalar    LFnl        Scalar               |
40 | 26, 39 | cop 3965 |
. . . . 5
          Scalar    LFnl        Scalar                |
41 | 40 | csn 3959 |
. . . 4
           Scalar    LFnl        Scalar                 |
42 | 24, 41 | cun 3388 |
. . 3
       
LFnl             Scalar    LFnl  LFnl       Scalar   oppr Scalar                Scalar    LFnl        Scalar                  |
43 | 2, 3, 42 | cmpt 4454 |
. 2
        
LFnl             Scalar    LFnl  LFnl       Scalar   oppr Scalar                Scalar    LFnl        Scalar                   |
44 | 1, 43 | wceq 1452 |
1
LDual         
LFnl             Scalar    LFnl  LFnl       Scalar   oppr Scalar                Scalar    LFnl        Scalar                   |