This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iblcnlem

Description: Expand out the universal quantifier in isibl2 . (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypotheses itgcnlem.r 
|- R = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) )
itgcnlem.s 
|- S = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) )
itgcnlem.t 
|- T = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) )
itgcnlem.u 
|- U = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) )
itgcnlem.v 
|- ( ( ph /\ x e. A ) -> B e. V )
Assertion iblcnlem 
|- ( 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 ) ) ) )

Proof

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 ) ) ) )