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