Step | Hyp | Ref
| Expression |
1 | | sibfof.1 |
. . . . . . . 8
        |
2 | | sibfof.0 |
. . . . . . . . . . 11
   |
3 | | sitgval.b |
. . . . . . . . . . . 12
     |
4 | | sitgval.j |
. . . . . . . . . . . 12
     |
5 | 3, 4 | tpsuni 19953 |
. . . . . . . . . . 11

   |
6 | 2, 5 | syl 17 |
. . . . . . . . . 10
    |
7 | 6 | sqxpeqd 4860 |
. . . . . . . . 9
         |
8 | 7 | feq2d 5715 |
. . . . . . . 8
                |
9 | 1, 8 | mpbid 214 |
. . . . . . 7
          |
10 | 9 | fovrnda 6440 |
. . . . . 6
 
         |
11 | | sitgval.s |
. . . . . . 7
sigaGen   |
12 | | sitgval.0 |
. . . . . . 7
     |
13 | | sitgval.x |
. . . . . . 7
     |
14 | | sitgval.h |
. . . . . . 7
RRHom Scalar    |
15 | | sitgval.1 |
. . . . . . 7
   |
16 | | sitgval.2 |
. . . . . . 7
  measures |
17 | | sibfmbl.1 |
. . . . . . 7
  sitg   |
18 | 3, 4, 11, 12, 13, 14, 15, 16, 17 | sibff 29169 |
. . . . . 6
         |
19 | | sibfof.2 |
. . . . . . 7
  sitg   |
20 | 3, 4, 11, 12, 13, 14, 15, 16, 19 | sibff 29169 |
. . . . . 6
         |
21 | | dmexg 6724 |
. . . . . . 7
  measures   |
22 | | uniexg 6588 |
. . . . . . 7
 
  |
23 | 16, 21, 22 | 3syl 18 |
. . . . . 6
    |
24 | | inidm 3641 |
. . . . . 6
      |
25 | 10, 18, 20, 23, 23, 24 | off 6546 |
. . . . 5
           |
26 | | sibfof.3 |
. . . . . . . 8
   |
27 | | sibfof.c |
. . . . . . . . 9
     |
28 | | eqid 2451 |
. . . . . . . . 9
         |
29 | 27, 28 | tpsuni 19953 |
. . . . . . . 8

       |
30 | 26, 29 | syl 17 |
. . . . . . 7
        |
31 | | fvex 5875 |
. . . . . . . 8
     |
32 | | unisg 28965 |
. . . . . . . 8
      sigaGen             |
33 | 31, 32 | ax-mp 5 |
. . . . . . 7
 sigaGen            |
34 | 30, 33 | syl6eqr 2503 |
. . . . . 6
  sigaGen        |
35 | 34 | feq3d 5716 |
. . . . 5
         
 
       sigaGen         |
36 | 25, 35 | mpbid 214 |
. . . 4
          sigaGen        |
37 | 31 | a1i 11 |
. . . . . . 7
       |
38 | 37 | sgsiga 28964 |
. . . . . 6
 sigaGen       sigAlgebra |
39 | | uniexg 6588 |
. . . . . 6
 sigaGen       sigAlgebra  sigaGen        |
40 | 38, 39 | syl 17 |
. . . . 5
  sigaGen        |
41 | 40, 23 | elmapd 7486 |
. . . 4
       sigaGen                 sigaGen         |
42 | 36, 41 | mpbird 236 |
. . 3
      sigaGen          |
43 | | inundif 3845 |
. . . . . . 7
      
      |
44 | 43 | imaeq2i 5166 |
. . . . . 6
                             |
45 | | ffun 5731 |
. . . . . . . 8
         
    |
46 | | unpreima 6006 |
. . . . . . . 8
                 
               
           
        |
47 | 25, 45, 46 | 3syl 18 |
. . . . . . 7
              
               
           
        |
48 | 47 | adantr 467 |
. . . . . 6
 
sigaGen                    
               
           
        |
49 | 44, 48 | syl5eqr 2499 |
. . . . 5
 
sigaGen                        
           
        |
50 | | dmmeas 29023 |
. . . . . . . 8
  measures  sigAlgebra |
51 | 16, 50 | syl 17 |
. . . . . . 7
  sigAlgebra |
52 | 51 | adantr 467 |
. . . . . 6
 
