Metamath Proof Explorer


Theorem itgre

Description: Real part of an integral. (Contributed by Mario Carneiro, 14-Aug-2014)

Ref Expression
Hypotheses itgcnval.1
|- ( ( ph /\ x e. A ) -> B e. V )
itgcnval.2
|- ( ph -> ( x e. A |-> B ) e. L^1 )
Assertion itgre
|- ( ph -> ( Re ` S. A B _d x ) = S. A ( Re ` B ) _d x )

Proof

Step Hyp Ref Expression
1 itgcnval.1
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 itgcnval.2
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
3 1 2 itgcnval
 |-  ( ph -> S. A B _d x = ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) )
4 3 fveq2d
 |-  ( ph -> ( Re ` S. A B _d x ) = ( Re ` ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) ) )
5 iblmbf
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
6 2 5 syl
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
7 6 1 mbfmptcl
 |-  ( ( ph /\ x e. A ) -> B e. CC )
8 7 recld
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. RR )
9 7 iblcn
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) ) )
10 2 9 mpbid
 |-  ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) )
11 10 simpld
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) e. L^1 )
12 8 11 itgrecl
 |-  ( ph -> S. A ( Re ` B ) _d x e. RR )
13 7 imcld
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. RR )
14 10 simprd
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) e. L^1 )
15 13 14 itgrecl
 |-  ( ph -> S. A ( Im ` B ) _d x e. RR )
16 12 15 crred
 |-  ( ph -> ( Re ` ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) ) = S. A ( Re ` B ) _d x )
17 4 16 eqtrd
 |-  ( ph -> ( Re ` S. A B _d x ) = S. A ( Re ` B ) _d x )