Step |
Hyp |
Ref |
Expression |
1 |
|
cbvitg.1 |
|- ( x = y -> B = C ) |
2 |
|
cbvitg.2 |
|- F/_ y B |
3 |
|
cbvitg.3 |
|- F/_ x C |
4 |
|
nfv |
|- F/ y x e. A |
5 |
|
nfcv |
|- F/_ y 0 |
6 |
|
nfcv |
|- F/_ y <_ |
7 |
|
nfcv |
|- F/_ y Re |
8 |
|
nfcv |
|- F/_ y / |
9 |
|
nfcv |
|- F/_ y ( _i ^ k ) |
10 |
2 8 9
|
nfov |
|- F/_ y ( B / ( _i ^ k ) ) |
11 |
7 10
|
nffv |
|- F/_ y ( Re ` ( B / ( _i ^ k ) ) ) |
12 |
5 6 11
|
nfbr |
|- F/ y 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) |
13 |
4 12
|
nfan |
|- F/ y ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) |
14 |
13 11 5
|
nfif |
|- F/_ y if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) |
15 |
|
nfv |
|- F/ x y e. A |
16 |
|
nfcv |
|- F/_ x 0 |
17 |
|
nfcv |
|- F/_ x <_ |
18 |
|
nfcv |
|- F/_ x Re |
19 |
|
nfcv |
|- F/_ x / |
20 |
|
nfcv |
|- F/_ x ( _i ^ k ) |
21 |
3 19 20
|
nfov |
|- F/_ x ( C / ( _i ^ k ) ) |
22 |
18 21
|
nffv |
|- F/_ x ( Re ` ( C / ( _i ^ k ) ) ) |
23 |
16 17 22
|
nfbr |
|- F/ x 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) |
24 |
15 23
|
nfan |
|- F/ x ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) |
25 |
24 22 16
|
nfif |
|- F/_ x if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) |
26 |
|
eleq1w |
|- ( x = y -> ( x e. A <-> y e. A ) ) |
27 |
1
|
fvoveq1d |
|- ( x = y -> ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) ) ) |
28 |
27
|
breq2d |
|- ( x = y -> ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) <-> 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) ) |
29 |
26 28
|
anbi12d |
|- ( x = y -> ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) <-> ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) ) ) |
30 |
29 27
|
ifbieq1d |
|- ( x = y -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) = if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) |
31 |
14 25 30
|
cbvmpt |
|- ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( y e. RR |-> if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) |
32 |
31
|
a1i |
|- ( k e. ( 0 ... 3 ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( y e. RR |-> if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) |
33 |
32
|
fveq2d |
|- ( k e. ( 0 ... 3 ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( y e. RR |-> if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) |
34 |
33
|
oveq2d |
|- ( k e. ( 0 ... 3 ) -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( ( _i ^ k ) x. ( S.2 ` ( y e. RR |-> if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) ) |
35 |
34
|
sumeq2i |
|- sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( y e. RR |-> if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) |
36 |
|
eqid |
|- ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) ) |
37 |
36
|
dfitg |
|- S. A B _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) |
38 |
|
eqid |
|- ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) ) |
39 |
38
|
dfitg |
|- S. A C _d y = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( y e. RR |-> if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) |
40 |
35 37 39
|
3eqtr4i |
|- S. A B _d x = S. A C _d y |