Step | Hyp | Ref
| Expression |
1 | | psrbag.d |
. . . 4
          |
2 | | psrbagconf1o.1 |
. . . 4

   |
3 | | gsumbagdiag.i |
. . . 4
   |
4 | | gsumbagdiag.f |
. . . 4
   |
5 | | gsumbagdiag.b |
. . . 4
     |
6 | | gsumbagdiag.g |
. . . 4
 CMnd |
7 | 1, 2, 3, 4 | gsumbagdiaglem 18611 |
. . . . 5
 


       


       |
8 | | gsumbagdiag.x |
. . . . . . . . . . . 12
 


         |
9 | 8 | anassrs 654 |
. . . . . . . . . . 11
    
     
  |
10 | | eqid 2453 |
. . . . . . . . . . 11
  
 
    
       |
11 | 9, 10 | fmptd 6051 |
. . . . . . . . . 10
 
  

        
 
      |
12 | 3 | adantr 467 |
. . . . . . . . . . . 12
 
   |
13 | | ssrab2 3516 |
. . . . . . . . . . . . . 14
    |
14 | 2, 13 | eqsstri 3464 |
. . . . . . . . . . . . 13
 |
15 | 4 | adantr 467 |
. . . . . . . . . . . . . 14
 
   |
16 | | simpr 463 |
. . . . . . . . . . . . . 14
 
   |
17 | 1, 2 | psrbagconcl 18609 |
. . . . . . . . . . . . . 14
 
      |
18 | 12, 15, 16, 17 | syl3anc 1269 |
. . . . . . . . . . . . 13
 
      |
19 | 14, 18 | sseldi 3432 |
. . . . . . . . . . . 12
 
      |
20 | | eqid 2453 |
. . . . . . . . . . . . 13


           |
21 | 1, 20 | psrbagconf1o 18610 |
. . . . . . . . . . . 12
  
    

              
 
    
       |
22 | 12, 19, 21 | syl2anc 667 |
. . . . . . . . . . 11
 
  

              
 
    
       |
23 | | f1of 5819 |
. . . . . . . . . . 11
  

              
 
    
      
       
 
            

      |
24 | 22, 23 | syl 17 |
. . . . . . . . . 10
 
  

              
 
    

      |
25 | | fco 5744 |
. . . . . . . . . 10
             
 
    


              
 
    

       
       

              

        |
26 | 11, 24, 25 | syl2anc 667 |
. . . . . . . . 9
 
           
       
 
     
         |
27 | 12 | adantr 467 |
. . . . . . . . . . . . . . . . 17
    
     
  |
28 | 15 | adantr 467 |
. . . . . . . . . . . . . . . . 17
    
     
  |
29 | 1 | psrbagf 18601 |
. . . . . . . . . . . . . . . . 17
 
       |
30 | 27, 28, 29 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
    
     
      |
31 | 30 | ffvelrnda 6027 |
. . . . . . . . . . . . . . 15
   



    
       |
32 | 16 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
    
     
  |
33 | 14, 32 | sseldi 3432 |
. . . . . . . . . . . . . . . . 17
    
     
  |
34 | 1 | psrbagf 18601 |
. . . . . . . . . . . . . . . . 17
 
       |
35 | 27, 33, 34 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
    
     
      |
36 | 35 | ffvelrnda 6027 |
. . . . . . . . . . . . . . 15
   



    
       |
37 | | ssrab2 3516 |
. . . . . . . . . . . . . . . . . 18


     |
38 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
    
     
        |
39 | 37, 38 | sseldi 3432 |
. . . . . . . . . . . . . . . . 17
    
     
  |
40 | 1 | psrbagf 18601 |
. . . . . . . . . . . . . . . . 17
 
       |
41 | 27, 39, 40 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
    
     
      |
42 | 41 | ffvelrnda 6027 |
. . . . . . . . . . . . . . 15
   



    
       |
43 | | nn0cn 10886 |
. . . . . . . . . . . . . . . 16
    
      |
44 | | nn0cn 10886 |
. . . . . . . . . . . . . . . 16
    
      |
45 | | nn0cn 10886 |
. . . . . . . . . . . . . . . 16
    
      |
46 | | sub32 9913 |
. . . . . . . . . . . . . . . 16
                                                 |
47 | 43, 44, 45, 46 | syl3an 1311 |
. . . . . . . . . . . . . . 15
                                                 |
48 | 31, 36, 42, 47 | syl3anc 1269 |
. . . . . . . . . . . . . 14
   



    
                                   |
