Step | Hyp | Ref
| Expression |
1 | | elex 3066 |
. 2
   |
2 | | oveq12 6324 |
. . . . . . 7
 
  LMHom   LMHom    |
3 | 2 | anidms 655 |
. . . . . 6
  LMHom   LMHom    |
4 | | mendval.b |
. . . . . 6
 LMHom   |
5 | 3, 4 | syl6eqr 2514 |
. . . . 5
  LMHom    |
6 | 5 | csbeq1d 3382 |
. . . 4
   LMHom   ![]_ ]_](_urbrack.gif)                            
               Scalar   Scalar              Scalar                           ![]_ ]_](_urbrack.gif)        
      
            
               Scalar   Scalar              Scalar                           |
7 | | ovex 6343 |
. . . . . 6
 LMHom   |
8 | 5, 7 | syl6eqelr 2549 |
. . . . 5
   |
9 | | simpr 467 |
. . . . . . . 8
 
   |
10 | 9 | opeq2d 4187 |
. . . . . . 7
 
      
      
   |
11 | | fveq2 5888 |
. . . . . . . . . . . 12
         |
12 | | ofeq 6560 |
. . . . . . . . . . . 12
      
  
         |
13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
             |
14 | 13 | oveqdr 6339 |
. . . . . . . . . 10
 
                   |
15 | 9, 9, 14 | mpt2eq123dv 6380 |
. . . . . . . . 9
 
                         |
16 | | mendval.p |
. . . . . . . . 9


          |
17 | 15, 16 | syl6eqr 2514 |
. . . . . . . 8
 
             |
18 | 17 | opeq2d 4187 |
. . . . . . 7
 
     
           
       |
19 | | eqidd 2463 |
. . . . . . . . . 10
 
       |
20 | 9, 9, 19 | mpt2eq123dv 6380 |
. . . . . . . . 9
 
             |
21 | | mendval.t |
. . . . . . . . 9


    |
22 | 20, 21 | syl6eqr 2514 |
. . . . . . . 8
 
       |
23 | 22 | opeq2d 4187 |
. . . . . . 7
 
      
              |
24 | 10, 18, 23 | tpeq123d 4079 |
. . . . . 6
 
       
      
            
                   
      
          |
25 | | fveq2 5888 |
. . . . . . . . . 10
 Scalar  Scalar    |
26 | 25 | adantr 471 |
. . . . . . . . 9
 
 Scalar  Scalar    |
27 | | mendval.s |
. . . . . . . . 9
Scalar   |
28 | 26, 27 | syl6eqr 2514 |
. . . . . . . 8
 
 Scalar    |
29 | 28 | opeq2d 4187 |
. . . . . . 7
 
  Scalar   Scalar    Scalar  
   |
30 | 28 | fveq2d 5892 |
. . . . . . . . . 10
 
    Scalar         |
31 | | fveq2 5888 |
. . . . . . . . . . . . 13
           |
32 | 31 | adantr 471 |
. . . . . . . . . . . 12
 
           |
33 | | ofeq 6560 |
. . . . . . . . . . . 12
                       |
34 | 32, 33 | syl 17 |
. . . . . . . . . . 11
 
               |
35 | | fveq2 5888 |
. . . . . . . . . . . . 13
           |
36 | 35 | adantr 471 |
. . . . . . . . . . . 12
 
           |
37 | 36 | xpeq1d 4876 |
. . . . . . . . . . 11
 
                   |
38 | | eqidd 2463 |
. . . . . . . . . . 11
 
   |
39 | 34, 37, 38 | oveq123d 6336 |
. . . . . . . . . 10
 
                                     |
40 | 30, 9, 39 | mpt2eq123dv 6380 |
. . . . . . . . 9
 
     Scalar                                                |
41 | | mendval.v |
. . . . . . . . 9

                        |
42 | 40, 41 | syl6eqr 2514 |
. . . . . . . 8
 
     Scalar                       |
43 | 42 | opeq2d 4187 |
. . . . . . 7
 
      
    Scalar                      
        |
44 | 29, 43 | preq12d 4072 |
. . . . . 6
 
   Scalar  
Scalar              Scalar                          Scalar              |
45 | 24, 44 | uneq12d 3601 |
. . . . 5
 
                            
               Scalar   Scalar              Scalar                                
      
          Scalar               |
46 | 8, 45 | csbied 3402 |
. . . 4
   ![]_ ]_](_urbrack.gif)        
      
            
               Scalar   Scalar              Scalar                                
      
          Scalar               |
47 | 6, 46 | eqtrd 2496 |
. . 3
   LMHom   ![]_ ]_](_urbrack.gif)                            
               Scalar   Scalar              Scalar                                
      
          Scalar               |
48 | | df-mend 36087 |
. . 3
MEndo   
LMHom   ![]_ ]_](_urbrack.gif)        
      
            
               Scalar   Scalar              Scalar                           |
49 | | tpex 6617 |
. . . 4
                       |
50 | | prex 4656 |
. . . 4
  Scalar             |
51 | 49, 50 | unex 6616 |
. . 3
       
      
          Scalar              |
52 | 47, 48, 51 | fvmpt 5971 |
. 2
 MEndo         
      
          Scalar               |
53 | 1, 52 | syl 17 |
1
 MEndo         
      
          Scalar               |