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