Step | Hyp | Ref
| Expression |
1 | | ofcfval3 28997 |
. . 3
  measures 

 ∘𝑓/𝑐
/𝑒       
/𝑒     |
2 | | measfrge0 29099 |
. . . . . 6
 measures 
         |
3 | | fdm 5745 |
. . . . . 6
          |
4 | 2, 3 | syl 17 |
. . . . 5
 measures 
  |
5 | 4 | adantr 472 |
. . . 4
  measures 

  |
6 | 5 | mpteq1d 4477 |
. . 3
  measures 

      /𝑒         /𝑒     |
7 | 1, 6 | eqtrd 2505 |
. 2
  measures 

 ∘𝑓/𝑐
/𝑒        /𝑒     |
8 | | measvxrge0 29101 |
. . . . . 6
  measures 
          |
9 | 8 | adantlr 729 |
. . . . 5
   measures             |
10 | | simplr 770 |
. . . . 5
   measures      |
11 | 9, 10 | xrpxdivcld 28479 |
. . . 4
   measures         /𝑒       |
12 | | eqid 2471 |
. . . 4
      /𝑒         /𝑒    |
13 | 11, 12 | fmptd 6061 |
. . 3
  measures 


     /𝑒            |
14 | | measbase 29093 |
. . . . . . 7
 measures 
 sigAlgebra |
15 | | 0elsiga 29010 |
. . . . . . 7
  sigAlgebra   |
16 | 14, 15 | syl 17 |
. . . . . 6
 measures 
  |
17 | 16 | adantr 472 |
. . . . 5
  measures 

  |
18 | | ovex 6336 |
. . . . 5
     /𝑒   |
19 | | fveq2 5879 |
. . . . . . 7

          |
20 | 19 | oveq1d 6323 |
. . . . . 6

     /𝑒       /𝑒    |
21 | 20, 12 | fvmptg 5961 |
. . . . 5
 
     /𝑒          /𝑒           /𝑒    |
22 | 17, 18, 21 | sylancl 675 |
. . . 4
  measures 

       /𝑒           /𝑒    |
23 | | measvnul 29102 |
. . . . . 6
 measures 
      |
24 | 23 | oveq1d 6323 |
. . . . 5
 measures 
     /𝑒   /𝑒    |
25 | | xdiv0rp 28474 |
. . . . 5

 /𝑒    |
26 | 24, 25 | sylan9eq 2525 |
. . . 4
  measures 

     /𝑒    |
27 | 22, 26 | eqtrd 2505 |
. . 3
  measures 

       /𝑒        |
28 | | simpll 768 |
. . . . . 6
    measures 

  
Disj    measures 
   |
29 | | simplr 770 |
. . . . . 6
    measures 

  
Disj      |
30 | | simprl 772 |
. . . . . 6
    measures 

  
Disj     |
31 | | simprr 774 |
. . . . . 6
    measures 

  
Disj   Disj   |
32 | | vex 3034 |
. . . . . . . . . 10
 |
33 | 32 | a1i 11 |
. . . . . . . . 9
   measures       |
34 | | simplll 776 |
. . . . . . . . . 10
    measures 

   measures    |
35 | | selpw 3949 |
. . . . . . . . . . . 12
 
  |
36 | | ssel2 3413 |
. . . . . . . . . . . 12
 
   |
37 | 35, 36 | sylanb 480 |
. . . . . . . . . . 11
  

  |
38 | 37 | adantll 728 |
. . . . . . . . . 10
    measures 

     |
39 | | measvxrge0 29101 |
. . . . . . . . . 10
  measures 
          |
40 | 34, 38, 39 | syl2anc 673 |
. . . . . . . . 9
    measures 

            |
41 | | simplr 770 |
. . . . . . . . 9
   measures    
  |
42 | 33, 40, 41 | esumdivc 28978 |
. . . . . . . 8
   measures     Σ*      /𝑒 
Σ*      
/𝑒    |
43 | 42 | 3ad2antr1 1195 |
. . . . . . 7
   measures    
Disj   Σ*      /𝑒 
Σ*      
/𝑒    |
44 | 14 | ad2antrr 740 |
. . . . . . . . . 10
   measures    
