Step |
Hyp |
Ref |
Expression |
1 |
|
itgcnlem.r |
|- R = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) |
2 |
|
itgcnlem.s |
|- S = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) |
3 |
|
itgcnlem.t |
|- T = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) |
4 |
|
itgcnlem.u |
|- U = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) |
5 |
|
itgcnlem.v |
|- ( ( ph /\ x e. A ) -> B e. V ) |
6 |
|
iblmbf |
|- ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn ) |
7 |
6
|
a1i |
|- ( ph -> ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn ) ) |
8 |
|
simp1 |
|- ( ( ( x e. A |-> B ) e. MblFn /\ ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) -> ( x e. A |-> B ) e. MblFn ) |
9 |
8
|
a1i |
|- ( ph -> ( ( ( x e. A |-> B ) e. MblFn /\ ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) -> ( x e. A |-> B ) e. MblFn ) ) |
10 |
|
eqid |
|- ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) |
11 |
|
eqid |
|- ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) |
12 |
|
eqid |
|- ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) |
13 |
|
eqid |
|- ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) |
14 |
|
0cn |
|- 0 e. CC |
15 |
14
|
elimel |
|- if ( B e. CC , B , 0 ) e. CC |
16 |
15
|
a1i |
|- ( ( ph /\ x e. A ) -> if ( B e. CC , B , 0 ) e. CC ) |
17 |
10 11 12 13 16
|
iblcnlem1 |
|- ( ph -> ( ( x e. A |-> if ( B e. CC , B , 0 ) ) e. L^1 <-> ( ( x e. A |-> if ( B e. CC , B , 0 ) ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR ) ) ) ) |
18 |
17
|
adantr |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( ( x e. A |-> if ( B e. CC , B , 0 ) ) e. L^1 <-> ( ( x e. A |-> if ( B e. CC , B , 0 ) ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR ) ) ) ) |
19 |
|
eqid |
|- A = A |
20 |
|
mbff |
|- ( ( x e. A |-> B ) e. MblFn -> ( x e. A |-> B ) : dom ( x e. A |-> B ) --> CC ) |
21 |
|
eqid |
|- ( x e. A |-> B ) = ( x e. A |-> B ) |
22 |
21 5
|
dmmptd |
|- ( ph -> dom ( x e. A |-> B ) = A ) |
23 |
22
|
feq2d |
|- ( ph -> ( ( x e. A |-> B ) : dom ( x e. A |-> B ) --> CC <-> ( x e. A |-> B ) : A --> CC ) ) |
24 |
23
|
biimpa |
|- ( ( ph /\ ( x e. A |-> B ) : dom ( x e. A |-> B ) --> CC ) -> ( x e. A |-> B ) : A --> CC ) |
25 |
20 24
|
sylan2 |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( x e. A |-> B ) : A --> CC ) |
26 |
21
|
fmpt |
|- ( A. x e. A B e. CC <-> ( x e. A |-> B ) : A --> CC ) |
27 |
25 26
|
sylibr |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> A. x e. A B e. CC ) |
28 |
|
iftrue |
|- ( B e. CC -> if ( B e. CC , B , 0 ) = B ) |
29 |
28
|
ralimi |
|- ( A. x e. A B e. CC -> A. x e. A if ( B e. CC , B , 0 ) = B ) |
30 |
27 29
|
syl |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> A. x e. A if ( B e. CC , B , 0 ) = B ) |
31 |
|
mpteq12 |
|- ( ( A = A /\ A. x e. A if ( B e. CC , B , 0 ) = B ) -> ( x e. A |-> if ( B e. CC , B , 0 ) ) = ( x e. A |-> B ) ) |
32 |
19 30 31
|
sylancr |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( x e. A |-> if ( B e. CC , B , 0 ) ) = ( x e. A |-> B ) ) |
33 |
32
|
eleq1d |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( ( x e. A |-> if ( B e. CC , B , 0 ) ) e. L^1 <-> ( x e. A |-> B ) e. L^1 ) ) |
34 |
32
|
eleq1d |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( ( x e. A |-> if ( B e. CC , B , 0 ) ) e. MblFn <-> ( x e. A |-> B ) e. MblFn ) ) |
35 |
|
eqid |
|- RR = RR |
36 |
28
|
imim2i |
|- ( ( x e. A -> B e. CC ) -> ( x e. A -> if ( B e. CC , B , 0 ) = B ) ) |
37 |
36
|
imp |
|- ( ( ( x e. A -> B e. CC ) /\ x e. A ) -> if ( B e. CC , B , 0 ) = B ) |
38 |
37
|
fveq2d |
|- ( ( ( x e. A -> B e. CC ) /\ x e. A ) -> ( Re ` if ( B e. CC , B , 0 ) ) = ( Re ` B ) ) |
39 |
38
|
ibllem |
|- ( ( x e. A -> B e. CC ) -> if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) |
40 |
39
|
a1d |
|- ( ( x e. A -> B e. CC ) -> ( x e. RR -> if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) |
41 |
40
|
ralimi2 |
|- ( A. x e. A B e. CC -> A. x e. RR if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) |
42 |
27 41
|
syl |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> A. x e. RR if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) |
43 |
|
mpteq12 |
|- ( ( RR = RR /\ A. x e. RR if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) |
44 |
35 42 43
|
sylancr |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) |
45 |
44
|
fveq2d |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) ) |
46 |
45 1
|
eqtr4di |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) = R ) |
47 |
46
|
eleq1d |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR <-> R e. RR ) ) |
48 |
38
|
negeqd |
|- ( ( ( x e. A -> B e. CC ) /\ x e. A ) -> -u ( Re ` if ( B e. CC , B , 0 ) ) = -u ( Re ` B ) ) |
49 |
48
|
ibllem |
|- ( ( x e. A -> B e. CC ) -> if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) |
50 |
49
|
a1d |
|- ( ( x e. A -> B e. CC ) -> ( x e. RR -> if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) |
51 |
50
|
ralimi2 |
|- ( A. x e. A B e. CC -> A. x e. RR if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) |
52 |
27 51
|
syl |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> A. x e. RR if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) |
53 |
|
mpteq12 |
|- ( ( RR = RR /\ A. x e. RR if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) |
54 |
35 52 53
|
sylancr |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) |
55 |
54
|
fveq2d |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) ) |
56 |
55 2
|
eqtr4di |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) = S ) |
57 |
56
|
eleq1d |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR <-> S e. RR ) ) |
58 |
47 57
|
anbi12d |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR ) <-> ( R e. RR /\ S e. RR ) ) ) |
59 |
37
|
fveq2d |
|- ( ( ( x e. A -> B e. CC ) /\ x e. A ) -> ( Im ` if ( B e. CC , B , 0 ) ) = ( Im ` B ) ) |
60 |
59
|
ibllem |
|- ( ( x e. A -> B e. CC ) -> if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) |
61 |
60
|
a1d |
|- ( ( x e. A -> B e. CC ) -> ( x e. RR -> if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) |
62 |
61
|
ralimi2 |
|- ( A. x e. A B e. CC -> A. x e. RR if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) |
63 |
27 62
|
syl |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> A. x e. RR if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) |
64 |
|
mpteq12 |
|- ( ( RR = RR /\ A. x e. RR if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) |
65 |
35 63 64
|
sylancr |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) |
66 |
65
|
fveq2d |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) ) |
67 |
66 3
|
eqtr4di |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) = T ) |
68 |
67
|
eleq1d |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR <-> T e. RR ) ) |
69 |
59
|
negeqd |
|- ( ( ( x e. A -> B e. CC ) /\ x e. A ) -> -u ( Im ` if ( B e. CC , B , 0 ) ) = -u ( Im ` B ) ) |
70 |
69
|
ibllem |
|- ( ( x e. A -> B e. CC ) -> if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) |
71 |
70
|
a1d |
|- ( ( x e. A -> B e. CC ) -> ( x e. RR -> if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) |
72 |
71
|
ralimi2 |
|- ( A. x e. A B e. CC -> A. x e. RR if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) |
73 |
27 72
|
syl |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> A. x e. RR if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) |
74 |
|
mpteq12 |
|- ( ( RR = RR /\ A. x e. RR if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) |
75 |
35 73 74
|
sylancr |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) |
76 |
75
|
fveq2d |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) ) |
77 |
76 4
|
eqtr4di |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) = U ) |
78 |
77
|
eleq1d |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR <-> U e. RR ) ) |
79 |
68 78
|
anbi12d |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR ) <-> ( T e. RR /\ U e. RR ) ) ) |
80 |
34 58 79
|
3anbi123d |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( ( ( x e. A |-> if ( B e. CC , B , 0 ) ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` if ( B e. CC , B , 0 ) ) ) , ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` if ( B e. CC , B , 0 ) ) ) , -u ( Re ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` if ( B e. CC , B , 0 ) ) ) , ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` if ( B e. CC , B , 0 ) ) ) , -u ( Im ` if ( B e. CC , B , 0 ) ) , 0 ) ) ) e. RR ) ) <-> ( ( x e. A |-> B ) e. MblFn /\ ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) ) ) |
81 |
18 33 80
|
3bitr3d |
|- ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) ) ) |
82 |
81
|
ex |
|- ( ph -> ( ( x e. A |-> B ) e. MblFn -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) ) ) ) |
83 |
7 9 82
|
pm5.21ndd |
|- ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) ) ) |