Metamath Proof Explorer

Theorem itgeqa

Description: Approximate equality of integrals. If C ( x ) = D ( x ) for almost all x , then S. B C ( x )d x = S. B D ( x ) d x and one is integrable iff the other is. (Contributed by Mario Carneiro, 12-Aug-2014) (Revised by Mario Carneiro, 2-Sep-2014)

Ref Expression
Hypotheses itgeqa.1 
|- ( ( ph /\ x e. B ) -> C e. CC )
itgeqa.2 
|- ( ( ph /\ x e. B ) -> D e. CC )
itgeqa.3 
|- ( ph -> A C_ RR )
itgeqa.4 
|- ( ph -> ( vol* ` A ) = 0 )
itgeqa.5 
|- ( ( ph /\ x e. ( B \ A ) ) -> C = D )
Assertion itgeqa 
|- ( ph -> ( ( ( x e. B |-> C ) e. L^1 <-> ( x e. B |-> D ) e. L^1 ) /\ S. B C _d x = S. B D _d x ) )

Proof

Step Hyp Ref Expression
1 itgeqa.1 
 |-  ( ( ph /\ x e. B ) -> C e. CC )
2 itgeqa.2 
 |-  ( ( ph /\ x e. B ) -> D e. CC )
3 itgeqa.3 
 |-  ( ph -> A C_ RR )
4 itgeqa.4 
 |-  ( ph -> ( vol* ` A ) = 0 )
5 itgeqa.5 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> C = D )
6 3 4 5 1 2 mbfeqa 
 |-  ( ph -> ( ( x e. B |-> C ) e. MblFn <-> ( x e. B |-> D ) e. MblFn ) )
7 ifan 
 |-  if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 )
8 1 adantlr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> C e. CC )
9 ax-icn 
 |-  _i e. CC
10 ine0 
 |-  _i =/= 0
11 elfzelz 
 |-  ( k e. ( 0 ... 3 ) -> k e. ZZ )
12 11 ad2antlr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> k e. ZZ )
13 expclz 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( _i ^ k ) e. CC )
14 9 10 12 13 mp3an12i 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> ( _i ^ k ) e. CC )
15 expne0i 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( _i ^ k ) =/= 0 )
16 9 10 12 15 mp3an12i 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> ( _i ^ k ) =/= 0 )
17 8 14 16 divcld 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> ( C / ( _i ^ k ) ) e. CC )
18 17 recld 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> ( Re ` ( C / ( _i ^ k ) ) ) e. RR )
19 0re 
 |-  0 e. RR
20 ifcl 
 |-  ( ( ( Re ` ( C / ( _i ^ k ) ) ) e. RR /\ 0 e. RR ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. RR )
21 18 19 20 sylancl 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. RR )
22 21 rexrd 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. RR* )
23 max1 
 |-  ( ( 0 e. RR /\ ( Re ` ( C / ( _i ^ k ) ) ) e. RR ) -> 0 <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
24 19 18 23 sylancr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> 0 <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
25 elxrge0 
 |-  ( if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) <-> ( if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. RR* /\ 0 <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
26 22 24 25 sylanbrc 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) )
27 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
28 27 a1i 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. B ) -> 0 e. ( 0 [,] +oo ) )
29 26 28 ifclda 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) e. ( 0 [,] +oo ) )
30 7 29 eqeltrid 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) )
31 30 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) -> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) )
32 31 fmpttd 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
33 ifan 
 |-  if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) = if ( x e. B , if ( 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) , 0 )
34 2 adantlr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> D e. CC )
35 34 14 16 divcld 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> ( D / ( _i ^ k ) ) e. CC )
36 35 recld 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> ( Re ` ( D / ( _i ^ k ) ) ) e. RR )
37 ifcl 
 |-  ( ( ( Re ` ( D / ( _i ^ k ) ) ) e. RR /\ 0 e. RR ) -> if ( 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) e. RR )
38 36 19 37 sylancl 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> if ( 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) e. RR )
39 38 rexrd 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> if ( 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) e. RR* )
40 max1 
 |-  ( ( 0 e. RR /\ ( Re ` ( D / ( _i ^ k ) ) ) e. RR ) -> 0 <_ if ( 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) )
41 19 36 40 sylancr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> 0 <_ if ( 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) )
42 elxrge0 
 |-  ( if ( 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) <-> ( if ( 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) e. RR* /\ 0 <_ if ( 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) )
43 39 41 42 sylanbrc 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. B ) -> if ( 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) )
44 43 28 ifclda 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> if ( x e. B , if ( 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) , 0 ) e. ( 0 [,] +oo ) )
45 33 44 eqeltrid 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) )
46 45 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) -> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) )
47 46 fmpttd 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
48 3 adantr 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> A C_ RR )
49 4 adantr 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( vol* ` A ) = 0 )
50 simpll 
 |-  ( ( ( ph /\ x e. ( RR \ A ) ) /\ x e. B ) -> ph )
51 simpr 
 |-  ( ( ( ph /\ x e. ( RR \ A ) ) /\ x e. B ) -> x e. B )
52 eldifn 
 |-  ( x e. ( RR \ A ) -> -. x e. A )
53 52 ad2antlr 
 |-  ( ( ( ph /\ x e. ( RR \ A ) ) /\ x e. B ) -> -. x e. A )
54 51 53 eldifd 
 |-  ( ( ( ph /\ x e. ( RR \ A ) ) /\ x e. B ) -> x e. ( B \ A ) )
55 50 54 5 syl2anc 
 |-  ( ( ( ph /\ x e. ( RR \ A ) ) /\ x e. B ) -> C = D )
56 55 fvoveq1d 
 |-  ( ( ( ph /\ x e. ( RR \ A ) ) /\ x e. B ) -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( D / ( _i ^ k ) ) ) )
57 56 ibllem 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) )
58 eldifi 
 |-  ( x e. ( RR \ A ) -> x e. RR )
59 58 adantl 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> x e. RR )
60 fvex 
 |-  ( Re ` ( C / ( _i ^ k ) ) ) e. _V
