Proof of Theorem ovolshftlem1
Step | Hyp | Ref
| Expression |
1 | | ovolshft.7 |
. . . . . . . . . . . . . 14
          |
2 | | ovolfcl 22412 |
. . . . . . . . . . . . . 14
                                              |
3 | 1, 2 | sylan 474 |
. . . . . . . . . . . . 13
 

                                    |
4 | 3 | simp1d 1019 |
. . . . . . . . . . . 12
 

          |
5 | 3 | simp2d 1020 |
. . . . . . . . . . . 12
 

          |
6 | | ovolshft.2 |
. . . . . . . . . . . . 13
   |
7 | 6 | adantr 467 |
. . . . . . . . . . . 12
 

  |
8 | 3 | simp3d 1021 |
. . . . . . . . . . . 12
 

                  |
9 | 4, 5, 7, 8 | leadd1dd 10224 |
. . . . . . . . . . 11
 

                      |
10 | | df-br 4402 |
. . . . . . . . . . 11
                                             |
11 | 9, 10 | sylib 200 |
. . . . . . . . . 10
 

                        |
12 | 4, 7 | readdcld 9667 |
. . . . . . . . . . 11
 

            |
13 | 5, 7 | readdcld 9667 |
. . . . . . . . . . 11
 

            |
14 | | opelxp 4863 |
. . . . . . . . . . 11
                         
                        |
15 | 12, 13, 14 | sylanbrc 669 |
. . . . . . . . . 10
 

                           |
16 | 11, 15 | elind 3617 |
. . . . . . . . 9
 

                            |
17 | | ovolshft.6 |
. . . . . . . . 9
                          |
18 | 16, 17 | fmptd 6044 |
. . . . . . . 8
          |
19 | | eqid 2450 |
. . . . . . . . 9
    
  |
20 | 19 | ovolfsf 22417 |
. . . . . . . 8
         
          |
21 | | ffn 5726 |
. . . . . . . 8
  
       
     |
22 | 18, 20, 21 | 3syl 18 |
. . . . . . 7
  
   |
23 | | eqid 2450 |
. . . . . . . . 9
    
  |
24 | 23 | ovolfsf 22417 |
. . . . . . . 8
         
          |
25 | | ffn 5726 |
. . . . . . . 8
  
       
     |
26 | 1, 24, 25 | 3syl 18 |
. . . . . . 7
  
   |
27 | | opex 4663 |
. . . . . . . . . . . . . 14
                        |
28 | 17 | fvmpt2 5955 |
. . . . . . . . . . . . . 14
                                                       |
29 | 27, 28 | mpan2 676 |
. . . . . . . . . . . . 13
                              |
30 | 29 | fveq2d 5867 |
. . . . . . . . . . . 12
                                      |
31 | | ovex 6316 |
. . . . . . . . . . . . 13
           |
32 | | ovex 6316 |
. . . . . . . . . . . . 13
           |
33 | 31, 32 | op2nd 6799 |
. . . . . . . . . . . 12
                                      |
34 | 30, 33 | syl6eq 2500 |
. . . . . . . . . . 11
                     |
35 | 29 | fveq2d 5867 |
. . . . . . . . . . . 12
                                      |
36 | 31, 32 | op1st 6798 |
. . . . . . . . . . . 12
                                      |
37 | 35, 36 | syl6eq 2500 |
. . . . . . . . . . 11
                     |
38 | 34, 37 | oveq12d 6306 |
. . . . . . . . . 10
                                           |
39 | 38 | adantl 468 |
. . . . . . . . 9
 

                                          |
40 | 5 | recnd 9666 |
. . . . . . . . . 10
 

          |
41 | 4 | recnd 9666 |
. . . . . . . . . 10
 

          |
42 | 7 | recnd 9666 |
. . . . . . . . . 10
 

  |
43 | 40, 41, 42 | pnpcan2d 10021 |
. . . . . . . . 9
 

                                          |
44 | 39, 43 | eqtrd 2484 |
. . . . . . . 8
 

                                      |
45 | 19 | ovolfsval 22416 |
. . . . . . . . 9
            
                        |
46 | 18, 45 | sylan 474 |
. . . . . . . 8
 

  
                        |
47 | 23 | ovolfsval 22416 |
. . . . . . . . 9
            
                        |
48 | 1, 47 | sylan 474 |
. . . . . . . 8
 

  
                        |
49 | 44, 46, 48 | 3eqtr4d 2494 |
. . . . . . 7
 

  
      
      |
