Metamath Proof Explorer

Theorem itg2add

Description: The S.2 integral is linear. (Measurability is an essential component of this theorem; otherwise consider the characteristic function of a nonmeasurable set and its complement.) (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses itg2add.f1 
|- ( ph -> F e. MblFn )
itg2add.f2 
|- ( ph -> F : RR --> ( 0 [,) +oo ) )
itg2add.f3 
|- ( ph -> ( S.2 ` F ) e. RR )
itg2add.g1 
|- ( ph -> G e. MblFn )
itg2add.g2 
|- ( ph -> G : RR --> ( 0 [,) +oo ) )
itg2add.g3 
|- ( ph -> ( S.2 ` G ) e. RR )
Assertion itg2add 
|- ( ph -> ( S.2 ` ( F oF + G ) ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )

Proof

Step Hyp Ref Expression
1 itg2add.f1 
 |-  ( ph -> F e. MblFn )
2 itg2add.f2 
 |-  ( ph -> F : RR --> ( 0 [,) +oo ) )
3 itg2add.f3 
 |-  ( ph -> ( S.2 ` F ) e. RR )
4 itg2add.g1 
 |-  ( ph -> G e. MblFn )
5 itg2add.g2 
 |-  ( ph -> G : RR --> ( 0 [,) +oo ) )
6 itg2add.g3 
 |-  ( ph -> ( S.2 ` G ) e. RR )
7 1 2 mbfi1fseq 
 |-  ( ph -> E. f ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) )
8 4 5 mbfi1fseq 
 |-  ( ph -> E. g ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) )
9 exdistrv 
 |-  ( E. f E. g ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) <-> ( E. f ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ E. g ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) )
10 1 adantr 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) ) -> F e. MblFn )
11 2 adantr 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) ) -> F : RR --> ( 0 [,) +oo ) )
12 3 adantr 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) ) -> ( S.2 ` F ) e. RR )
13 4 adantr 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) ) -> G e. MblFn )
14 5 adantr 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) ) -> G : RR --> ( 0 [,) +oo ) )
15 6 adantr 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) ) -> ( S.2 ` G ) e. RR )
16 simprl1 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) ) -> f : NN --> dom S.1 )
17 simprl2 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) ) -> A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) )
18 simprl3 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) ) -> A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) )
19 simprr1 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) ) -> g : NN --> dom S.1 )
20 simprr2 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) ) -> A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) )
21 simprr3 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) ) -> A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) )
22 10 11 12 13 14 15 16 17 18 19 20 21 itg2addlem 
 |-  ( ( ph /\ ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) ) -> ( S.2 ` ( F oF + G ) ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )
23 22 ex 
 |-  ( ph -> ( ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) -> ( S.2 ` ( F oF + G ) ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) ) )
24 23 exlimdvv 
 |-  ( ph -> ( E. f E. g ( ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) -> ( S.2 ` ( F oF + G ) ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) ) )
25 9 24 biimtrrid 
 |-  ( ph -> ( ( E. f ( f : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( f ` n ) /\ ( f ` n ) oR <_ ( f ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( f ` n ) ` x ) ) ~~> ( F ` x ) ) /\ E. g ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( G ` x ) ) ) -> ( S.2 ` ( F oF + G ) ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) ) )
26 7 8 25 mp2and 
 |-  ( ph -> ( S.2 ` ( F oF + G ) ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )