Metamath Proof Explorer

Theorem itg2const

Description: Integral of a constant function. (Contributed by Mario Carneiro, 12-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion itg2const 
|- ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) = ( B x. ( vol ` A ) ) )

Proof

Step Hyp Ref Expression
1 reex 
 |-  RR e. _V
2 1 a1i 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> RR e. _V )
3 simpl3 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) /\ x e. RR ) -> B e. ( 0 [,) +oo ) )
4 1re 
 |-  1 e. RR
5 0re 
 |-  0 e. RR
6 4 5 ifcli 
 |-  if ( x e. A , 1 , 0 ) e. RR
7 6 a1i 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) /\ x e. RR ) -> if ( x e. A , 1 , 0 ) e. RR )
8 fconstmpt 
 |-  ( RR X. { B } ) = ( x e. RR |-> B )
9 8 a1i 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( RR X. { B } ) = ( x e. RR |-> B ) )
10 eqidd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( x e. RR |-> if ( x e. A , 1 , 0 ) ) = ( x e. RR |-> if ( x e. A , 1 , 0 ) ) )
11 2 3 7 9 10 offval2 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( ( RR X. { B } ) oF x. ( x e. RR |-> if ( x e. A , 1 , 0 ) ) ) = ( x e. RR |-> ( B x. if ( x e. A , 1 , 0 ) ) ) )
12 ovif2 
 |-  ( B x. if ( x e. A , 1 , 0 ) ) = if ( x e. A , ( B x. 1 ) , ( B x. 0 ) )
13 simp3 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> B e. ( 0 [,) +oo ) )
14 elrege0 
 |-  ( B e. ( 0 [,) +oo ) <-> ( B e. RR /\ 0 <_ B ) )
15 13 14 sylib 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( B e. RR /\ 0 <_ B ) )
16 15 simpld 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> B e. RR )
17 16 recnd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> B e. CC )
18 17 mulridd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( B x. 1 ) = B )
19 17 mul01d 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( B x. 0 ) = 0 )
20 18 19 ifeq12d 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> if ( x e. A , ( B x. 1 ) , ( B x. 0 ) ) = if ( x e. A , B , 0 ) )
21 12 20 eqtrid 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( B x. if ( x e. A , 1 , 0 ) ) = if ( x e. A , B , 0 ) )
22 21 mpteq2dv 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( x e. RR |-> ( B x. if ( x e. A , 1 , 0 ) ) ) = ( x e. RR |-> if ( x e. A , B , 0 ) ) )
23 11 22 eqtrd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( ( RR X. { B } ) oF x. ( x e. RR |-> if ( x e. A , 1 , 0 ) ) ) = ( x e. RR |-> if ( x e. A , B , 0 ) ) )
24 eqid 
 |-  ( x e. RR |-> if ( x e. A , 1 , 0 ) ) = ( x e. RR |-> if ( x e. A , 1 , 0 ) )
25 24 i1f1 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> ( x e. RR |-> if ( x e. A , 1 , 0 ) ) e. dom S.1 )
26 25 3adant3 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( x e. RR |-> if ( x e. A , 1 , 0 ) ) e. dom S.1 )
27 26 16 i1fmulc 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( ( RR X. { B } ) oF x. ( x e. RR |-> if ( x e. A , 1 , 0 ) ) ) e. dom S.1 )
28 23 27 eqeltrrd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( x e. RR |-> if ( x e. A , B , 0 ) ) e. dom S.1 )
29 15 simprd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> 0 <_ B )
30 0le0 
 |-  0 <_ 0
31 breq2 
 |-  ( B = if ( x e. A , B , 0 ) -> ( 0 <_ B <-> 0 <_ if ( x e. A , B , 0 ) ) )
32 breq2 
 |-  ( 0 = if ( x e. A , B , 0 ) -> ( 0 <_ 0 <-> 0 <_ if ( x e. A , B , 0 ) ) )
33 31 32 ifboth 
 |-  ( ( 0 <_ B /\ 0 <_ 0 ) -> 0 <_ if ( x e. A , B , 0 ) )
34 29 30 33 sylancl 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> 0 <_ if ( x e. A , B , 0 ) )
35 34 ralrimivw 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> A. x e. RR 0 <_ if ( x e. A , B , 0 ) )
36 ax-resscn 
 |-  RR C_ CC
37 36 a1i 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> RR C_ CC )
38 16 adantr 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) /\ x e. RR ) -> B e. RR )
39 ifcl 
 |-  ( ( B e. RR /\ 0 e. RR ) -> if ( x e. A , B , 0 ) e. RR )
40 38 5 39 sylancl 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) /\ x e. RR ) -> if ( x e. A , B , 0 ) e. RR )
41 40 ralrimiva 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> A. x e. RR if ( x e. A , B , 0 ) e. RR )
42 eqid 
 |-  ( x e. RR |-> if ( x e. A , B , 0 ) ) = ( x e. RR |-> if ( x e. A , B , 0 ) )
43 42 fnmpt 
 |-  ( A. x e. RR if ( x e. A , B , 0 ) e. RR -> ( x e. RR |-> if ( x e. A , B , 0 ) ) Fn RR )
44 41 43 syl 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( x e. RR |-> if ( x e. A , B , 0 ) ) Fn RR )
45 37 44 0pledm 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( 0p oR <_ ( x e. RR |-> if ( x e. A , B , 0 ) ) <-> ( RR X. { 0 } ) oR <_ ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
46 5 a1i 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) /\ x e. RR ) -> 0 e. RR )
47 fconstmpt 
 |-  ( RR X. { 0 } ) = ( x e. RR |-> 0 )
48 47 a1i 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( RR X. { 0 } ) = ( x e. RR |-> 0 ) )
49 eqidd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( x e. RR |-> if ( x e. A , B , 0 ) ) = ( x e. RR |-> if ( x e. A , B , 0 ) ) )
50 2 46 40 48 49 ofrfval2 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( ( RR X. { 0 } ) oR <_ ( x e. RR |-> if ( x e. A , B , 0 ) ) <-> A. x e. RR 0 <_ if ( x e. A , B , 0 ) ) )
51 45 50 bitrd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( 0p oR <_ ( x e. RR |-> if ( x e. A , B , 0 ) ) <-> A. x e. RR 0 <_ if ( x e. A , B , 0 ) ) )
52 35 51 mpbird 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> 0p oR <_ ( x e. RR |-> if ( x e. A , B , 0 ) ) )
53 itg2itg1 
 |-  ( ( ( x e. RR |-> if ( x e. A , B , 0 ) ) e. dom S.1 /\ 0p oR <_ ( x e. RR |-> if ( x e. A , B , 0 ) ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) = ( S.1 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
54 28 52 53 syl2anc 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) = ( S.1 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
55 26 16 itg1mulc 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( S.1 ` ( ( RR X. { B } ) oF x. ( x e. RR |-> if ( x e. A , 1 , 0 ) ) ) ) = ( B x. ( S.1 ` ( x e. RR |-> if ( x e. A , 1 , 0 ) ) ) ) )
56 23 fveq2d 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( S.1 ` ( ( RR X. { B } ) oF x. ( x e. RR |-> if ( x e. A , 1 , 0 ) ) ) ) = ( S.1 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
57 24 itg11 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> ( S.1 ` ( x e. RR |-> if ( x e. A , 1 , 0 ) ) ) = ( vol ` A ) )
58 57 3adant3 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( S.1 ` ( x e. RR |-> if ( x e. A , 1 , 0 ) ) ) = ( vol ` A ) )
59 58 oveq2d 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( B x. ( S.1 ` ( x e. RR |-> if ( x e. A , 1 , 0 ) ) ) ) = ( B x. ( vol ` A ) ) )
60 55 56 59 3eqtr3d 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( S.1 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) = ( B x. ( vol ` A ) ) )
61 54 60 eqtrd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) = ( B x. ( vol ` A ) ) )