49 | 48 | mpteq2dva 4492 |
. . . . . . . . . . . . 13
    
     

                                     |
50 | | ovex 6323 |
. . . . . . . . . . . . . . 15
           |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . 14
   



    
             |
52 | 30 | feqmptd 5923 |
. . . . . . . . . . . . . . 15
    
     
        |
53 | 35 | feqmptd 5923 |
. . . . . . . . . . . . . . 15
    
     
        |
54 | 27, 31, 36, 52, 53 | offval2 6553 |
. . . . . . . . . . . . . 14
    
     
 
               |
55 | 41 | feqmptd 5923 |
. . . . . . . . . . . . . 14
    
     
        |
56 | 27, 51, 42, 54, 55 | offval2 6553 |
. . . . . . . . . . . . 13
    
     
                          |
57 | | ovex 6323 |
. . . . . . . . . . . . . . 15
           |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . 14
   



    
             |
59 | 27, 31, 42, 52, 55 | offval2 6553 |
. . . . . . . . . . . . . 14
    
     
 
               |
60 | 27, 58, 36, 59, 53 | offval2 6553 |
. . . . . . . . . . . . 13
    
     
                          |
61 | 49, 56, 60 | 3eqtr4d 2497 |
. . . . . . . . . . . 12
    
     
              |
62 | 19 | adantr 467 |
. . . . . . . . . . . . 13
    
     
 
   |
63 | 1, 20 | psrbagconcl 18609 |
. . . . . . . . . . . . 13
  
  
     
              |
64 | 27, 62, 38, 63 | syl3anc 1269 |
. . . . . . . . . . . 12
    
     
              |
65 | 61, 64 | eqeltrrd 2532 |
. . . . . . . . . . 11
    
     
              |
66 | 61 | mpteq2dva 4492 |
. . . . . . . . . . 11
 
  

            
       
 
    |
67 | | nfcv 2594 |
. . . . . . . . . . . . 13
   |
68 | | nfcsb1v 3381 |
. . . . . . . . . . . . 13
  
 ![]_ ]_](_urbrack.gif)  |
69 | | csbeq1a 3374 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)   |
70 | 67, 68, 69 | cbvmpt 4497 |
. . . . . . . . . . . 12
  
 
    
       ![]_ ]_](_urbrack.gif)   |
71 | 70 | a1i 11 |
. . . . . . . . . . 11
 
  

      
       ![]_ ]_](_urbrack.gif)    |
72 | | csbeq1 3368 |
. . . . . . . . . . 11
         ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   |
73 | 65, 66, 71, 72 | fmptco 6061 |
. . . . . . . . . 10
 
           
       
 
                  ![]_ ]_](_urbrack.gif)    |
74 | 73 | feq1d 5719 |
. . . . . . . . 9
 
    
       

              

     
 
             ![]_ ]_](_urbrack.gif)               |
75 | 26, 74 | mpbid 214 |
. . . . . . . 8
 
  

            ![]_ ]_](_urbrack.gif)    

        |
76 | | eqid 2453 |
. . . . . . . . 9
  
 
          ![]_ ]_](_urbrack.gif)    
 
          ![]_ ]_](_urbrack.gif)   |
77 | 76 | fmpt 6048 |
. . . . . . . 8
 


             ![]_ ]_](_urbrack.gif)
 
             ![]_ ]_](_urbrack.gif)              |
78 | 75, 77 | sylibr 216 |
. . . . . . 7
 
  
              ![]_ ]_](_urbrack.gif)
  |
79 | 78 | r19.21bi 2759 |
. . . . . 6
    
     
        ![]_ ]_](_urbrack.gif)   |
80 | 79 | anasss 653 |
. . . . 5
 


               ![]_ ]_](_urbrack.gif)   |
81 | 7, 80 | syldan 473 |
. . . 4
 


               ![]_ ]_](_urbrack.gif)   |
82 | 1, 2, 3, 4, 5, 6, 81 | gsumbagdiag 18612 |
. . 3
  g  


            ![]_ ]_](_urbrack.gif)    g  


            ![]_ ]_](_urbrack.gif)     |
83 | | eqid 2453 |
. . . 4
         |
84 | 1 | psrbaglefi 18608 |
. . . . . 6
 
 
    |
85 | 3, 4, 84 | syl2anc 667 |
. . . . 5
 
    |
86 | 2, 85 | syl5eqel 2535 |
. . . 4
   |
