MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg1mulc Structured version   Unicode version

Theorem itg1mulc 19597
Description: The integral of a constant times a simple function is the constant times the original integral. (Contributed by Mario Carneiro, 25-Jun-2014.)
Hypotheses
Ref Expression
i1fmulc.2  |-  ( ph  ->  F  e.  dom  S.1 )
i1fmulc.3  |-  ( ph  ->  A  e.  RR )
Assertion
Ref Expression
itg1mulc  |-  ( ph  ->  ( S.1 `  (
( RR  X.  { A } )  o F  x.  F ) )  =  ( A  x.  ( S.1 `  F ) ) )

Proof of Theorem itg1mulc
Dummy variables  k  m  n  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 itg10 19581 . . 3  |-  ( S.1 `  ( RR  X.  {
0 } ) )  =  0
2 reex 9082 . . . . . 6  |-  RR  e.  _V
32a1i 11 . . . . 5  |-  ( (
ph  /\  A  = 
0 )  ->  RR  e.  _V )
4 i1fmulc.2 . . . . . . 7  |-  ( ph  ->  F  e.  dom  S.1 )
5 i1ff 19569 . . . . . . 7  |-  ( F  e.  dom  S.1  ->  F : RR --> RR )
64, 5syl 16 . . . . . 6  |-  ( ph  ->  F : RR --> RR )
76adantr 453 . . . . 5  |-  ( (
ph  /\  A  = 
0 )  ->  F : RR --> RR )
8 i1fmulc.3 . . . . . 6  |-  ( ph  ->  A  e.  RR )
98adantr 453 . . . . 5  |-  ( (
ph  /\  A  = 
0 )  ->  A  e.  RR )
10 0re 9092 . . . . . 6  |-  0  e.  RR
1110a1i 11 . . . . 5  |-  ( (
ph  /\  A  = 
0 )  ->  0  e.  RR )
12 simplr 733 . . . . . . 7  |-  ( ( ( ph  /\  A  =  0 )  /\  x  e.  RR )  ->  A  =  0 )
1312oveq1d 6097 . . . . . 6  |-  ( ( ( ph  /\  A  =  0 )  /\  x  e.  RR )  ->  ( A  x.  x
)  =  ( 0  x.  x ) )
14 mul02lem2 9244 . . . . . . 7  |-  ( x  e.  RR  ->  (
0  x.  x )  =  0 )
1514adantl 454 . . . . . 6  |-  ( ( ( ph  /\  A  =  0 )  /\  x  e.  RR )  ->  ( 0  x.  x
)  =  0 )
1613, 15eqtrd 2469 . . . . 5  |-  ( ( ( ph  /\  A  =  0 )  /\  x  e.  RR )  ->  ( A  x.  x
)  =  0 )
173, 7, 9, 11, 16caofid2 6336 . . . 4  |-  ( (
ph  /\  A  = 
0 )  ->  (
( RR  X.  { A } )  o F  x.  F )  =  ( RR  X.  {
0 } ) )
1817fveq2d 5733 . . 3  |-  ( (
ph  /\  A  = 
0 )  ->  ( S.1 `  ( ( RR 
X.  { A }
)  o F  x.  F ) )  =  ( S.1 `  ( RR  X.  { 0 } ) ) )
19 simpr 449 . . . . 5  |-  ( (
ph  /\  A  = 
0 )  ->  A  =  0 )
2019oveq1d 6097 . . . 4  |-  ( (
ph  /\  A  = 
0 )  ->  ( A  x.  ( S.1 `  F ) )  =  ( 0  x.  ( S.1 `  F ) ) )
21 itg1cl 19578 . . . . . . . 8  |-  ( F  e.  dom  S.1  ->  ( S.1 `  F )  e.  RR )
224, 21syl 16 . . . . . . 7  |-  ( ph  ->  ( S.1 `  F
)  e.  RR )
2322recnd 9115 . . . . . 6  |-  ( ph  ->  ( S.1 `  F
)  e.  CC )
2423mul02d 9265 . . . . 5  |-  ( ph  ->  ( 0  x.  ( S.1 `  F ) )  =  0 )
2524adantr 453 . . . 4  |-  ( (
ph  /\  A  = 
0 )  ->  (
0  x.  ( S.1 `  F ) )  =  0 )
2620, 25eqtrd 2469 . . 3  |-  ( (
ph  /\  A  = 
0 )  ->  ( A  x.  ( S.1 `  F ) )  =  0 )
271, 18, 263eqtr4a 2495 . 2  |-  ( (
ph  /\  A  = 
0 )  ->  ( S.1 `  ( ( RR 
X.  { A }
)  o F  x.  F ) )  =  ( A  x.  ( S.1 `  F ) ) )
284, 8i1fmulc 19596 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( RR  X.  { A } )  o F  x.  F )  e.  dom  S.1 )
2928adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  A  =/=  0 )  ->  (
( RR  X.  { A } )  o F  x.  F )  e. 
dom  S.1 )
30 i1ff 19569 . . . . . . . . . . . . 13  |-  ( ( ( RR  X.  { A } )  o F  x.  F )  e. 
dom  S.1  ->  ( ( RR  X.  { A }
)  o F  x.  F ) : RR --> RR )
3129, 30syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  A  =/=  0 )  ->  (
( RR  X.  { A } )  o F  x.  F ) : RR --> RR )
32 frn 5598 . . . . . . . . . . . 12  |-  ( ( ( RR  X.  { A } )  o F  x.  F ) : RR --> RR  ->  ran  ( ( RR  X.  { A } )  o F  x.  F ) 
C_  RR )
3331, 32syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  0 )  ->  ran  ( ( RR  X.  { A } )  o F  x.  F ) 
C_  RR )
3433ssdifssd 3486 . . . . . . . . . 10  |-  ( (
ph  /\  A  =/=  0 )  ->  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  C_  RR )
3534sselda 3349 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  m  e.  RR )
3635recnd 9115 . . . . . . . 8  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  m  e.  CC )
378adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  A  =/=  0 )  ->  A  e.  RR )
3837recnd 9115 . . . . . . . . 9  |-  ( (
ph  /\  A  =/=  0 )  ->  A  e.  CC )
3938adantr 453 . . . . . . . 8  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  A  e.  CC )
40 simplr 733 . . . . . . . 8  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  A  =/=  0 )
4136, 39, 40divcan2d 9793 . . . . . . 7  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( A  x.  ( m  /  A
) )  =  m )
424, 8i1fmulclem 19595 . . . . . . . . . 10  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  RR )  ->  ( `' ( ( RR 
X.  { A }
)  o F  x.  F ) " {
m } )  =  ( `' F " { ( m  /  A ) } ) )
4335, 42syldan 458 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( `' ( ( RR  X.  { A } )  o F  x.  F )
" { m }
)  =  ( `' F " { ( m  /  A ) } ) )
4443fveq2d 5733 . . . . . . . 8  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( vol `  ( `' ( ( RR  X.  { A } )  o F  x.  F ) " { m } ) )  =  ( vol `  ( `' F " { ( m  /  A ) } ) ) )
4544eqcomd 2442 . . . . . . 7  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( vol `  ( `' F " { ( m  /  A ) } ) )  =  ( vol `  ( `' ( ( RR  X.  { A } )  o F  x.  F ) " { m } ) ) )
4641, 45oveq12d 6100 . . . . . 6  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( ( A  x.  ( m  /  A ) )  x.  ( vol `  ( `' F " { ( m  /  A ) } ) ) )  =  ( m  x.  ( vol `  ( `' ( ( RR 
X.  { A }
)  o F  x.  F ) " {
m } ) ) ) )
478ad2antrr 708 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  A  e.  RR )
4835, 47, 40redivcld 9843 . . . . . . . 8  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( m  /  A )  e.  RR )
4948recnd 9115 . . . . . . 7  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( m  /  A )  e.  CC )
504ad2antrr 708 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  F  e.  dom  S.1 )
5147recnd 9115 . . . . . . . . . . 11  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  A  e.  CC )
52 eldifsni 3929 . . . . . . . . . . . 12  |-  ( m  e.  ( ran  (
( RR  X.  { A } )  o F  x.  F )  \  { 0 } )  ->  m  =/=  0
)
5352adantl 454 . . . . . . . . . . 11  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  m  =/=  0 )
5436, 51, 53, 40divne0d 9807 . . . . . . . . . 10  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( m  /  A )  =/=  0
)
55 eldifsn 3928 . . . . . . . . . 10  |-  ( ( m  /  A )  e.  ( RR  \  { 0 } )  <-> 
( ( m  /  A )  e.  RR  /\  ( m  /  A
)  =/=  0 ) )
5648, 54, 55sylanbrc 647 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( m  /  A )  e.  ( RR  \  { 0 } ) )
57 i1fima2sn 19573 . . . . . . . . 9  |-  ( ( F  e.  dom  S.1  /\  ( m  /  A
)  e.  ( RR 
\  { 0 } ) )  ->  ( vol `  ( `' F " { ( m  /  A ) } ) )  e.  RR )
5850, 56, 57syl2anc 644 . . . . . . . 8  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( vol `  ( `' F " { ( m  /  A ) } ) )  e.  RR )
5958recnd 9115 . . . . . . 7  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( vol `  ( `' F " { ( m  /  A ) } ) )  e.  CC )
6039, 49, 59mulassd 9112 . . . . . 6  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( ( A  x.  ( m  /  A ) )  x.  ( vol `  ( `' F " { ( m  /  A ) } ) ) )  =  ( A  x.  ( ( m  /  A )  x.  ( vol `  ( `' F " { ( m  /  A ) } ) ) ) ) )
6146, 60eqtr3d 2471 . . . . 5  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( m  x.  ( vol `  ( `' ( ( RR 
X.  { A }
)  o F  x.  F ) " {
m } ) ) )  =  ( A  x.  ( ( m  /  A )  x.  ( vol `  ( `' F " { ( m  /  A ) } ) ) ) ) )
6261sumeq2dv 12498 . . . 4  |-  ( (
ph  /\  A  =/=  0 )  ->  sum_ m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) ( m  x.  ( vol `  ( `' ( ( RR  X.  { A } )  o F  x.  F ) " { m } ) ) )  =  sum_ m  e.  ( ran  (
( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) ( A  x.  (
( m  /  A
)  x.  ( vol `  ( `' F " { ( m  /  A ) } ) ) ) ) )
63 i1frn 19570 . . . . . . 7  |-  ( ( ( RR  X.  { A } )  o F  x.  F )  e. 
dom  S.1  ->  ran  ( ( RR  X.  { A } )  o F  x.  F )  e. 
Fin )
6429, 63syl 16 . . . . . 6  |-  ( (
ph  /\  A  =/=  0 )  ->  ran  ( ( RR  X.  { A } )  o F  x.  F )  e.  Fin )
65 difss 3475 . . . . . 6  |-  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  C_  ran  ( ( RR  X.  { A } )  o F  x.  F )
66 ssfi 7330 . . . . . 6  |-  ( ( ran  ( ( RR 
X.  { A }
)  o F  x.  F )  e.  Fin  /\  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) 
C_  ran  ( ( RR  X.  { A }
)  o F  x.  F ) )  -> 
( ran  ( ( RR  X.  { A }
)  o F  x.  F )  \  {
0 } )  e. 
Fin )
6764, 65, 66sylancl 645 . . . . 5  |-  ( (
ph  /\  A  =/=  0 )  ->  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  e.  Fin )
6849, 59mulcld 9109 . . . . 5  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( (
m  /  A )  x.  ( vol `  ( `' F " { ( m  /  A ) } ) ) )  e.  CC )
6967, 38, 68fsummulc2 12568 . . . 4  |-  ( (
ph  /\  A  =/=  0 )  ->  ( A  x.  sum_ m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) ( ( m  /  A )  x.  ( vol `  ( `' F " { ( m  /  A ) } ) ) ) )  = 
sum_ m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } ) ( A  x.  ( ( m  /  A )  x.  ( vol `  ( `' F " { ( m  /  A ) } ) ) ) ) )
7062, 69eqtr4d 2472 . . 3  |-  ( (
ph  /\  A  =/=  0 )  ->  sum_ m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) ( m  x.  ( vol `  ( `' ( ( RR  X.  { A } )  o F  x.  F ) " { m } ) ) )  =  ( A  x.  sum_ m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) ( ( m  /  A )  x.  ( vol `  ( `' F " { ( m  /  A ) } ) ) ) ) )
71 itg1val 19576 . . . 4  |-  ( ( ( RR  X.  { A } )  o F  x.  F )  e. 
dom  S.1  ->  ( S.1 `  ( ( RR  X.  { A } )  o F  x.  F ) )  =  sum_ m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) ( m  x.  ( vol `  ( `' ( ( RR  X.  { A } )  o F  x.  F ) " { m } ) ) ) )
7229, 71syl 16 . . 3  |-  ( (
ph  /\  A  =/=  0 )  ->  ( S.1 `  ( ( RR 
X.  { A }
)  o F  x.  F ) )  = 
sum_ m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } ) ( m  x.  ( vol `  ( `' ( ( RR 
X.  { A }
)  o F  x.  F ) " {
m } ) ) ) )
734adantr 453 . . . . . 6  |-  ( (
ph  /\  A  =/=  0 )  ->  F  e.  dom  S.1 )
74 itg1val 19576 . . . . . 6  |-  ( F  e.  dom  S.1  ->  ( S.1 `  F )  =  sum_ k  e.  ( ran  F  \  {
0 } ) ( k  x.  ( vol `  ( `' F " { k } ) ) ) )
7573, 74syl 16 . . . . 5  |-  ( (
ph  /\  A  =/=  0 )  ->  ( S.1 `  F )  = 
sum_ k  e.  ( ran  F  \  {
0 } ) ( k  x.  ( vol `  ( `' F " { k } ) ) ) )
76 id 21 . . . . . . 7  |-  ( k  =  ( m  /  A )  ->  k  =  ( m  /  A ) )
77 sneq 3826 . . . . . . . . 9  |-  ( k  =  ( m  /  A )  ->  { k }  =  { ( m  /  A ) } )
7877imaeq2d 5204 . . . . . . . 8  |-  ( k  =  ( m  /  A )  ->  ( `' F " { k } )  =  ( `' F " { ( m  /  A ) } ) )
7978fveq2d 5733 . . . . . . 7  |-  ( k  =  ( m  /  A )  ->  ( vol `  ( `' F " { k } ) )  =  ( vol `  ( `' F " { ( m  /  A ) } ) ) )
8076, 79oveq12d 6100 . . . . . 6  |-  ( k  =  ( m  /  A )  ->  (
k  x.  ( vol `  ( `' F " { k } ) ) )  =  ( ( m  /  A
)  x.  ( vol `  ( `' F " { ( m  /  A ) } ) ) ) )
81 eqid 2437 . . . . . . 7  |-  ( n  e.  ( ran  (
( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) 
|->  ( n  /  A
) )  =  ( n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  |->  ( n  /  A ) )
82 eldifi 3470 . . . . . . . . 9  |-  ( n  e.  ( ran  (
( RR  X.  { A } )  o F  x.  F )  \  { 0 } )  ->  n  e.  ran  ( ( RR  X.  { A } )  o F  x.  F ) )
832a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  RR  e.  _V )
84 ffn 5592 . . . . . . . . . . . . . . . . . 18  |-  ( F : RR --> RR  ->  F  Fn  RR )
856, 84syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  F  Fn  RR )
86 eqidd 2438 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 y )  =  ( F `  y
) )
8783, 8, 85, 86ofc1 6328 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( ( RR  X.  { A } )  o F  x.  F ) `  y )  =  ( A  x.  ( F `
 y ) ) )
8887adantlr 697 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  A  =/=  0 )  /\  y  e.  RR )  ->  (
( ( RR  X.  { A } )  o F  x.  F ) `
 y )  =  ( A  x.  ( F `  y )
) )
8988oveq1d 6097 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  A  =/=  0 )  /\  y  e.  RR )  ->  (
( ( ( RR 
X.  { A }
)  o F  x.  F ) `  y
)  /  A )  =  ( ( A  x.  ( F `  y ) )  /  A ) )
906adantr 453 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  A  =/=  0 )  ->  F : RR --> RR )
9190ffvelrnda 5871 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  A  =/=  0 )  /\  y  e.  RR )  ->  ( F `  y )  e.  RR )
9291recnd 9115 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  A  =/=  0 )  /\  y  e.  RR )  ->  ( F `  y )  e.  CC )
9338adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  A  =/=  0 )  /\  y  e.  RR )  ->  A  e.  CC )
94 simplr 733 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  A  =/=  0 )  /\  y  e.  RR )  ->  A  =/=  0 )
9592, 93, 94divcan3d 9796 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  A  =/=  0 )  /\  y  e.  RR )  ->  (
( A  x.  ( F `  y )
)  /  A )  =  ( F `  y ) )
9689, 95eqtrd 2469 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  A  =/=  0 )  /\  y  e.  RR )  ->  (
( ( ( RR 
X.  { A }
)  o F  x.  F ) `  y
)  /  A )  =  ( F `  y ) )
9790, 84syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  A  =/=  0 )  ->  F  Fn  RR )
98 fnfvelrn 5868 . . . . . . . . . . . . . 14  |-  ( ( F  Fn  RR  /\  y  e.  RR )  ->  ( F `  y
)  e.  ran  F
)
9997, 98sylan 459 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  A  =/=  0 )  /\  y  e.  RR )  ->  ( F `  y )  e.  ran  F )
10096, 99eqeltrd 2511 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  A  =/=  0 )  /\  y  e.  RR )  ->  (
( ( ( RR 
X.  { A }
)  o F  x.  F ) `  y
)  /  A )  e.  ran  F )
101100ralrimiva 2790 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  0 )  ->  A. y  e.  RR  ( ( ( ( RR  X.  { A } )  o F  x.  F ) `  y )  /  A
)  e.  ran  F
)
102 ffn 5592 . . . . . . . . . . . . 13  |-  ( ( ( RR  X.  { A } )  o F  x.  F ) : RR --> RR  ->  (
( RR  X.  { A } )  o F  x.  F )  Fn  RR )
10331, 102syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  A  =/=  0 )  ->  (
( RR  X.  { A } )  o F  x.  F )  Fn  RR )
104 oveq1 6089 . . . . . . . . . . . . . 14  |-  ( n  =  ( ( ( RR  X.  { A } )  o F  x.  F ) `  y )  ->  (
n  /  A )  =  ( ( ( ( RR  X.  { A } )  o F  x.  F ) `  y )  /  A
) )
105104eleq1d 2503 . . . . . . . . . . . . 13  |-  ( n  =  ( ( ( RR  X.  { A } )  o F  x.  F ) `  y )  ->  (
( n  /  A
)  e.  ran  F  <->  ( ( ( ( RR 
X.  { A }
)  o F  x.  F ) `  y
)  /  A )  e.  ran  F ) )
106105ralrn 5874 . . . . . . . . . . . 12  |-  ( ( ( RR  X.  { A } )  o F  x.  F )  Fn  RR  ->  ( A. n  e.  ran  ( ( RR  X.  { A } )  o F  x.  F ) ( n  /  A )  e.  ran  F  <->  A. y  e.  RR  ( ( ( ( RR  X.  { A } )  o F  x.  F ) `  y )  /  A
)  e.  ran  F
) )
107103, 106syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  0 )  ->  ( A. n  e.  ran  ( ( RR  X.  { A } )  o F  x.  F ) ( n  /  A
)  e.  ran  F  <->  A. y  e.  RR  (
( ( ( RR 
X.  { A }
)  o F  x.  F ) `  y
)  /  A )  e.  ran  F ) )
108101, 107mpbird 225 . . . . . . . . . 10  |-  ( (
ph  /\  A  =/=  0 )  ->  A. n  e.  ran  ( ( RR 
X.  { A }
)  o F  x.  F ) ( n  /  A )  e. 
ran  F )
109108r19.21bi 2805 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  n  e.  ran  ( ( RR 
X.  { A }
)  o F  x.  F ) )  -> 
( n  /  A
)  e.  ran  F
)
11082, 109sylan2 462 . . . . . . . 8  |-  ( ( ( ph  /\  A  =/=  0 )  /\  n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( n  /  A )  e.  ran  F )
11134sselda 3349 . . . . . . . . . 10  |-  ( ( ( ph  /\  A  =/=  0 )  /\  n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  n  e.  RR )
112111recnd 9115 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  n  e.  CC )
11338adantr 453 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  A  e.  CC )
114 eldifsni 3929 . . . . . . . . . 10  |-  ( n  e.  ( ran  (
( RR  X.  { A } )  o F  x.  F )  \  { 0 } )  ->  n  =/=  0
)
115114adantl 454 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  n  =/=  0 )
116 simplr 733 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  A  =/=  0 )
117112, 113, 115, 116divne0d 9807 . . . . . . . 8  |-  ( ( ( ph  /\  A  =/=  0 )  /\  n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( n  /  A )  =/=  0
)
118 eldifsn 3928 . . . . . . . 8  |-  ( ( n  /  A )  e.  ( ran  F  \  { 0 } )  <-> 
( ( n  /  A )  e.  ran  F  /\  ( n  /  A )  =/=  0
) )
119110, 117, 118sylanbrc 647 . . . . . . 7  |-  ( ( ( ph  /\  A  =/=  0 )  /\  n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( n  /  A )  e.  ( ran  F  \  {
0 } ) )
120 eldifi 3470 . . . . . . . . 9  |-  ( k  e.  ( ran  F  \  { 0 } )  ->  k  e.  ran  F )
121 fnfvelrn 5868 . . . . . . . . . . . . . 14  |-  ( ( ( ( RR  X.  { A } )  o F  x.  F )  Fn  RR  /\  y  e.  RR )  ->  (
( ( RR  X.  { A } )  o F  x.  F ) `
 y )  e. 
ran  ( ( RR 
X.  { A }
)  o F  x.  F ) )
122103, 121sylan 459 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  A  =/=  0 )  /\  y  e.  RR )  ->  (
( ( RR  X.  { A } )  o F  x.  F ) `
 y )  e. 
ran  ( ( RR 
X.  { A }
)  o F  x.  F ) )
12388, 122eqeltrrd 2512 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  A  =/=  0 )  /\  y  e.  RR )  ->  ( A  x.  ( F `  y ) )  e. 
ran  ( ( RR 
X.  { A }
)  o F  x.  F ) )
124123ralrimiva 2790 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  0 )  ->  A. y  e.  RR  ( A  x.  ( F `  y ) )  e.  ran  (
( RR  X.  { A } )  o F  x.  F ) )
125 oveq2 6090 . . . . . . . . . . . . . 14  |-  ( k  =  ( F `  y )  ->  ( A  x.  k )  =  ( A  x.  ( F `  y ) ) )
126125eleq1d 2503 . . . . . . . . . . . . 13  |-  ( k  =  ( F `  y )  ->  (
( A  x.  k
)  e.  ran  (
( RR  X.  { A } )  o F  x.  F )  <->  ( A  x.  ( F `  y
) )  e.  ran  ( ( RR  X.  { A } )  o F  x.  F ) ) )
127126ralrn 5874 . . . . . . . . . . . 12  |-  ( F  Fn  RR  ->  ( A. k  e.  ran  F ( A  x.  k
)  e.  ran  (
( RR  X.  { A } )  o F  x.  F )  <->  A. y  e.  RR  ( A  x.  ( F `  y ) )  e.  ran  (
( RR  X.  { A } )  o F  x.  F ) ) )
12897, 127syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  0 )  ->  ( A. k  e.  ran  F ( A  x.  k
)  e.  ran  (
( RR  X.  { A } )  o F  x.  F )  <->  A. y  e.  RR  ( A  x.  ( F `  y ) )  e.  ran  (
( RR  X.  { A } )  o F  x.  F ) ) )
129124, 128mpbird 225 . . . . . . . . . 10  |-  ( (
ph  /\  A  =/=  0 )  ->  A. k  e.  ran  F ( A  x.  k )  e. 
ran  ( ( RR 
X.  { A }
)  o F  x.  F ) )
130129r19.21bi 2805 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  ran  F )  -> 
( A  x.  k
)  e.  ran  (
( RR  X.  { A } )  o F  x.  F ) )
131120, 130sylan2 462 . . . . . . . 8  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( A  x.  k )  e.  ran  ( ( RR  X.  { A } )  o F  x.  F ) )
13238adantr 453 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  A  e.  CC )
133 frn 5598 . . . . . . . . . . . . 13  |-  ( F : RR --> RR  ->  ran 
F  C_  RR )
13490, 133syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  A  =/=  0 )  ->  ran  F 
C_  RR )
135134ssdifssd 3486 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  0 )  ->  ( ran  F  \  { 0 } )  C_  RR )
136135sselda 3349 . . . . . . . . . 10  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  k  e.  RR )
137136recnd 9115 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  k  e.  CC )
138 simplr 733 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  A  =/=  0 )
139 eldifsni 3929 . . . . . . . . . 10  |-  ( k  e.  ( ran  F  \  { 0 } )  ->  k  =/=  0
)
140139adantl 454 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  k  =/=  0 )
141132, 137, 138, 140mulne0d 9675 . . . . . . . 8  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( A  x.  k )  =/=  0
)
142 eldifsn 3928 . . . . . . . 8  |-  ( ( A  x.  k )  e.  ( ran  (
( RR  X.  { A } )  o F  x.  F )  \  { 0 } )  <-> 
( ( A  x.  k )  e.  ran  ( ( RR  X.  { A } )  o F  x.  F )  /\  ( A  x.  k )  =/=  0
) )
143131, 141, 142sylanbrc 647 . . . . . . 7  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( A  x.  k )  e.  ( ran  ( ( RR 
X.  { A }
)  o F  x.  F )  \  {
0 } ) )
144 simpl 445 . . . . . . . . . . . 12  |-  ( ( n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  n  e.  ( ran  ( ( RR 
X.  { A }
)  o F  x.  F )  \  {
0 } ) )
145 ssel2 3344 . . . . . . . . . . . 12  |-  ( ( ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) 
C_  RR  /\  n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  n  e.  RR )
14634, 144, 145syl2an 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  A  =/=  0 )  /\  (
n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  /\  k  e.  ( ran  F  \  { 0 } ) ) )  ->  n  e.  RR )
147146recnd 9115 . . . . . . . . . 10  |-  ( ( ( ph  /\  A  =/=  0 )  /\  (
n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  /\  k  e.  ( ran  F  \  { 0 } ) ) )  ->  n  e.  CC )
1488ad2antrr 708 . . . . . . . . . . 11  |-  ( ( ( ph  /\  A  =/=  0 )  /\  (
n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  /\  k  e.  ( ran  F  \  { 0 } ) ) )  ->  A  e.  RR )
149148recnd 9115 . . . . . . . . . 10  |-  ( ( ( ph  /\  A  =/=  0 )  /\  (
n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  /\  k  e.  ( ran  F  \  { 0 } ) ) )  ->  A  e.  CC )
150136adantrl 698 . . . . . . . . . . 11  |-  ( ( ( ph  /\  A  =/=  0 )  /\  (
n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  /\  k  e.  ( ran  F  \  { 0 } ) ) )  ->  k  e.  RR )
151150recnd 9115 . . . . . . . . . 10  |-  ( ( ( ph  /\  A  =/=  0 )  /\  (
n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  /\  k  e.  ( ran  F  \  { 0 } ) ) )  ->  k  e.  CC )
152 simplr 733 . . . . . . . . . 10  |-  ( ( ( ph  /\  A  =/=  0 )  /\  (
n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  /\  k  e.  ( ran  F  \  { 0 } ) ) )  ->  A  =/=  0 )
153147, 149, 151, 152divmuld 9813 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  (
n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  /\  k  e.  ( ran  F  \  { 0 } ) ) )  ->  (
( n  /  A
)  =  k  <->  ( A  x.  k )  =  n ) )
154153bicomd 194 . . . . . . . 8  |-  ( ( ( ph  /\  A  =/=  0 )  /\  (
n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  /\  k  e.  ( ran  F  \  { 0 } ) ) )  ->  (
( A  x.  k
)  =  n  <->  ( n  /  A )  =  k ) )
155 eqcom 2439 . . . . . . . 8  |-  ( n  =  ( A  x.  k )  <->  ( A  x.  k )  =  n )
156 eqcom 2439 . . . . . . . 8  |-  ( k  =  ( n  /  A )  <->  ( n  /  A )  =  k )
157154, 155, 1563bitr4g 281 . . . . . . 7  |-  ( ( ( ph  /\  A  =/=  0 )  /\  (
n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  /\  k  e.  ( ran  F  \  { 0 } ) ) )  ->  (
n  =  ( A  x.  k )  <->  k  =  ( n  /  A
) ) )
15881, 119, 143, 157f1o2d 6297 . . . . . 6  |-  ( (
ph  /\  A  =/=  0 )  ->  (
n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  |->  ( n  /  A ) ) : ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) -1-1-onto-> ( ran  F  \  {
0 } ) )
159 oveq1 6089 . . . . . . . 8  |-  ( n  =  m  ->  (
n  /  A )  =  ( m  /  A ) )
160 ovex 6107 . . . . . . . 8  |-  ( m  /  A )  e. 
_V
161159, 81, 160fvmpt 5807 . . . . . . 7  |-  ( m  e.  ( ran  (
( RR  X.  { A } )  o F  x.  F )  \  { 0 } )  ->  ( ( n  e.  ( ran  (
( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) 
|->  ( n  /  A
) ) `  m
)  =  ( m  /  A ) )
162161adantl 454 . . . . . 6  |-  ( ( ( ph  /\  A  =/=  0 )  /\  m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) )  ->  ( (
n  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } )  |->  ( n  /  A ) ) `  m )  =  ( m  /  A ) )
163 i1fima2sn 19573 . . . . . . . . 9  |-  ( ( F  e.  dom  S.1  /\  k  e.  ( ran 
F  \  { 0 } ) )  -> 
( vol `  ( `' F " { k } ) )  e.  RR )
16473, 163sylan 459 . . . . . . . 8  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( vol `  ( `' F " { k } ) )  e.  RR )
165136, 164remulcld 9117 . . . . . . 7  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( k  x.  ( vol `  ( `' F " { k } ) ) )  e.  RR )
166165recnd 9115 . . . . . 6  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  ( ran  F  \  { 0 } ) )  ->  ( k  x.  ( vol `  ( `' F " { k } ) ) )  e.  CC )
16780, 67, 158, 162, 166fsumf1o 12518 . . . . 5  |-  ( (
ph  /\  A  =/=  0 )  ->  sum_ k  e.  ( ran  F  \  { 0 } ) ( k  x.  ( vol `  ( `' F " { k } ) ) )  =  sum_ m  e.  ( ran  (
( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) ( ( m  /  A )  x.  ( vol `  ( `' F " { ( m  /  A ) } ) ) ) )
16875, 167eqtrd 2469 . . . 4  |-  ( (
ph  /\  A  =/=  0 )  ->  ( S.1 `  F )  = 
sum_ m  e.  ( ran  ( ( RR  X.  { A } )  o F  x.  F ) 
\  { 0 } ) ( ( m  /  A )  x.  ( vol `  ( `' F " { ( m  /  A ) } ) ) ) )
169168oveq2d 6098 . . 3  |-  ( (
ph  /\  A  =/=  0 )  ->  ( A  x.  ( S.1 `  F ) )  =  ( A  x.  sum_ m  e.  ( ran  (
( RR  X.  { A } )  o F  x.  F )  \  { 0 } ) ( ( m  /  A )  x.  ( vol `  ( `' F " { ( m  /  A ) } ) ) ) ) )
17070, 72, 1693eqtr4d 2479 . 2  |-  ( (
ph  /\  A  =/=  0 )  ->  ( S.1 `  ( ( RR 
X.  { A }
)  o F  x.  F ) )  =  ( A  x.  ( S.1 `  F ) ) )
17127, 170pm2.61dane 2683 1  |-  ( ph  ->  ( S.1 `  (
( RR  X.  { A } )  o F  x.  F ) )  =  ( A  x.  ( S.1 `  F ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726    =/= wne 2600   A.wral 2706   _Vcvv 2957    \ cdif 3318    C_ wss 3321   {csn 3815    e. cmpt 4267    X. cxp 4877   `'ccnv 4878   dom cdm 4879   ran crn 4880   "cima 4882    Fn wfn 5450   -->wf 5451   ` cfv 5455  (class class class)co 6082    o Fcof 6304   Fincfn 7110   CCcc 8989   RRcr 8990   0cc0 8991    x. cmul 8996    / cdiv 9678   sum_csu 12480   volcvol 19361   S.1citg1 19508
This theorem is referenced by:  itg1sub  19602  itg2const  19633  itg2mulclem  19639  itg2monolem1  19643  itg2addnclem  26257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-rep 4321  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-inf2 7597  ax-cnex 9047  ax-resscn 9048  ax-1cn 9049  ax-icn 9050  ax-addcl 9051  ax-addrcl 9052  ax-mulcl 9053  ax-mulrcl 9054  ax-mulcom 9055  ax-addass 9056  ax-mulass 9057  ax-distr 9058  ax-i2m1 9059  ax-1ne0 9060  ax-1rid 9061  ax-rnegex 9062  ax-rrecex 9063  ax-cnre 9064  ax-pre-lttri 9065  ax-pre-lttrn 9066  ax-pre-ltadd 9067  ax-pre-mulgt0 9068  ax-pre-sup 9069
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2711  df-rex 2712  df-reu 2713  df-rmo 2714  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-int 4052  df-iun 4096  df-br 4214  df-opab 4268  df-mpt 4269  df-tr 4304  df-eprel 4495  df-id 4499  df-po 4504  df-so 4505  df-fr 4542  df-se 4543  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-isom 5464  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-of 6306  df-1st 6350  df-2nd 6351  df-riota 6550  df-recs 6634  df-rdg 6669  df-1o 6725  df-2o 6726  df-oadd 6729  df-er 6906  df-map 7021  df-pm 7022  df-en 7111  df-dom 7112  df-sdom 7113  df-fin 7114  df-sup 7447  df-oi 7480  df-card 7827  df-cda 8049  df-pnf 9123  df-mnf 9124  df-xr 9125  df-ltxr 9126  df-le 9127  df-sub 9294  df-neg 9295  df-div 9679  df-nn 10002  df-2 10059  df-3 10060  df-n0 10223  df-z 10284  df-uz 10490  df-q 10576  df-rp 10614  df-xadd 10712  df-ioo 10921  df-ico 10923  df-icc 10924  df-fz 11045  df-fzo 11137  df-fl 11203  df-seq 11325  df-exp 11384  df-hash 11620  df-cj 11905  df-re 11906  df-im 11907  df-sqr 12041  df-abs 12042  df-clim 12283  df-sum 12481  df-xmet 16696  df-met 16697  df-ovol 19362  df-vol 19363  df-mbf 19513  df-itg1 19514
  Copyright terms: Public domain W3C validator