50 | 22, 26, 49 | eqfnfvd 5977 |
. . . . . 6
  
      |
51 | 50 | seqeq3d 12218 |
. . . . 5
    
     
    |
52 | | ovolshft.5 |
. . . . 5
   
   |
53 | 51, 52 | syl6eqr 2502 |
. . . 4
    
    |
54 | 53 | rneqd 5061 |
. . 3
         |
55 | 54 | supeq1d 7957 |
. 2
      
          |
56 | | ovolshft.3 |
. . . . . . . . 9
       |
57 | 56 | eleq2d 2513 |
. . . . . . . 8
         |
58 | | oveq1 6295 |
. . . . . . . . . 10
       |
59 | 58 | eleq1d 2512 |
. . . . . . . . 9
   
     |
60 | 59 | elrab 3195 |
. . . . . . . 8
    
      |
61 | 57, 60 | syl6bb 265 |
. . . . . . 7
         |
62 | 61 | biimpa 487 |
. . . . . 6
 
       |
63 | | simprr 765 |
. . . . . . . 8
 
         |
64 | | ovolshft.8 |
. . . . . . . . . 10

     |
65 | | ovolshft.1 |
. . . . . . . . . . 11

  |
66 | | ovolfioo 22413 |
. . . . . . . . . . 11
 
    
       

        
            |
67 | 65, 1, 66 | syl2anc 666 |
. . . . . . . . . 10
     

        
            |
68 | 64, 67 | mpbid 214 |
. . . . . . . . 9
  
        
           |
69 | 68 | adantr 467 |
. . . . . . . 8
 
     

        
           |
70 | | breq2 4405 |
. . . . . . . . . . 11
           
             |
71 | | breq1 4404 |
. . . . . . . . . . 11
   
       
             |
72 | 70, 71 | anbi12d 716 |
. . . . . . . . . 10
            
        
          
              |
73 | 72 | rexbidv 2900 |
. . . . . . . . 9
    
        
        
                          |
74 | 73 | rspcv 3145 |
. . . . . . . 8
    

        
                                   |
75 | 63, 69, 74 | sylc 62 |
. . . . . . 7
 
     
        
               |
76 | 37 | adantl 468 |
. . . . . . . . . . 11
                             |
77 | 76 | breq1d 4411 |
. . . . . . . . . 10
                 
             |
78 | 4 | adantlr 720 |
. . . . . . . . . . 11
                   |
79 | 6 | ad2antrr 731 |
. . . . . . . . . . 11
           |
80 | | simplrl 769 |
. . . . . . . . . . 11
           |
81 | 78, 79, 80 | ltaddsubd 10210 |
. . . . . . . . . 10
                   
             |
82 | 77, 81 | bitrd 257 |
. . . . . . . . 9
                 
             |
83 | 34 | adantl 468 |
. . . . . . . . . . 11
                             |
84 | 83 | breq2d 4413 |
. . . . . . . . . 10
         
       
             |
85 | 5 | adantlr 720 |
. . . . . . . . . . 11
                   |
86 | 80, 79, 85 | ltsubaddd 10206 |
. . . . . . . . . 10
           
       
             |
87 | 84, 86 | bitr4d 260 |
. . . . . . . . 9
         
       
             |
88 | 82, 87 | anbi12d 716 |
. . . . . . . 8
                  
        
          
              |
89 | 88 | rexbidva 2897 |
. . . . . . 7
 
               
        
                          |
90 | 75, 89 | mpbird 236 |
. . . . . 6
 
     
        
           |
91 | 62, 90 | syldan 473 |
. . . . 5
 
          
           |
92 | 91 | ralrimiva 2801 |
. . . 4
  
        
           |
93 | | ssrab2 3513 |
. . . . . 6
     |
94 | 56, 93 | syl6eqss 3481 |
. . . . 5

  |
95 | | ovolfioo 22413 |
. . . . 5
 
    
       

        
            |
96 | 94, 18, 95 | syl2anc 666 |
. . . 4
     

        
            |
97 | 92, 96 | mpbird 236 |
. . 3

     |
98 | | ovolshft.4 |
. . . 4
  
     
  
     
   
   |
99 | | eqid 2450 |
. . . 4
   
     
   |
100 | 98, 99 | elovolmr 22422 |
. . 3
         
        
      |
101 | 18, 97, 100 | syl2anc 666 |
. 2
      
      |
102 | 55, 101 | eqeltrrd 2529 |
1
       |