Metamath Proof Explorer

Theorem itgmulc2nclem1

Description: Lemma for itgmulc2nc ; cf. itgmulc2lem1 . (Contributed by Brendan Leahy, 17-Nov-2017)

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

Proof

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