Step | Hyp | Ref
| Expression |
1 | | psrval.s |
. 2
 mPwSer   |
2 | | df-psr 18635 |
. . . 4
mPwSer    
      
  ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)                                    g   
                         
  Scalar    
                           
 TopSet                    |
3 | 2 | a1i 11 |
. . 3
 mPwSer              ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)                                    g   
                         
  Scalar    
                           
 TopSet                     |
4 | | simprl 769 |
. . . . . . . 8
 

    |
5 | 4 | oveq2d 6336 |
. . . . . . 7
 

  
     |
6 | | rabeq 3050 |
. . . . . . 7
              
      
   |
7 | 5, 6 | syl 17 |
. . . . . 6
 

  
      
            |
8 | | psrval.d |
. . . . . 6
          |
9 | 7, 8 | syl6eqr 2514 |
. . . . 5
 

  
      
   |
10 | 9 | csbeq1d 3382 |
. . . 4
 

             ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)                                    g   
                         
  Scalar    
                           
 TopSet                    ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)                                    g   
                         
  Scalar    
                           
 TopSet                    |
11 | | ovex 6348 |
. . . . . . 7
   |
12 | 11 | rabex 4571 |
. . . . . 6
          |
13 | 9, 12 | syl6eqelr 2549 |
. . . . 5
 

 
  |
14 | | simplrr 776 |
. . . . . . . . . . 11
   
 
   |
15 | 14 | fveq2d 5896 |
. . . . . . . . . 10
   
 
           |
16 | | psrval.k |
. . . . . . . . . 10
     |
17 | 15, 16 | syl6eqr 2514 |
. . . . . . . . 9
   
 
       |
18 | | simpr 467 |
. . . . . . . . 9
   
 
   |
19 | 17, 18 | oveq12d 6338 |
. . . . . . . 8
   
 
           |
20 | | psrval.b |
. . . . . . . . 9
     |
21 | 20 | ad2antrr 737 |
. . . . . . . 8
   
 
     |
22 | 19, 21 | eqtr4d 2499 |
. . . . . . 7
   
 
         |
23 | 22 | csbeq1d 3382 |
. . . . . 6
   
 
         ![]_ ]_](_urbrack.gif)                                    g   
                         
  Scalar    
                           
 TopSet                    ![]_ ]_](_urbrack.gif)        
      
                    g 
                              Scalar    
                           
 TopSet                    |
24 | | ovex 6348 |
. . . . . . . 8
       |
25 | 22, 24 | syl6eqelr 2549 |
. . . . . . 7
   
 
   |
26 | | simpr 467 |
. . . . . . . . . 10
           |
27 | 26 | opeq2d 4187 |
. . . . . . . . 9
               
         |
28 | 14 | adantr 471 |
. . . . . . . . . . . . . . 15
           |
29 | 28 | fveq2d 5896 |
. . . . . . . . . . . . . 14
                 |
30 | | psrval.a |
. . . . . . . . . . . . . 14
    |
31 | 29, 30 | syl6eqr 2514 |
. . . . . . . . . . . . 13
             |
32 | | ofeq 6565 |
. . . . . . . . . . . . 13
           |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . 12
                |
34 | 26, 26 | xpeq12d 4881 |
. . . . . . . . . . . 12
               |
35 | 33, 34 | reseq12d 5128 |
. . . . . . . . . . 11
                       |
36 | | psrval.p |
. . . . . . . . . . 11
     |
37 | 35, 36 | syl6eqr 2514 |
. . . . . . . . . 10
                  |
38 | 37 | opeq2d 4187 |
. . . . . . . . 9
                              |
39 | 18 | adantr 471 |
. . . . . . . . . . . . 13
           |
40 | | rabeq 3050 |
. . . . . . . . . . . . . . . 16
   


   |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . 15
           


   |
42 | 28 | fveq2d 5896 |
. . . . . . . . . . . . . . . . 17
                   |
43 | | psrval.m |
. . . . . . . . . . . . . . . . 17
     |
44 | 42, 43 | syl6eqr 2514 |
. . . . . . . . . . . . . . . 16
              |
45 | 44 | oveqd 6337 |
. . . . . . . . . . . . . . 15
                                
          |
46 | 41, 45 | mpteq12dv 4497 |
. . . . . . . . . . . . . 14
                                   
          
      |
47 | 28, 46 | oveq12d 6338 |
. . . . . . . . . . . . 13
          g                           g                      |
48 | 39, 47 | mpteq12dv 4497 |
. . . . . . . . . . . 12
           g                             g   
          
        |