61 c0ex 
 |-  0 e. _V
62 60 61 ifex 
 |-  if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. _V
63 eqid 
 |-  ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
64 63 fvmpt2 
 |-  ( ( x e. RR /\ if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. _V ) -> ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` x ) = if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
65 59 62 64 sylancl 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` x ) = if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
66 fvex 
 |-  ( Re ` ( D / ( _i ^ k ) ) ) e. _V
67 66 61 ifex 
 |-  if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) e. _V
68 eqid 
 |-  ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) )
69 68 fvmpt2 
 |-  ( ( x e. RR /\ if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) e. _V ) -> ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` x ) = if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) )
70 59 67 69 sylancl 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` x ) = if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) )
71 57 65 70 3eqtr4d 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` x ) = ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` x ) )
72 71 ralrimiva 
 |-  ( ph -> A. x e. ( RR \ A ) ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` x ) = ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` x ) )
73 nfv 
 |-  F/ y ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` x ) = ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` x )
74 nffvmpt1 
 |-  F/_ x ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` y )
75 nffvmpt1 
 |-  F/_ x ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` y )
76 74 75 nfeq 
 |-  F/ x ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` y ) = ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` y )
77 fveq2 
 |-  ( x = y -> ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` x ) = ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` y ) )
78 fveq2 
 |-  ( x = y -> ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` x ) = ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` y ) )
79 77 78 eqeq12d 
 |-  ( x = y -> ( ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` x ) = ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` x ) <-> ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` y ) = ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` y ) ) )
80 73 76 79 cbvralw 
 |-  ( A. x e. ( RR \ A ) ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` x ) = ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` x ) <-> A. y e. ( RR \ A ) ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` y ) = ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` y ) )
81 72 80 sylib 
 |-  ( ph -> A. y e. ( RR \ A ) ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` y ) = ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` y ) )
82 81 r19.21bi 
 |-  ( ( ph /\ y e. ( RR \ A ) ) -> ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` y ) = ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` y ) )
83 82 adantlr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ y e. ( RR \ A ) ) -> ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ` y ) = ( ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ` y ) )
84 32 47 48 49 83 itg2eqa 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ) )
85 84 eleq1d 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) )
86 85 ralbidva 
 |-  ( ph -> ( A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) )
87 6 86 anbi12d 
 |-  ( ph -> ( ( ( x e. B |-> C ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) <-> ( ( x e. B |-> D ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) ) )
88 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
89 eqidd 
 |-  ( ( ph /\ x e. B ) -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) ) )
90 88 89 1 isibl2 
 |-  ( ph -> ( ( x e. B |-> C ) e. L^1 <-> ( ( x e. B |-> C ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) ) )
91 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) )
92 eqidd 
 |-  ( ( ph /\ x e. B ) -> ( Re ` ( D / ( _i ^ k ) ) ) = ( Re ` ( D / ( _i ^ k ) ) ) )
93 91 92 2 isibl2 
 |-  ( ph -> ( ( x e. B |-> D ) e. L^1 <-> ( ( x e. B |-> D ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) ) )
94 87 90 93 3bitr4d 
 |-  ( ph -> ( ( x e. B |-> C ) e. L^1 <-> ( x e. B |-> D ) e. L^1 ) )
95 84 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ) ) )
96 95 sumeq2dv 
 |-  ( ph -> sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ) ) )
97 eqid 
 |-  ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) )
98 97 dfitg 
 |-  S. B C _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
99 eqid 
 |-  ( Re ` ( D / ( _i ^ k ) ) ) = ( Re ` ( D / ( _i ^ k ) ) )
100 99 dfitg 
 |-  S. B D _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ) )
101 96 98 100 3eqtr4g 
 |-  ( ph -> S. B C _d x = S. B D _d x )
102 94 101 jca 
 |-  ( ph -> ( ( ( x e. B |-> C ) e. L^1 <-> ( x e. B |-> D ) e. L^1 ) /\ S. B C _d x = S. B D _d x ) )