87 | 3 | adantr 467 |
. . . . 5
 
   |
88 | 4 | adantr 467 |
. . . . . . 7
 
   |
89 | | simpr 463 |
. . . . . . 7
 
   |
90 | 1, 2 | psrbagconcl 18609 |
. . . . . . 7
 
      |
91 | 87, 88, 89, 90 | syl3anc 1269 |
. . . . . 6
 
      |
92 | 14, 91 | sseldi 3432 |
. . . . 5
 
      |
93 | 1 | psrbaglefi 18608 |
. . . . 5
  
  


      |
94 | 87, 92, 93 | syl2anc 667 |
. . . 4
 
 

      |
95 | | xpfi 7847 |
. . . . 5
 
     |
96 | 86, 86, 95 | syl2anc 667 |
. . . 4
     |
97 | | simprl 765 |
. . . . . . 7
 


         |
98 | 7 | simpld 461 |
. . . . . . 7
 


         |
99 | | brxp 4868 |
. . . . . . 7
    

   |
100 | 97, 98, 99 | sylanbrc 671 |
. . . . . 6
 


             |
101 | 100 | pm2.24d 138 |
. . . . 5
 


               
 
  ![]_ ]_](_urbrack.gif)
       |
102 | 101 | impr 625 |
. . . 4
 
 


          
        ![]_ ]_](_urbrack.gif)       |
103 | 5, 83, 6, 86, 94, 81, 96, 102 | gsum2d2 17618 |
. . 3
  g  


            ![]_ ]_](_urbrack.gif)    g   g                ![]_ ]_](_urbrack.gif)       |
104 | 1 | psrbaglefi 18608 |
. . . . 5
  
   

      |
105 | 12, 19, 104 | syl2anc 667 |
. . . 4
 
 

      |
106 | | simprl 765 |
. . . . . . 7
 


         |
107 | 1, 2, 3, 4 | gsumbagdiaglem 18611 |
. . . . . . . 8
 


       


       |
108 | 107 | simpld 461 |
. . . . . . 7
 


         |
109 | | brxp 4868 |
. . . . . . 7
    

   |
110 | 106, 108,
109 | sylanbrc 671 |
. . . . . 6
 


             |
111 | 110 | pm2.24d 138 |
. . . . 5
 


               
 
  ![]_ ]_](_urbrack.gif)
       |
112 | 111 | impr 625 |
. . . 4
 
 


          
        ![]_ ]_](_urbrack.gif)       |
113 | 5, 83, 6, 86, 105, 80, 96, 112 | gsum2d2 17618 |
. . 3
  g  


            ![]_ ]_](_urbrack.gif)    g   g                ![]_ ]_](_urbrack.gif)       |
114 | 82, 103, 113 | 3eqtr3d 2495 |
. 2
  g   g                ![]_ ]_](_urbrack.gif)      g   g 


            ![]_ ]_](_urbrack.gif)       |
115 | 6 | adantr 467 |
. . . . . . . 8
 
 CMnd |
116 | 81 | anassrs 654 |
. . . . . . . . 9
    
     
        ![]_ ]_](_urbrack.gif)   |
117 | | eqid 2453 |
. . . . . . . . 9
  
 
          ![]_ ]_](_urbrack.gif)    
 
          ![]_ ]_](_urbrack.gif)   |
118 | 116, 117 | fmptd 6051 |
. . . . . . . 8
 
  

            ![]_ ]_](_urbrack.gif)    

        |
119 | | ovex 6323 |
. . . . . . . . . . . 12
   |
120 | 1, 119 | rabex2 4559 |
. . . . . . . . . . 11
 |
121 | 120 | a1i 11 |
. . . . . . . . . 10
 
   |
122 | | rabexg 4556 |
. . . . . . . . . 10
 

      |
123 | | mptexg 6140 |
. . . . . . . . . 10
                      ![]_ ]_](_urbrack.gif)    |
124 | 121, 122,
123 | 3syl 18 |
. . . . . . . . 9
 
  

            ![]_ ]_](_urbrack.gif)    |
125 | | funmpt 5621 |
. . . . . . . . . 10
 

            ![]_ ]_](_urbrack.gif)   |
126 | 125 | a1i 11 |
. . . . . . . . 9
 
                ![]_ ]_](_urbrack.gif)    |
127 | | fvex 5880 |
. . . . . . . . . 10
     |
128 | 127 | a1i 11 |
. . . . . . . . 9
 
       |