49 | 26, 26, 48 | mpt2eq123dv 6385 |
. . . . . . . . . . 11
             g                                g 
                      |
50 | | psrval.t |
. . . . . . . . . . 11
 
  g                       |
51 | 49, 50 | syl6eqr 2514 |
. . . . . . . . . 10
             g                             |
52 | 51 | opeq2d 4187 |
. . . . . . . . 9
                   g                            
        |
53 | 27, 38, 52 | tpeq123d 4079 |
. . . . . . . 8
                                           g   
                         
                        |
54 | 28 | opeq2d 4187 |
. . . . . . . . 9
          Scalar   
 Scalar      |
55 | 17 | adantr 471 |
. . . . . . . . . . . 12
               |
56 | | ofeq 6565 |
. . . . . . . . . . . . . 14
             |
57 | 44, 56 | syl 17 |
. . . . . . . . . . . . 13
                 |
58 | 39 | xpeq1d 4879 |
. . . . . . . . . . . . 13
                   |
59 | | eqidd 2463 |
. . . . . . . . . . . . 13
           |
60 | 57, 58, 59 | oveq123d 6341 |
. . . . . . . . . . . 12
                               |
61 | 55, 26, 60 | mpt2eq123dv 6385 |
. . . . . . . . . . 11
                                         |
62 | | psrval.v |
. . . . . . . . . . 11


         |
63 | 61, 62 | syl6eqr 2514 |
. . . . . . . . . 10
                            
 |
64 | 63 | opeq2d 4187 |
. . . . . . . . 9
                    
                       |
65 | 28 | fveq2d 5896 |
. . . . . . . . . . . . . . 15
                   |
66 | | psrval.o |
. . . . . . . . . . . . . . 15
     |
67 | 65, 66 | syl6eqr 2514 |
. . . . . . . . . . . . . 14
               |
68 | 67 | sneqd 3992 |
. . . . . . . . . . . . 13
                   |
69 | 39, 68 | xpeq12d 4881 |
. . . . . . . . . . . 12
                       |
70 | 69 | fveq2d 5896 |
. . . . . . . . . . 11
                               |
71 | | psrval.j |
. . . . . . . . . . . 12
           |
72 | 71 | ad3antrrr 741 |
. . . . . . . . . . 11
                   |
73 | 70, 72 | eqtr4d 2499 |
. . . . . . . . . 10
                       |
74 | 73 | opeq2d 4187 |
. . . . . . . . 9
          TopSet               
 TopSet      |
75 | 54, 64, 74 | tpeq123d 4079 |
. . . . . . . 8
           Scalar    
                           
 TopSet                
  Scalar             TopSet       |
76 | 53, 75 | uneq12d 3601 |
. . . . . . 7
                
      
                    g 
                              Scalar    
                           
 TopSet                         
      
          Scalar             TopSet        |
77 | 25, 76 | csbied 3402 |
. . . . . 6
   
 
   ![]_ ]_](_urbrack.gif)        
      
                    g 
                              Scalar    
                           
 TopSet                         
      
          Scalar             TopSet        |
78 | 23, 77 | eqtrd 2496 |
. . . . 5
   
 
         ![]_ ]_](_urbrack.gif)                                    g   
                         
  Scalar    
                           
 TopSet                         
      
          Scalar             TopSet        |
79 | 13, 78 | csbied 3402 |
. . . 4
 

  
 ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)        
      
                    g 
                              Scalar    
                           
 TopSet                         
      
          Scalar             TopSet        |
80 | 10, 79 | eqtrd 2496 |
. . 3
 

             ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)                                    g   
                         
  Scalar    
                           
 TopSet                         
      
          Scalar             TopSet        |
81 | | psrval.i |
. . . 4
   |
82 | | elex 3066 |
. . . 4
   |
83 | 81, 82 | syl 17 |
. . 3
   |
84 | | psrval.r |
. . . 4
   |
85 | | elex 3066 |
. . . 4
   |
86 | 84, 85 | syl 17 |
. . 3
   |
87 | | tpex 6622 |
. . . . 5
                       |
88 | | tpex 6622 |
. . . . 5
  Scalar             TopSet      |
89 | 87, 88 | unex 6621 |
. . . 4
       
      
          Scalar             TopSet       |
90 | 89 | a1i 11 |
. . 3
                          Scalar             TopSet        |
91 | 3, 80, 83, 86, 90 | ovmpt2d 6456 |
. 2
  mPwSer                           Scalar             TopSet        |
92 | 1, 91 | syl5eq 2508 |
1
        
      
          Scalar             TopSet        |