Metamath Proof Explorer

Theorem itgconst

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

Ref Expression
Assertion itgconst 
|- ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> S. A B _d x = ( B x. ( vol ` A ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( y = ( Re ` B ) /\ x e. A ) -> y = ( Re ` B ) )
2 1 itgeq2dv 
 |-  ( y = ( Re ` B ) -> S. A y _d x = S. A ( Re ` B ) _d x )
3 oveq1 
 |-  ( y = ( Re ` B ) -> ( y x. ( vol ` A ) ) = ( ( Re ` B ) x. ( vol ` A ) ) )
4 2 3 eqeq12d 
 |-  ( y = ( Re ` B ) -> ( S. A y _d x = ( y x. ( vol ` A ) ) <-> S. A ( Re ` B ) _d x = ( ( Re ` B ) x. ( vol ` A ) ) ) )
5 simplr 
 |-  ( ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) /\ x e. A ) -> y e. RR )
6 fconstmpt 
 |-  ( A X. { y } ) = ( x e. A |-> y )
7 simpl1 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> A e. dom vol )
8 simp2 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( vol ` A ) e. RR )
9 8 adantr 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> ( vol ` A ) e. RR )
10 simpr 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> y e. RR )
11 10 recnd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> y e. CC )
12 iblconst 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ y e. CC ) -> ( A X. { y } ) e. L^1 )
13 7 9 11 12 syl3anc 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> ( A X. { y } ) e. L^1 )
14 6 13 eqeltrrid 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> ( x e. A |-> y ) e. L^1 )
15 5 14 itgrevallem1 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> S. A y _d x = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u y ) , -u y , 0 ) ) ) ) )
16 ifan 
 |-  if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = if ( x e. A , if ( 0 <_ y , y , 0 ) , 0 )
17 16 mpteq2i 
 |-  ( x e. RR |-> if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) = ( x e. RR |-> if ( x e. A , if ( 0 <_ y , y , 0 ) , 0 ) )
18 17 fveq2i 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ y , y , 0 ) , 0 ) ) )
19 0re 
 |-  0 e. RR
20 ifcl 
 |-  ( ( y e. RR /\ 0 e. RR ) -> if ( 0 <_ y , y , 0 ) e. RR )
21 10 19 20 sylancl 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> if ( 0 <_ y , y , 0 ) e. RR )
22 max1 
 |-  ( ( 0 e. RR /\ y e. RR ) -> 0 <_ if ( 0 <_ y , y , 0 ) )
23 19 10 22 sylancr 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> 0 <_ if ( 0 <_ y , y , 0 ) )
24 elrege0 
 |-  ( if ( 0 <_ y , y , 0 ) e. ( 0 [,) +oo ) <-> ( if ( 0 <_ y , y , 0 ) e. RR /\ 0 <_ if ( 0 <_ y , y , 0 ) ) )
