Step | Hyp | Ref
| Expression |
1 | | ldualset.w |
. 2
   |
2 | | elex 3065 |
. 2
   |
3 | | ldualset.d |
. . 3
LDual   |
4 | | fveq2 5887 |
. . . . . . . 8
 LFnl  LFnl    |
5 | | ldualset.f |
. . . . . . . 8
LFnl   |
6 | 4, 5 | syl6eqr 2513 |
. . . . . . 7
 LFnl    |
7 | 6 | opeq2d 4186 |
. . . . . 6
       LFnl        
   |
8 | | fveq2 5887 |
. . . . . . . . . . . . 13
 Scalar  Scalar    |
9 | | ldualset.r |
. . . . . . . . . . . . 13
Scalar   |
10 | 8, 9 | syl6eqr 2513 |
. . . . . . . . . . . 12
 Scalar    |
11 | 10 | fveq2d 5891 |
. . . . . . . . . . 11
   Scalar        |
12 | | ldualset.a |
. . . . . . . . . . 11
    |
13 | 11, 12 | syl6eqr 2513 |
. . . . . . . . . 10
   Scalar    |
14 | | ofeq 6559 |
. . . . . . . . . 10
   Scalar       Scalar     |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
     Scalar     |
16 | 6 | sqxpeqd 4878 |
. . . . . . . . 9
  LFnl  LFnl       |
17 | 15, 16 | reseq12d 5124 |
. . . . . . . 8
     Scalar    LFnl  LFnl    
     |
18 | | ldualset.p |
. . . . . . . 8
     |
19 | 17, 18 | syl6eqr 2513 |
. . . . . . 7
     Scalar    LFnl  LFnl   
 |
20 | 19 | opeq2d 4186 |
. . . . . 6
          Scalar    LFnl  LFnl            |
21 | 10 | fveq2d 5891 |
. . . . . . . 8
 oppr Scalar   oppr    |
22 | | ldualset.o |
. . . . . . . 8
oppr   |
23 | 21, 22 | syl6eqr 2513 |
. . . . . . 7
 oppr Scalar     |
24 | 23 | opeq2d 4186 |
. . . . . 6
  Scalar   oppr Scalar   
 Scalar      |
25 | 7, 20, 24 | tpeq123d 4078 |
. . . . 5
        LFnl        
    Scalar    LFnl  LFnl       Scalar   oppr Scalar                     Scalar       |
26 | 10 | fveq2d 5891 |
. . . . . . . . . 10
    Scalar         |
27 | | ldualset.k |
. . . . . . . . . 10
     |
28 | 26, 27 | syl6eqr 2513 |
. . . . . . . . 9
    Scalar     |
29 | 10 | fveq2d 5891 |
. . . . . . . . . . . 12
    Scalar         |
30 | | ldualset.t |
. . . . . . . . . . . 12
     |
31 | 29, 30 | syl6eqr 2513 |
. . . . . . . . . . 11
    Scalar    |
32 | | ofeq 6559 |
. . . . . . . . . . 11
    Scalar        Scalar     |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
      Scalar     |
34 | | eqidd 2462 |
. . . . . . . . . 10
   |
35 | | fveq2 5887 |
. . . . . . . . . . . 12
           |
36 | | ldualset.v |
. . . . . . . . . . . 12
     |
37 | 35, 36 | syl6eqr 2513 |
. . . . . . . . . . 11
       |
38 | 37 | xpeq1d 4875 |
. . . . . . . . . 10
               |
39 | 33, 34, 38 | oveq123d 6335 |
. . . . . . . . 9
       Scalar                      |
40 | 28, 6, 39 | mpt2eq123dv 6379 |
. . . . . . . 8
     Scalar    LFnl        Scalar                          |
41 | | ldualset.s |
. . . . . . . 8
 
         |
42 | 40, 41 | syl6eqr 2513 |
. . . . . . 7
     Scalar    LFnl        Scalar             
 |
43 | 42 | opeq2d 4186 |
. . . . . 6
           Scalar    LFnl        Scalar              
        |
44 | 43 | sneqd 3991 |
. . . . 5
            Scalar    LFnl        Scalar                      
   |
45 | 25, 44 | uneq12d 3600 |
. . . 4
        
LFnl             Scalar    LFnl  LFnl       Scalar   oppr Scalar                Scalar    LFnl        Scalar                                  Scalar                |
46 | | df-ldual 32734 |
. . . 4
LDual         
LFnl             Scalar    LFnl  LFnl       Scalar   oppr Scalar                Scalar    LFnl        Scalar                   |
47 | | tpex 6616 |
. . . . 5
                Scalar      |
48 | | snex 4654 |
. . . . 5
         |
49 | 47, 48 | unex 6615 |
. . . 4
       
      
  Scalar               |
50 | 45, 46, 49 | fvmpt 5970 |
. . 3
 LDual         
      
  Scalar                |
51 | 3, 50 | syl5eq 2507 |
. 2
                  Scalar                |
52 | 1, 2, 51 | 3syl 18 |
1
        
      
  Scalar                |