sigaGen        sigAlgebra |
53 | | imaiun 6150 |
. . . . . . . 8
       

        
                 |
54 | | iunid 4333 |
. . . . . . . . 9
  
            |
55 | 54 | imaeq2i 5166 |
. . . . . . . 8
       

                
     |
56 | 53, 55 | eqtr3i 2475 |
. . . . . . 7
  
                     
      |
57 | | inss2 3653 |
. . . . . . . . . 10

 
 
    |
58 | 6 | feq3d 5716 |
. . . . . . . . . . . . . . 15
      
         |
59 | 18, 58 | mpbird 236 |
. . . . . . . . . . . . . 14
        |
60 | 6 | feq3d 5716 |
. . . . . . . . . . . . . . 15
      
         |
61 | 20, 60 | mpbird 236 |
. . . . . . . . . . . . . 14
        |
62 | | ffn 5728 |
. . . . . . . . . . . . . . 15
         |
63 | 1, 62 | syl 17 |
. . . . . . . . . . . . . 14
     |
64 | 59, 61, 23, 63 | ofpreima2 28269 |
. . . . . . . . . . . . 13
           
                                    |
65 | 64 | adantr 467 |
. . . . . . . . . . . 12
 
                                                   |
66 | 51 | adantr 467 |
. . . . . . . . . . . . 13
 
   
 sigAlgebra |
67 | 51 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
                
 sigAlgebra |
68 | | simpll 760 |
. . . . . . . . . . . . . . . 16
                   |
69 | | inss1 3652 |
. . . . . . . . . . . . . . . . . 18
               |
70 | | cnvimass 5188 |
. . . . . . . . . . . . . . . . . . . 20
    
 |
71 | | fdm 5733 |
. . . . . . . . . . . . . . . . . . . . 21
         |
72 | 1, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20

    |
73 | 70, 72 | syl5sseq 3480 |
. . . . . . . . . . . . . . . . . . 19
      
   |
74 | 73 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
             |
75 | 69, 74 | syl5ss 3443 |
. . . . . . . . . . . . . . . . 17
 
                 |
76 | 75 | sselda 3432 |
. . . . . . . . . . . . . . . 16
                     |
77 | 51 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 

   sigAlgebra |
78 | | sibfof.4 |
. . . . . . . . . . . . . . . . . . . 20
   |
79 | 78 | sgsiga 28964 |
. . . . . . . . . . . . . . . . . . 19
 sigaGen  
sigAlgebra |
80 | 11, 79 | syl5eqel 2533 |
. . . . . . . . . . . . . . . . . 18
  sigAlgebra |
81 | 80 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 

  
sigAlgebra |
82 | 3, 4, 11, 12, 13, 14, 15, 16, 17 | sibfmbl 29168 |
. . . . . . . . . . . . . . . . . 18
  MblFnM   |
83 | 82 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 

   MblFnM   |
84 | 4 | tpstop 19954 |
. . . . . . . . . . . . . . . . . . . . 21

  |
85 | | cldssbrsiga 29009 |
. . . . . . . . . . . . . . . . . . . . 21
     sigaGen    |
86 | 2, 84, 85 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
    
sigaGen    |
87 | 86 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 

      sigaGen    |
88 | 78 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 

    |
89 | | xp1st 6823 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
90 | 89 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
 

        |
91 | 6 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 

     |
92 | 90, 91 | eleqtrd 2531 |
. . . . . . . . . . . . . . . . . . . 20
 

         |
93 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . 21
   |
94 | 93 | t1sncld 20342 |
. . . . . . . . . . . . . . . . . . . 20
                    |
95 | 88, 92, 94 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
 

              |
96 | 87, 95 | sseldd 3433 |
. . . . . . . . . . . . . . . . . 18
 

        sigaGen    |
97 | 96, 11 | syl6eleqr 2540 |
. . . . . . . . . . . . . . . . 17
 

          |
98 | 77, 81, 83, 97 | mbfmcnvima 29079 |
. . . . . . . . . . . . . . . 16
 

               |
99 | 68, 76, 98 | syl2anc 667 |
. . . . . . . . . . . . . . 15
                              |
100 | 3, 4, 11, 12, 13, 14, 15, 16, 19 | sibfmbl 29168 |
. . . . . . . . . . . . . . . . . 18
  MblFnM   |