Disj    sigAlgebra |
45 | | simpr1 1036 |
. . . . . . . . . 10
   measures    
Disj      |
46 | | simpr2 1037 |
. . . . . . . . . 10
   measures    
Disj     |
47 | | sigaclcu 29013 |
. . . . . . . . . 10
   sigAlgebra

    |
48 | 44, 45, 46, 47 | syl3anc 1292 |
. . . . . . . . 9
   measures    
Disj      |
49 | | fveq2 5879 |
. . . . . . . . . . 11
             |
50 | 49 | oveq1d 6323 |
. . . . . . . . . 10
      
/𝑒       
/𝑒    |
51 | | ovex 6336 |
. . . . . . . . . 10
     /𝑒   |
52 | 50, 12, 51 | fvmpt3i 5968 |
. . . . . . . . 9
 
      
/𝑒            
/𝑒    |
53 | 48, 52 | syl 17 |
. . . . . . . 8
   measures    
Disj          /𝑒            
/𝑒    |
54 | | simpll 768 |
. . . . . . . . . 10
   measures    
Disj   measures    |
55 | | simpr3 1038 |
. . . . . . . . . 10
   measures    
Disj   Disj   |
56 | | measvun 29105 |
. . . . . . . . . 10
  measures 


Disj        Σ*        |
57 | 54, 45, 46, 55, 56 | syl112anc 1296 |
. . . . . . . . 9
   measures    
Disj        Σ*        |
58 | 57 | oveq1d 6323 |
. . . . . . . 8
   measures    
Disj         /𝑒  Σ*     
/𝑒    |
59 | 53, 58 | eqtrd 2505 |
. . . . . . 7
   measures    
Disj          /𝑒       Σ*      /𝑒    |
60 | | fveq2 5879 |
. . . . . . . . . . . 12
           |
61 | 60 | oveq1d 6323 |
. . . . . . . . . . 11
      /𝑒       /𝑒    |
62 | 61, 12, 51 | fvmpt3i 5968 |
. . . . . . . . . 10
       
/𝑒           /𝑒    |
63 | 37, 62 | syl 17 |
. . . . . . . . 9
  

       /𝑒           /𝑒    |
64 | 63 | esumeq2dv 28933 |
. . . . . . . 8
  Σ*         /𝑒     
Σ*      
/𝑒    |
65 | 45, 64 | syl 17 |
. . . . . . 7
   measures    
Disj   Σ*        
/𝑒      Σ*       /𝑒    |
66 | 43, 59, 65 | 3eqtr4d 2515 |
. . . . . 6
   measures    
Disj          /𝑒       Σ*         /𝑒        |
67 | 28, 29, 30, 31, 66 | syl13anc 1294 |
. . . . 5
    measures 

  
Disj          /𝑒       Σ*         /𝑒        |
68 | 67 | ex 441 |
. . . 4
   measures       Disj 
       /𝑒       Σ*         /𝑒         |
69 | 68 | ralrimiva 2809 |
. . 3
  measures 

   
Disj         /𝑒      
Σ*         /𝑒         |
70 | | ismeas 29095 |
. . . . . 6
  sigAlgebra       
/𝑒   measures        
/𝑒         
      
/𝑒         
Disj        
/𝑒       Σ*         /𝑒           |
71 | 14, 70 | syl 17 |
. . . . 5
 measures 
       /𝑒   measures        
/𝑒         
      
/𝑒         
Disj        
/𝑒       Σ*         /𝑒           |
72 | 71 | biimprd 231 |
. . . 4
 measures 
       
/𝑒         
      
/𝑒         
Disj        
/𝑒       Σ*         /𝑒             
/𝑒   measures     |
73 | 72 | adantr 472 |
. . 3
  measures 

       
/𝑒         
      
/𝑒         
Disj        
/𝑒       Σ*         /𝑒             
/𝑒   measures     |
74 | 13, 27, 69, 73 | mp3and 1393 |
. 2
  measures 


     /𝑒   measures    |
75 | 7, 74 | eqeltrd 2549 |
1
  measures 

 ∘𝑓/𝑐
/𝑒  measures    |