Metamath Proof Explorer

Theorem itgmulc2lem1

Description: Lemma for itgmulc2 : positive real case. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgmulc2.1 
|- ( ph -> C e. CC )
itgmulc2.2 
|- ( ( ph /\ x e. A ) -> B e. V )
itgmulc2.3 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
itgmulc2.4 
|- ( ph -> C e. RR )
itgmulc2.5 
|- ( ( ph /\ x e. A ) -> B e. RR )
itgmulc2.6 
|- ( ph -> 0 <_ C )
itgmulc2.7 
|- ( ( ph /\ x e. A ) -> 0 <_ B )
Assertion itgmulc2lem1 
|- ( ph -> ( C x. S. A B _d x ) = S. A ( C x. B ) _d x )

Proof

Step Hyp Ref Expression
1 itgmulc2.1 
 |-  ( ph -> C e. CC )
2 itgmulc2.2 
 |-  ( ( ph /\ x e. A ) -> B e. V )
3 itgmulc2.3 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
4 itgmulc2.4 
 |-  ( ph -> C e. RR )
5 itgmulc2.5 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
6 itgmulc2.6 
 |-  ( ph -> 0 <_ C )
7 itgmulc2.7 
 |-  ( ( ph /\ x e. A ) -> 0 <_ B )
8 elrege0 
 |-  ( B e. ( 0 [,) +oo ) <-> ( B e. RR /\ 0 <_ B ) )
9 5 7 8 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> B e. ( 0 [,) +oo ) )
10 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
11 10 a1i 
 |-  ( ( ph /\ -. x e. A ) -> 0 e. ( 0 [,) +oo ) )
12 9 11 ifclda 
 |-  ( ph -> if ( x e. A , B , 0 ) e. ( 0 [,) +oo ) )
13 12 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , B , 0 ) e. ( 0 [,) +oo ) )
14 13 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , B , 0 ) ) : RR --> ( 0 [,) +oo ) )
15 5 7 iblpos 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) ) )
16 3 15 mpbid 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) )
17 16 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR )
18 elrege0 
 |-  ( C e. ( 0 [,) +oo ) <-> ( C e. RR /\ 0 <_ C ) )
19 4 6 18 sylanbrc 
 |-  ( ph -> C e. ( 0 [,) +oo ) )
20 14 17 19 itg2mulc 
 |-  ( ph -> ( S.2 ` ( ( RR X. { C } ) oF x. ( x e. RR |-> if ( x e. A , B , 0 ) ) ) ) = ( C x. ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) ) )
21 reex 
 |-  RR e. _V
22 21 a1i 
 |-  ( ph -> RR e. _V )
23 4 adantr 
 |-  ( ( ph /\ x e. RR ) -> C e. RR )
24 fconstmpt 
 |-  ( RR X. { C } ) = ( x e. RR |-> C )
25 24 a1i 
 |-  ( ph -> ( RR X. { C } ) = ( x e. RR |-> C ) )
26 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , B , 0 ) ) = ( x e. RR |-> if ( x e. A , B , 0 ) ) )
27 22 23 13 25 26 offval2 
 |-  ( ph -> ( ( RR X. { C } ) oF x. ( x e. RR |-> if ( x e. A , B , 0 ) ) ) = ( x e. RR |-> ( C x. if ( x e. A , B , 0 ) ) ) )
28 ovif2 
 |-  ( C x. if ( x e. A , B , 0 ) ) = if ( x e. A , ( C x. B ) , ( C x. 0 ) )
29 1 mul01d 
 |-  ( ph -> ( C x. 0 ) = 0 )
30 29 adantr 
 |-  ( ( ph /\ x e. RR ) -> ( C x. 0 ) = 0 )
31 30 ifeq2d 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , ( C x. B ) , ( C x. 0 ) ) = if ( x e. A , ( C x. B ) , 0 ) )
32 28 31 eqtrid 
 |-  ( ( ph /\ x e. RR ) -> ( C x. if ( x e. A , B , 0 ) ) = if ( x e. A , ( C x. B ) , 0 ) )
33 32 mpteq2dva 
 |-  ( ph -> ( x e. RR |-> ( C x. if ( x e. A , B , 0 ) ) ) = ( x e. RR |-> if ( x e. A , ( C x. B ) , 0 ) ) )
34 27 33 eqtrd 
 |-  ( ph -> ( ( RR X. { C } ) oF x. ( x e. RR |-> if ( x e. A , B , 0 ) ) ) = ( x e. RR |-> if ( x e. A , ( C x. B ) , 0 ) ) )
35 34 fveq2d 
 |-  ( ph -> ( S.2 ` ( ( RR X. { C } ) oF x. ( x e. RR |-> if ( x e. A , B , 0 ) ) ) ) = ( S.2 ` ( x e. RR |-> if ( x e. A , ( C x. B ) , 0 ) ) ) )
36 20 35 eqtr3d 
 |-  ( ph -> ( C x. ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) ) = ( S.2 ` ( x e. RR |-> if ( x e. A , ( C x. B ) , 0 ) ) ) )
37 5 3 7 itgposval 
 |-  ( ph -> S. A B _d x = ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
38 37 oveq2d 
 |-  ( ph -> ( C x. S. A B _d x ) = ( C x. ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) ) )
39 4 adantr 
 |-  ( ( ph /\ x e. A ) -> C e. RR )
40 39 5 remulcld 
 |-  ( ( ph /\ x e. A ) -> ( C x. B ) e. RR )
41 1 2 3 iblmulc2 
 |-  ( ph -> ( x e. A |-> ( C x. B ) ) e. L^1 )
42 6 adantr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ C )
43 39 5 42 7 mulge0d 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( C x. B ) )
44 40 41 43 itgposval 
 |-  ( ph -> S. A ( C x. B ) _d x = ( S.2 ` ( x e. RR |-> if ( x e. A , ( C x. B ) , 0 ) ) ) )
45 36 38 44 3eqtr4d 
 |-  ( ph -> ( C x. S. A B _d x ) = S. A ( C x. B ) _d x )