25 21 23 24 sylanbrc 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> if ( 0 <_ y , y , 0 ) e. ( 0 [,) +oo ) )
26 itg2const 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ if ( 0 <_ y , y , 0 ) e. ( 0 [,) +oo ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ y , y , 0 ) , 0 ) ) ) = ( if ( 0 <_ y , y , 0 ) x. ( vol ` A ) ) )
27 7 9 25 26 syl3anc 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ y , y , 0 ) , 0 ) ) ) = ( if ( 0 <_ y , y , 0 ) x. ( vol ` A ) ) )
28 18 27 syl5eq 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) = ( if ( 0 <_ y , y , 0 ) x. ( vol ` A ) ) )
29 ifan 
 |-  if ( ( x e. A /\ 0 <_ -u y ) , -u y , 0 ) = if ( x e. A , if ( 0 <_ -u y , -u y , 0 ) , 0 )
30 29 mpteq2i 
 |-  ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u y ) , -u y , 0 ) ) = ( x e. RR |-> if ( x e. A , if ( 0 <_ -u y , -u y , 0 ) , 0 ) )
31 30 fveq2i 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u y ) , -u y , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ -u y , -u y , 0 ) , 0 ) ) )
32 renegcl 
 |-  ( y e. RR -> -u y e. RR )
33 32 adantl 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> -u y e. RR )
34 ifcl 
 |-  ( ( -u y e. RR /\ 0 e. RR ) -> if ( 0 <_ -u y , -u y , 0 ) e. RR )
35 33 19 34 sylancl 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> if ( 0 <_ -u y , -u y , 0 ) e. RR )
36 max1 
 |-  ( ( 0 e. RR /\ -u y e. RR ) -> 0 <_ if ( 0 <_ -u y , -u y , 0 ) )
37 19 33 36 sylancr 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> 0 <_ if ( 0 <_ -u y , -u y , 0 ) )
38 elrege0 
 |-  ( if ( 0 <_ -u y , -u y , 0 ) e. ( 0 [,) +oo ) <-> ( if ( 0 <_ -u y , -u y , 0 ) e. RR /\ 0 <_ if ( 0 <_ -u y , -u y , 0 ) ) )
39 35 37 38 sylanbrc 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> if ( 0 <_ -u y , -u y , 0 ) e. ( 0 [,) +oo ) )
40 itg2const 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ if ( 0 <_ -u y , -u y , 0 ) e. ( 0 [,) +oo ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ -u y , -u y , 0 ) , 0 ) ) ) = ( if ( 0 <_ -u y , -u y , 0 ) x. ( vol ` A ) ) )
41 7 9 39 40 syl3anc 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ -u y , -u y , 0 ) , 0 ) ) ) = ( if ( 0 <_ -u y , -u y , 0 ) x. ( vol ` A ) ) )
42 31 41 syl5eq 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u y ) , -u y , 0 ) ) ) = ( if ( 0 <_ -u y , -u y , 0 ) x. ( vol ` A ) ) )
43 28 42 oveq12d 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u y ) , -u y , 0 ) ) ) ) = ( ( if ( 0 <_ y , y , 0 ) x. ( vol ` A ) ) - ( if ( 0 <_ -u y , -u y , 0 ) x. ( vol ` A ) ) ) )
44 21 recnd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> if ( 0 <_ y , y , 0 ) e. CC )
45 35 recnd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> if ( 0 <_ -u y , -u y , 0 ) e. CC )
46 8 recnd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( vol ` A ) e. CC )
47 46 adantr 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> ( vol ` A ) e. CC )
48 44 45 47 subdird 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> ( ( if ( 0 <_ y , y , 0 ) - if ( 0 <_ -u y , -u y , 0 ) ) x. ( vol ` A ) ) = ( ( if ( 0 <_ y , y , 0 ) x. ( vol ` A ) ) - ( if ( 0 <_ -u y , -u y , 0 ) x. ( vol ` A ) ) ) )
49 max0sub 
 |-  ( y e. RR -> ( if ( 0 <_ y , y , 0 ) - if ( 0 <_ -u y , -u y , 0 ) ) = y )
50 49 adantl 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> ( if ( 0 <_ y , y , 0 ) - if ( 0 <_ -u y , -u y , 0 ) ) = y )
51 50 oveq1d 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> ( ( if ( 0 <_ y , y , 0 ) - if ( 0 <_ -u y , -u y , 0 ) ) x. ( vol ` A ) ) = ( y x. ( vol ` A ) ) )
52 43 48 51 3eqtr2rd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> ( y x. ( vol ` A ) ) = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u y ) , -u y , 0 ) ) ) ) )
53 15 52 eqtr4d 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ y e. RR ) -> S. A y _d x = ( y x. ( vol ` A ) ) )
54 53 ralrimiva 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> A. y e. RR S. A y _d x = ( y x. ( vol ` A ) ) )
55 recl 
 |-  ( B e. CC -> ( Re ` B ) e. RR )
56 55 3ad2ant3 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( Re ` B ) e. RR )
57 4 54 56 rspcdva 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> S. A ( Re ` B ) _d x = ( ( Re ` B ) x. ( vol ` A ) ) )
58 simpl 
 |-  ( ( y = ( Im ` B ) /\ x e. A ) -> y = ( Im ` B ) )
59 58 itgeq2dv 
 |-  ( y = ( Im ` B ) -> S. A y _d x = S. A ( Im ` B ) _d x )
60 oveq1 
 |-  ( y = ( Im ` B ) -> ( y x. ( vol ` A ) ) = ( ( Im ` B ) x. ( vol ` A ) ) )
61 59 60 eqeq12d 
 |-  ( y = ( Im ` B ) -> ( S. A y _d x = ( y x. ( vol ` A ) ) <-> S. A ( Im ` B ) _d x = ( ( Im ` B ) x. ( vol ` A ) ) ) )
62 imcl 
 |-  ( B e. CC -> ( Im ` B ) e. RR )
63 62 3ad2ant3 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( Im ` B ) e. RR )
64 61 54 63 rspcdva 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> S. A ( Im ` B ) _d x = ( ( Im ` B ) x. ( vol ` A ) ) )
65 64 oveq2d 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( _i x. S. A ( Im ` B ) _d x ) = ( _i x. ( ( Im ` B ) x. ( vol ` A ) ) ) )
66 ax-icn 
 |-  _i e. CC
67 66 a1i 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> _i e. CC )
68 63 recnd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( Im ` B ) e. CC )
69 67 68 46 mulassd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( ( _i x. ( Im ` B ) ) x. ( vol ` A ) ) = ( _i x. ( ( Im ` B ) x. ( vol ` A ) ) ) )
70 65 69 eqtr4d 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( _i x. S. A ( Im ` B ) _d x ) = ( ( _i x. ( Im ` B ) ) x. ( vol ` A ) ) )
71 57 70 oveq12d 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) = ( ( ( Re ` B ) x. ( vol ` A ) ) + ( ( _i x. ( Im ` B ) ) x. ( vol ` A ) ) ) )
72 56 recnd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( Re ` B ) e. CC )
73 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` B ) e. CC ) -> ( _i x. ( Im ` B ) ) e. CC )
74 66 68 73 sylancr 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( _i x. ( Im ` B ) ) e. CC )
75 72 74 46 adddird 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) x. ( vol ` A ) ) = ( ( ( Re ` B ) x. ( vol ` A ) ) + ( ( _i x. ( Im ` B ) ) x. ( vol ` A ) ) ) )
76 71 75 eqtr4d 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) = ( ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) x. ( vol ` A ) ) )
77 simpl3 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ x e. A ) -> B e. CC )
78 fconstmpt 
 |-  ( A X. { B } ) = ( x e. A |-> B )
79 iblconst 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( A X. { B } ) e. L^1 )
80 78 79 eqeltrrid 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( x e. A |-> B ) e. L^1 )
81 77 80 itgcnval 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> S. A B _d x = ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) )
82 replim 
 |-  ( B e. CC -> B = ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) )
83 82 3ad2ant3 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> B = ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) )
84 83 oveq1d 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( B x. ( vol ` A ) ) = ( ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) x. ( vol ` A ) ) )
85 76 81 84 3eqtr4d 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> S. A B _d x = ( B x. ( vol ` A ) ) )