101 | 100 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 

   MblFnM   |
102 | | xp2nd 6824 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
103 | 102 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
 

        |
104 | 103, 91 | eleqtrd 2531 |
. . . . . . . . . . . . . . . . . . . 20
 

         |
105 | 93 | t1sncld 20342 |
. . . . . . . . . . . . . . . . . . . 20
                    |
106 | 88, 104, 105 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
 

              |
107 | 87, 106 | sseldd 3433 |
. . . . . . . . . . . . . . . . . 18
 

        sigaGen    |
108 | 107, 11 | syl6eleqr 2540 |
. . . . . . . . . . . . . . . . 17
 

          |
109 | 77, 81, 101, 108 | mbfmcnvima 29079 |
. . . . . . . . . . . . . . . 16
 

               |
110 | 68, 76, 109 | syl2anc 667 |
. . . . . . . . . . . . . . 15
                              |
111 | | inelsiga 28957 |
. . . . . . . . . . . . . . 15
   sigAlgebra           
           
                          |
112 | 67, 99, 110, 111 | syl3anc 1268 |
. . . . . . . . . . . . . 14
                                           |
113 | 112 | ralrimiva 2802 |
. . . . . . . . . . . . 13
 
                                         |
114 | 3, 4, 11, 12, 13, 14, 15, 16, 17 | sibfrn 29170 |
. . . . . . . . . . . . . . . . 17
   |
115 | 3, 4, 11, 12, 13, 14, 15, 16, 19 | sibfrn 29170 |
. . . . . . . . . . . . . . . . 17
   |
116 | | xpfi 7842 |
. . . . . . . . . . . . . . . . 17
 
     |
117 | 114, 115,
116 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
     |
118 | | inss2 3653 |
. . . . . . . . . . . . . . . 16
            |
119 | | ssdomg 7615 |
. . . . . . . . . . . . . . . 16
                             |
120 | 117, 118,
119 | mpisyl 21 |
. . . . . . . . . . . . . . 15
              |
121 | | isfinite 8157 |
. . . . . . . . . . . . . . . . 17
  
    |
122 | 121 | biimpi 198 |
. . . . . . . . . . . . . . . 16
    
  |
123 | | sdomdom 7597 |
. . . . . . . . . . . . . . . 16
  
    |
124 | 117, 122,
123 | 3syl 18 |
. . . . . . . . . . . . . . 15
     |
125 | | domtr 7622 |
. . . . . . . . . . . . . . 15
                           |
126 | 120, 124,
125 | syl2anc 667 |
. . . . . . . . . . . . . 14
            |
127 | 126 | adantr 467 |
. . . . . . . . . . . . 13
 
               |
128 | | nfcv 2592 |
. . . . . . . . . . . . . 14
            |
129 | 128 | sigaclcuni 28940 |
. . . . . . . . . . . . 13
   sigAlgebra                                                                                   |
130 | 66, 113, 127, 129 | syl3anc 1268 |
. . . . . . . . . . . 12
 
                                         |
131 | 65, 130 | eqeltrd 2529 |
. . . . . . . . . . 11
 
                |
132 | 131 | ralrimiva 2802 |
. . . . . . . . . 10
  
               |
133 | | ssralv 3493 |
. . . . . . . . . 10
      
   

             

                  |
134 | 57, 132, 133 | mpsyl 65 |
. . . . . . . . 9
                    |
135 | 134 | adantr 467 |
. . . . . . . 8
 
sigaGen       

                 |
136 | | ffun 5731 |
. . . . . . . . . . . . . 14
      |
137 | 1, 136 | syl 17 |
. . . . . . . . . . . . 13

 |
138 | | imafi 7867 |
. . . . . . . . . . . . 13
 
         |
139 | 137, 117,
138 | syl2anc 667 |
. . . . . . . . . . . 12
       |
140 | 18, 20, 9, 23 | ofrn2 28241 |
. . . . . . . . . . . 12
          |
141 | | ssfi 7792 |
. . . . . . . . . . . 12
                   |
142 | 139, 140,
141 | syl2anc 667 |
. . . . . . . . . . 11
      |
143 | | ssdomg 7615 |
. . . . . . . . . . 11
     
 
 
  
           |
144 | 142, 57, 143 | mpisyl 21 |
. . . . . . . . . 10
  
        |
