Metamath Proof Explorer

Theorem itgsplit

Description: The S. integral splits under an almost disjoint union. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itgsplit.i 
|- ( ph -> ( vol* ` ( A i^i B ) ) = 0 )
itgsplit.u 
|- ( ph -> U = ( A u. B ) )
itgsplit.c 
|- ( ( ph /\ x e. U ) -> C e. V )
itgsplit.a 
|- ( ph -> ( x e. A |-> C ) e. L^1 )
itgsplit.b 
|- ( ph -> ( x e. B |-> C ) e. L^1 )
Assertion itgsplit 
|- ( ph -> S. U C _d x = ( S. A C _d x + S. B C _d x ) )

Proof

Step Hyp Ref Expression
1 itgsplit.i 
 |-  ( ph -> ( vol* ` ( A i^i B ) ) = 0 )
2 itgsplit.u 
 |-  ( ph -> U = ( A u. B ) )
3 itgsplit.c 
 |-  ( ( ph /\ x e. U ) -> C e. V )
4 itgsplit.a 
 |-  ( ph -> ( x e. A |-> C ) e. L^1 )
5 itgsplit.b 
 |-  ( ph -> ( x e. B |-> C ) e. L^1 )
6 iblmbf 
 |-  ( ( x e. A |-> C ) e. L^1 -> ( x e. A |-> C ) e. MblFn )
7 4 6 syl 
 |-  ( ph -> ( x e. A |-> C ) e. MblFn )
8 ssun1 
 |-  A C_ ( A u. B )
9 8 2 sseqtrrid 
 |-  ( ph -> A C_ U )
10 9 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. U )
11 10 3 syldan 
 |-  ( ( ph /\ x e. A ) -> C e. V )
12 7 11 mbfdm2 
 |-  ( ph -> A e. dom vol )
13 12 adantr 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> A e. dom vol )
14 iblmbf 
 |-  ( ( x e. B |-> C ) e. L^1 -> ( x e. B |-> C ) e. MblFn )
15 5 14 syl 
 |-  ( ph -> ( x e. B |-> C ) e. MblFn )
16 ssun2 
 |-  B C_ ( A u. B )
17 16 2 sseqtrrid 
 |-  ( ph -> B C_ U )
18 17 sselda 
 |-  ( ( ph /\ x e. B ) -> x e. U )
19 18 3 syldan 
 |-  ( ( ph /\ x e. B ) -> C e. V )
20 15 19 mbfdm2 
 |-  ( ph -> B e. dom vol )
21 20 adantr 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> B e. dom vol )
22 1 adantr 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( vol* ` ( A i^i B ) ) = 0 )
23 2 adantr 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> U = ( A u. B ) )
24 2 eleq2d 
 |-  ( ph -> ( x e. U <-> x e. ( A u. B ) ) )
25 elun 
 |-  ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
26 24 25 bitrdi 
 |-  ( ph -> ( x e. U <-> ( x e. A \/ x e. B ) ) )
27 26 biimpa 
 |-  ( ( ph /\ x e. U ) -> ( x e. A \/ x e. B ) )
28 7 11 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
29 15 19 mbfmptcl 
 |-  ( ( ph /\ x e. B ) -> C e. CC )
30 28 29 jaodan 
 |-  ( ( ph /\ ( x e. A \/ x e. B ) ) -> C e. CC )
31 27 30 syldan 
 |-  ( ( ph /\ x e. U ) -> C e. CC )
32 31 adantlr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> C e. CC )
33 ax-icn 
 |-  _i e. CC
34 elfznn0 
 |-  ( k e. ( 0 ... 3 ) -> k e. NN0 )
35 34 adantl 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> k e. NN0 )
36 expcl 
 |-  ( ( _i e. CC /\ k e. NN0 ) -> ( _i ^ k ) e. CC )
37 33 35 36 sylancr 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( _i ^ k ) e. CC )
38 37 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> ( _i ^ k ) e. CC )
39 ine0 
 |-  _i =/= 0
40 elfzelz 
 |-  ( k e. ( 0 ... 3 ) -> k e. ZZ )
41 40 adantl 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> k e. ZZ )
42 expne0i 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( _i ^ k ) =/= 0 )
43 33 39 41 42 mp3an12i 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( _i ^ k ) =/= 0 )
44 43 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> ( _i ^ k ) =/= 0 )
45 32 38 44 divcld 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> ( C / ( _i ^ k ) ) e. CC )
46 45 recld 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> ( Re ` ( C / ( _i ^ k ) ) ) e. RR )
47 0re 
 |-  0 e. RR
48 ifcl 
 |-  ( ( ( Re ` ( C / ( _i ^ k ) ) ) e. RR /\ 0 e. RR ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. RR )
49 46 47 48 sylancl 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. RR )
50 49 rexrd 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. RR* )
51 max1 
 |-  ( ( 0 e. RR /\ ( Re ` ( C / ( _i ^ k ) ) ) e. RR ) -> 0 <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
52 47 46 51 sylancr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> 0 <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
53 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 ) ) )
54 50 52 53 sylanbrc 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) )
55 ifan 
 |-  if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 )
56 55 mpteq2i 
 |-  ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) )
57 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 )
58 57 mpteq2i 
 |-  ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) )
59 ifan 
 |-  if ( ( x e. U /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( x e. U , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 )
60 59 mpteq2i 
 |-  ( x e. RR |-> if ( ( x e. U /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( x e. U , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) )
61 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
62 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) ) )
63 61 62 4 11 iblitg 
 |-  ( ( ph /\ k e. ZZ ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
64 40 63 sylan2 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
65 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 ) ) )
66 eqidd 
 |-  ( ( ph /\ x e. B ) -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) ) )
67 65 66 5 19 iblitg 
 |-  ( ( ph /\ k e. ZZ ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
68 40 67 sylan2 
 |-  ( ( 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 )
69 13 21 22 23 54 56 58 60 64 68 itg2split 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. U /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) + ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) )
70 69 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. U /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( ( _i ^ k ) x. ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) + ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) ) )
71 63 recnd 
 |-  ( ( ph /\ k e. ZZ ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. CC )
72 40 71 sylan2 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. CC )
73 68 recnd 
 |-  ( ( 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. CC )
74 37 72 73 adddid 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( ( _i ^ k ) x. ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) + ( 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. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) + ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) ) )
75 70 74 eqtrd 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. U /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) + ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) ) )
76 75 sumeq2dv 
 |-  ( ph -> sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. U /\ 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. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) + ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) ) )
77 fzfid 
 |-  ( ph -> ( 0 ... 3 ) e. Fin )
78 37 72 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) e. CC )
79 37 73 mulcld 
 |-  ( ( 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 ) ) ) ) e. CC )
80 77 78 79 fsumadd 
 |-  ( ph -> sum_ k e. ( 0 ... 3 ) ( ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) + ( ( _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. A /\ 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 ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) ) )
81 76 80 eqtrd 
 |-  ( ph -> sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. U /\ 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. A /\ 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 ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) ) )
82 eqid 
 |-  ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) )
83 82 dfitg 
 |-  S. U C _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. U /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
84 82 dfitg 
 |-  S. A C _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
85 82 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 ) ) ) )
86 84 85 oveq12i 
 |-  ( S. A C _d x + S. B C _d x ) = ( sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 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 ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) )
87 81 83 86 3eqtr4g 
 |-  ( ph -> S. U C _d x = ( S. A C _d x + S. B C _d x ) )