129 | | suppssdm 6932 |
. . . . . . . . . . 11
  

            ![]_ ]_](_urbrack.gif)  supp                     ![]_ ]_](_urbrack.gif)   |
130 | 117 | dmmptss 5334 |
. . . . . . . . . . 11
 

            ![]_ ]_](_urbrack.gif) 


     |
131 | 129, 130 | sstri 3443 |
. . . . . . . . . 10
  

            ![]_ ]_](_urbrack.gif)  supp             |
132 | 131 | a1i 11 |
. . . . . . . . 9
 
                 ![]_ ]_](_urbrack.gif)  supp              |
133 | | suppssfifsupp 7903 |
. . . . . . . . 9
    
             ![]_ ]_](_urbrack.gif)   
             ![]_ ]_](_urbrack.gif)        
                     ![]_ ]_](_urbrack.gif)  supp               
             ![]_ ]_](_urbrack.gif)  finSupp       |
134 | 124, 126,
128, 94, 132, 133 | syl32anc 1277 |
. . . . . . . 8
 
  

            ![]_ ]_](_urbrack.gif)  finSupp       |
135 | 5, 83, 115, 94, 118, 134 | gsumcl 17561 |
. . . . . . 7
 
  g                ![]_ ]_](_urbrack.gif)     |
136 | | eqid 2453 |
. . . . . . 7
  g                ![]_ ]_](_urbrack.gif)      g                ![]_ ]_](_urbrack.gif)     |
137 | 135, 136 | fmptd 6051 |
. . . . . 6
   g                ![]_ ]_](_urbrack.gif)          |
138 | 1, 2 | psrbagconf1o 18610 |
. . . . . . . 8
 
            |
139 | 3, 4, 138 | syl2anc 667 |
. . . . . . 7
            |
140 | | f1ocnv 5831 |
. . . . . . 7
         
            |
141 | | f1of 5819 |
. . . . . . 7
          
            |
142 | 139, 140,
141 | 3syl 18 |
. . . . . 6
    
        |
143 | | fco 5744 |
. . . . . 6
    g                ![]_ ]_](_urbrack.gif)         
            g                ![]_ ]_](_urbrack.gif)       
         |
144 | 137, 142,
143 | syl2anc 667 |
. . . . 5
    g   
 
          ![]_ ]_](_urbrack.gif)       
         |
145 | | coass 5357 |
. . . . . . . 8
    g                 
      g                 
     |
146 | | f1ococnv2 5845 |
. . . . . . . . . 10
         
         
  
   |
147 | 139, 146 | syl 17 |
. . . . . . . . 9
    
            |
148 | 147 | coeq2d 5000 |
. . . . . . . 8
    g   
           
         g            |
149 | 145, 148 | syl5eq 2499 |
. . . . . . 7
     g                 
      g            |
150 | | eqidd 2454 |
. . . . . . . . 9
        
    |
151 | | eqidd 2454 |
. . . . . . . . 9
   g          g          |
152 | | breq2 4409 |
. . . . . . . . . . . 12
  
  
  
    |
153 | 152 | rabbidv 3038 |
. . . . . . . . . . 11
  
 
          |
154 | | ovex 6323 |
. . . . . . . . . . . . 13
    |
155 | | psrass1lem.y |
. . . . . . . . . . . . 13
      |
156 | 154, 155 | csbie 3391 |
. . . . . . . . . . . 12
     ![]_ ]_](_urbrack.gif)
 |
157 | | oveq1 6302 |
. . . . . . . . . . . . 13
  
      
 
   |
158 | 157 | csbeq1d 3372 |
. . . . . . . . . . . 12
  
      ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   |
159 | 156, 158 | syl5eqr 2501 |
. . . . . . . . . . 11
  
         ![]_ ]_](_urbrack.gif)   |
160 | 153, 159 | mpteq12dv 4484 |
. . . . . . . . . 10
  
                     ![]_ ]_](_urbrack.gif)    |
161 | 160 | oveq2d 6311 |
. . . . . . . . 9
  
  g        g   
 
          ![]_ ]_](_urbrack.gif)     |
162 | 91, 150, 151, 161 | fmptco 6061 |
. . . . . . . 8
    g   
      
     g                ![]_ ]_](_urbrack.gif)      |
163 | 162 | coeq1d 4999 |
. . . . . . 7
     g                 
      g                ![]_ ]_](_urbrack.gif)       
     |
164 | | coires1 5356 |
. . . . . . . . 9
   g             g   
      |
165 | | ssid 3453 |
. . . . . . . . . 10
 |
166 | | resmpt 5157 |
. . . . . . . . . 10
    g       
   g   
      |
167 | 165, 166 | ax-mp 5 |
. . . . . . . . 9
   g       
   g   
     |
168 | 164, 167 | eqtri 2475 |
. . . . . . . 8
   g            g         |
169 | 168 | a1i 11 |
. . . . . . 7
    g   
        g          |
170 | 149, 163,
169 | 3eqtr3d 2495 |
. . . . . 6
    g   
 
          ![]_ ]_](_urbrack.gif)       
     g          |
171 | 170 | feq1d 5719 |
. . . . 5
     g                ![]_ ]_](_urbrack.gif)       
         g               |
172 | 144, 171 | mpbid 214 |
. . . 4
   g              |
173 | | rabexg 4556 |
. . . . . . . 8
   
  |
174 | 120, 173 | mp1i 13 |
. . . . . . 7
 
    |
175 | 2, 174 | syl5eqel 2535 |
. . . . . 6
   |
176 | | mptexg 6140 |
. . . . . 6
   g          |
177 | 175, 176 | syl 17 |
. . . . 5
   g          |
178 | | funmpt 5621 |
. . . . . 6
  g         |
179 | 178 | a1i 11 |
. . . . 5
   g   
      |
180 | 127 | a1i 11 |
. . . . 5
       |
181 | | suppssdm 6932 |
. . . . . . 7
   g        supp        g         |
182 | | eqid 2453 |
. . . . . . . 8
  g          g         |
183 | 182 | dmmptss 5334 |
. . . . . . 7
  g       
 |
184 | 181, 183 | sstri 3443 |
. . . . . 6
   g        supp       |
185 | 184 | a1i 11 |
. . . . 5
    g   
    supp        |
186 | | suppssfifsupp 7903 |
. . . . 5
     g   
    
 g             
   g        supp          g        finSupp       |
187 | 177, 179,
180, 86, 185, 186 | syl32anc 1277 |
. . . 4
   g        finSupp       |
188 | 5, 83, 6, 86, 172, 187, 139 | gsumf1o 17562 |
. . 3
  g   g          g    g   
      
      |
189 | 162 | oveq2d 6311 |
. . 3
  g    g   
      
     g   g                ![]_ ]_](_urbrack.gif)       |
190 | 188, 189 | eqtrd 2487 |
. 2
  g   g          g   g                ![]_ ]_](_urbrack.gif)       |
191 | 6 | adantr 467 |
. . . . . 6
 
 CMnd |
192 | 120 | a1i 11 |
. . . . . . . 8
 
   |
193 | | rabexg 4556 |
. . . . . . . 8
 

      |
194 | | mptexg 6140 |
. . . . . . . 8
                 |
195 | 192, 193,
194 | 3syl 18 |
. . . . . . 7
 
  

       |
196 | | funmpt 5621 |
. . . . . . . 8
 

      |
197 | 196 | a1i 11 |
. . . . . . 7
 
           |
198 | 127 | a1i 11 |
. . . . . . 7
 
       |
199 | | suppssdm 6932 |
. . . . . . . . 9
  

     supp               |
200 | 10 | dmmptss 5334 |
. . . . . . . . 9
 

      
 
   |
201 | 199, 200 | sstri 3443 |
. . . . . . . 8
  

     supp      

     |
202 | 201 | a1i 11 |
. . . . . . 7
 
          supp      

      |
203 | | suppssfifsupp 7903 |
. . . . . . 7
    
       
            
              supp      

       
      finSupp       |
204 | 195, 197,
198, 105, 202, 203 | syl32anc 1277 |
. . . . . 6
 
  

     finSupp       |
205 | 5, 83, 191, 105, 11, 204, 22 | gsumf1o 17562 |
. . . . 5
 
  g           g   
       

               |
206 | 73 | oveq2d 6311 |
. . . . 5
 
  g   
       

              g                ![]_ ]_](_urbrack.gif)     |
207 | 205, 206 | eqtrd 2487 |
. . . 4
 
  g           g 


            ![]_ ]_](_urbrack.gif)     |
208 | 207 | mpteq2dva 4492 |
. . 3
   g             g                ![]_ ]_](_urbrack.gif)      |
209 | 208 | oveq2d 6311 |
. 2
  g   g             g   g                ![]_ ]_](_urbrack.gif)       |
210 | 114, 190,
209 | 3eqtr4d 2497 |
1
  g   g          g   g              |