145 | | isfinite 8157 |
. . . . . . . . . . . 12
         |
146 | 142, 145 | sylib 200 |
. . . . . . . . . . 11
      |
147 | | sdomdom 7597 |
. . . . . . . . . . 11
   
 
   |
148 | 146, 147 | syl 17 |
. . . . . . . . . 10
      |
149 | | domtr 7622 |
. . . . . . . . . 10
   
         
       |
150 | 144, 148,
149 | syl2anc 667 |
. . . . . . . . 9
  
     |
151 | 150 | adantr 467 |
. . . . . . . 8
 
sigaGen        
     |
152 | | nfcv 2592 |
. . . . . . . . 9
   
    |
153 | 152 | sigaclcuni 28940 |
. . . . . . . 8
   sigAlgebra                   
   
  
                |
154 | 52, 135, 151, 153 | syl3anc 1268 |
. . . . . . 7
 
sigaGen       

                 |
155 | 56, 154 | syl5eqelr 2534 |
. . . . . 6
 
sigaGen              
 
     |
156 | | difpreima 6008 |
. . . . . . . . . 10
           
 
                   
      |
157 | 25, 45, 156 | 3syl 18 |
. . . . . . . . 9
        
 
                   
      |
158 | | cnvimarndm 5189 |
. . . . . . . . . . 11
               |
159 | 158 | difeq2i 3548 |
. . . . . . . . . 10
                              
    |
160 | | cnvimass 5188 |
. . . . . . . . . . 11
        
   |
161 | | ssdif0 3823 |
. . . . . . . . . . 11
         
 
         
     |
162 | 160, 161 | mpbi 212 |
. . . . . . . . . 10
         
    |
163 | 159, 162 | eqtri 2473 |
. . . . . . . . 9
                      |
164 | 157, 163 | syl6eq 2501 |
. . . . . . . 8
        
 
     |
165 | | 0elsiga 28936 |
. . . . . . . . 9
  sigAlgebra   |
166 | 16, 50, 165 | 3syl 18 |
. . . . . . . 8

  |
167 | 164, 166 | eqeltrd 2529 |
. . . . . . 7
        
 
     |
168 | 167 | adantr 467 |
. . . . . 6
 
sigaGen              
 
     |
169 | | unelsiga 28956 |
. . . . . 6
   sigAlgebra        
 
          
              
            
 
      |
170 | 52, 155, 168, 169 | syl3anc 1268 |
. . . . 5
 
sigaGen               
            
 
      |
171 | 49, 170 | eqeltrd 2529 |
. . . 4
 
sigaGen                 |
172 | 171 | ralrimiva 2802 |
. . 3
  sigaGen                 |
173 | 51, 38 | ismbfm 29074 |
. . 3
      MblFnM sigaGen      
      sigaGen        
sigaGen                   |
174 | 42, 172, 173 | mpbir2and 933 |
. 2
     MblFnM sigaGen         |
175 | 64 | adantr 467 |
. . . . . . 7
 
           
  
                                            |
176 | 175 | fveq2d 5869 |
. . . . . 6
 
           
                                                       |
177 | | measbasedom 29024 |
. . . . . . . . 9
  measures
measures    |
178 | 16, 177 | sylib 200 |
. . . . . . . 8
 measures    |
179 | 178 | adantr 467 |
. . . . . . 7
 
           
measures    |
180 | | eldifi 3555 |
. . . . . . . 8
    
      
     |
181 | 180, 113 | sylan2 477 |
. . . . . . 7
 
           
                                     |
182 | 126 | adantr 467 |
. . . . . . 7
 
           
           |
183 | | sneq 3978 |
. . . . . . . . . . 11
    
 
        |
184 | 183 | imaeq2d 5168 |
. . . . . . . . . 10
    
                    |
185 | | sneq 3978 |
. . . . . . . . . . 11
    
 
        |
186 | 185 | imaeq2d 5168 |
. . . . . . . . . 10
    
                    |
187 | | ffun 5731 |
. . . . . . . . . . . 12
      
  |
188 | 18, 187 | syl 17 |
. . . . . . . . . . 11
   |
189 | | sndisj 4394 |
. . . . . . . . . . 11
Disj     |
190 | | disjpreima 28194 |
. . . . . . . . . . 11
  Disj     Disj           |
