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 syl5bir
 |-  ( 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 ) ) )