191 | 188, 189,
190 | sylancl 668 |
. . . . . . . . . 10
 Disj
          |
192 | | ffun 5731 |
. . . . . . . . . . . 12
      
  |
193 | 20, 192 | syl 17 |
. . . . . . . . . . 11
   |
194 | | sndisj 4394 |
. . . . . . . . . . 11
Disj     |
195 | | disjpreima 28194 |
. . . . . . . . . . 11
  Disj     Disj           |
196 | 193, 194,
195 | sylancl 668 |
. . . . . . . . . 10
 Disj
          |
197 | 184, 186,
191, 196 | disjxpin 28198 |
. . . . . . . . 9
 Disj
                             |
198 | | disjss1 4379 |
. . . . . . . . 9
           
Disj                            Disj                                      |
199 | 118, 197,
198 | mpsyl 65 |
. . . . . . . 8
 Disj
                                    |
200 | 199 | adantr 467 |
. . . . . . 7
 
           
Disj                                     |
201 | | measvuni 29036 |
. . . . . . 7
  measures                                               Disj                                    
                                      
Σ*
                                        |
202 | 179, 181,
182, 200, 201 | syl112anc 1272 |
. . . . . 6
 
           
                                      
Σ*
                                        |
203 | | ssfi 7792 |
. . . . . . . . 9
                           |
204 | 117, 118,
203 | sylancl 668 |
. . . . . . . 8
            |
205 | 204 | adantr 467 |
. . . . . . 7
 
           
           |
206 | | simpll 760 |
. . . . . . . 8
      
                 
  |
207 | | simpr 463 |
. . . . . . . . . 10
      
                 
           |
208 | 118, 207 | sseldi 3430 |
. . . . . . . . 9
      
                 
    |
209 | | xp1st 6823 |
. . . . . . . . 9
         |
210 | 208, 209 | syl 17 |
. . . . . . . 8
      
                 
      |
211 | | xp2nd 6824 |
. . . . . . . . 9
         |
212 | 208, 211 | syl 17 |
. . . . . . . 8
      
                 
      |
213 | | oveq12 6299 |
. . . . . . . . . . . . . . . 16
 
    |
214 | | sibfof.5 |
. . . . . . . . . . . . . . . 16

      |
215 | 213, 214 | sylan9eqr 2507 |
. . . . . . . . . . . . . . 15
 
          |
216 | 215 | ex 436 |
. . . . . . . . . . . . . 14
   
        |
217 | 216 | necon3ad 2637 |
. . . . . . . . . . . . 13
            |
218 | | neorian 2718 |
. . . . . . . . . . . . 13
 

  |
219 | 217, 218 | syl6ibr 231 |
. . . . . . . . . . . 12
        
   |
220 | 219 | adantr 467 |
. . . . . . . . . . 11
 

         
   |
221 | 220 | ralrimivva 2809 |
. . . . . . . . . 10
  
       
   |
222 | 206, 221 | syl 17 |
. . . . . . . . 9
      
                 


 
    
    |
223 | 69 | a1i 11 |
. . . . . . . . . . . . 13
 
           
                |
224 | 223 | sselda 3432 |
. . . . . . . . . . . 12
      
                 

      |
225 | | fniniseg 6003 |
. . . . . . . . . . . . 13
 
     
  
      |
226 | 206, 63, 225 | 3syl 18 |
. . . . . . . . . . . 12
      
                 
     
  
      |
227 | 224, 226 | mpbid 214 |
. . . . . . . . . . 11
      
                 
  
     |
228 | | simpr 463 |
. . . . . . . . . . . 12
      
    |
229 | | 1st2nd2 6830 |
. . . . . . . . . . . . . . 15
                |
230 | 229 | fveq2d 5869 |
. . . . . . . . . . . . . 14
                    |
231 | | df-ov 6293 |
. . . . . . . . . . . . . 14
                        |
232 | 230, 231 | syl6eqr 2503 |
. . . . . . . . . . . . 13
         
       |
233 | 232 | adantr 467 |
. . . . . . . . . . . 12
      
              |
234 | 228, 233 | eqtr3d 2487 |
. . . . . . . . . . 11
                   |
235 | 227, 234 | syl 17 |
. . . . . . . . . 10
      
                 
    
       |
236 | | simplr 762 |
. . . . . . . . . . . 12
      
                 
             |
237 | 236 | eldifbd 3417 |
. . . . . . . . . . 11
      
                 
        |
238 | | elsn 3982 |
. . . . . . . . . . . 12
             |
239 | 238 | necon3bbii 2671 |
. . . . . . . . . . 11
             |
240 | 237, 239 | sylib 200 |
. . . . . . . . . 10
      
                 
      |
241 | 235, 240 | eqnetrrd 2692 |
. . . . . . . . 9
      
                 
                |
242 | 180, 76 | sylanl2 657 |
. . . . . . . . . . 11
      
                 

   |
243 | 242, 89 | syl 17 |
. . . . . . . . . 10
      
                 
      |
244 | 242, 102 | syl 17 |
. . . . . . . . . 10
      
                 
      |
245 | | oveq1 6297 |
. . . . . . . . . . . . 13
    
      
   |
246 | 245 | neeq1d 2683 |
. . . . . . . . . . . 12
    
 
                  |
247 | | neeq1 2686 |
. . . . . . . . . . . . 13
    
       |
248 | 247 | orbi1d 709 |
. . . . . . . . . . . 12
    
 
    
   |
249 | 246, 248 | imbi12d 322 |
. . . . . . . . . . 11
    
        

     
    
    
    |
250 | | oveq2 6298 |
. . . . . . . . . . . . 13
    
          
       |
251 | 250 | neeq1d 2683 |
. . . . . . . . . . . 12
    
     
                      |
252 | | neeq1 2686 |
. . . . . . . . . . . . 13
    
       |
253 | 252 | orbi2d 708 |
. . . . . . . . . . . 12
    
     
    
       |
254 | 251, 253 | imbi12d 322 |
. . . . . . . . . . 11
    
      
    
    

     
        
    
        |
255 | 249, 254 | rspc2v 3159 |
. . . . . . . . . 10
                    
                              |
256 | 243, 244,
255 | syl2anc 667 |
. . . . . . . . 9
      
                 
 

       
      
        
    
        |
257 | 222, 241,
256 | mp2d 46 |
. . . . . . . 8
      
                 
    
      |
258 | 3, 4, 11, 12, 13, 14, 15, 16, 17, 19, 2, 78 | sibfinima 29172 |
. . . . . . . 8
      
                                                |
259 | 206, 210,
212, 257, 258 | syl31anc 1271 |
. . . . . . 7
      
                 
                                 |
260 | 205, 259 | esumpfinval 28896 |
. . . . . 6
 
           
Σ*
                                                                               |
261 | 176, 202,
260 | 3eqtrd 2489 |
. . . . 5
 
           
              
                                        |
262 | | rge0ssre 11740 |
. . . . . . 7
    |
263 | 262, 259 | sseldi 3430 |
. . . . . 6
      
                 
                              |
264 | 205, 263 | fsumrecl 13800 |
. . . . 5
 
           
                                         |
265 | 261, 264 | eqeltrd 2529 |
. . . 4
 
           
                |
266 | 179 | adantr 467 |
. . . . . . 7
      
                 
measures    |
267 | 180, 112 | sylanl2 657 |
. . . . . . 7
      
                 
                          |
268 | | measge0 29029 |
. . . . . . 7
  measures                          
                              |
269 | 266, 267,
268 | syl2anc 667 |
. . . . . 6
      
                 
                              |
270 | 205, 263,
269 | fsumge0 13855 |
. . . . 5
 
           
                                         |
271 | 270, 261 | breqtrrd 4429 |
. . . 4
 
           
                |
272 | | elrege0 11738 |
. . . 4
                 
      
                         |
273 | 265, 271,
272 | sylanbrc 670 |
. . 3
 
           
                   |
274 | 273 | ralrimiva 2802 |
. 2
                                 |
275 | | eqid 2451 |
. . 3
sigaGen      sigaGen       |
276 | | eqid 2451 |
. . 3
         |
277 | | eqid 2451 |
. . 3
         |
278 | | eqid 2451 |
. . 3
RRHom Scalar   RRHom Scalar    |
279 | 27, 28, 275, 276, 277, 278, 26, 16 | issibf 29166 |
. 2
      sitg      MblFnM sigaGen         
    
                             |
280 | 174, 142,
274, 279 | mpbir3and 1191 |
1
     sitg   |