| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mbfimaopn.1 |
|- J = ( TopOpen ` CCfld ) |
| 2 |
|
mbfimaopn.2 |
|- G = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) ) |
| 3 |
|
mbfimaopn.3 |
|- B = ( (,) " ( QQ X. QQ ) ) |
| 4 |
|
mbfimaopn.4 |
|- K = ran ( x e. B , y e. B |-> ( x X. y ) ) |
| 5 |
|
eqid |
|- ( topGen ` ran (,) ) = ( topGen ` ran (,) ) |
| 6 |
2 5 1
|
cnrehmeo |
|- G e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Homeo J ) |
| 7 |
|
hmeocn |
|- ( G e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Homeo J ) -> G e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Cn J ) ) |
| 8 |
6 7
|
ax-mp |
|- G e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Cn J ) |
| 9 |
|
cnima |
|- ( ( G e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Cn J ) /\ A e. J ) -> ( `' G " A ) e. ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) ) |
| 10 |
8 9
|
mpan |
|- ( A e. J -> ( `' G " A ) e. ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) ) |
| 11 |
3
|
fveq2i |
|- ( topGen ` B ) = ( topGen ` ( (,) " ( QQ X. QQ ) ) ) |
| 12 |
11
|
tgqioo |
|- ( topGen ` ran (,) ) = ( topGen ` B ) |
| 13 |
12 12
|
oveq12i |
|- ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) = ( ( topGen ` B ) tX ( topGen ` B ) ) |
| 14 |
|
qtopbas |
|- ( (,) " ( QQ X. QQ ) ) e. TopBases |
| 15 |
3 14
|
eqeltri |
|- B e. TopBases |
| 16 |
|
txbasval |
|- ( ( B e. TopBases /\ B e. TopBases ) -> ( ( topGen ` B ) tX ( topGen ` B ) ) = ( B tX B ) ) |
| 17 |
15 15 16
|
mp2an |
|- ( ( topGen ` B ) tX ( topGen ` B ) ) = ( B tX B ) |
| 18 |
4
|
txval |
|- ( ( B e. TopBases /\ B e. TopBases ) -> ( B tX B ) = ( topGen ` K ) ) |
| 19 |
15 15 18
|
mp2an |
|- ( B tX B ) = ( topGen ` K ) |
| 20 |
13 17 19
|
3eqtri |
|- ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) = ( topGen ` K ) |
| 21 |
10 20
|
eleqtrdi |
|- ( A e. J -> ( `' G " A ) e. ( topGen ` K ) ) |
| 22 |
4
|
txbas |
|- ( ( B e. TopBases /\ B e. TopBases ) -> K e. TopBases ) |
| 23 |
15 15 22
|
mp2an |
|- K e. TopBases |
| 24 |
|
eltg3 |
|- ( K e. TopBases -> ( ( `' G " A ) e. ( topGen ` K ) <-> E. t ( t C_ K /\ ( `' G " A ) = U. t ) ) ) |
| 25 |
23 24
|
ax-mp |
|- ( ( `' G " A ) e. ( topGen ` K ) <-> E. t ( t C_ K /\ ( `' G " A ) = U. t ) ) |
| 26 |
21 25
|
sylib |
|- ( A e. J -> E. t ( t C_ K /\ ( `' G " A ) = U. t ) ) |
| 27 |
26
|
adantl |
|- ( ( F e. MblFn /\ A e. J ) -> E. t ( t C_ K /\ ( `' G " A ) = U. t ) ) |
| 28 |
2
|
cnref1o |
|- G : ( RR X. RR ) -1-1-onto-> CC |
| 29 |
|
f1ofo |
|- ( G : ( RR X. RR ) -1-1-onto-> CC -> G : ( RR X. RR ) -onto-> CC ) |
| 30 |
28 29
|
ax-mp |
|- G : ( RR X. RR ) -onto-> CC |
| 31 |
|
elssuni |
|- ( A e. J -> A C_ U. J ) |
| 32 |
1
|
cnfldtopon |
|- J e. ( TopOn ` CC ) |
| 33 |
32
|
toponunii |
|- CC = U. J |
| 34 |
31 33
|
sseqtrrdi |
|- ( A e. J -> A C_ CC ) |
| 35 |
34
|
ad2antlr |
|- ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> A C_ CC ) |
| 36 |
|
foimacnv |
|- ( ( G : ( RR X. RR ) -onto-> CC /\ A C_ CC ) -> ( G " ( `' G " A ) ) = A ) |
| 37 |
30 35 36
|
sylancr |
|- ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> ( G " ( `' G " A ) ) = A ) |
| 38 |
|
simprr |
|- ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> ( `' G " A ) = U. t ) |
| 39 |
38
|
imaeq2d |
|- ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> ( G " ( `' G " A ) ) = ( G " U. t ) ) |
| 40 |
|
imauni |
|- ( G " U. t ) = U_ w e. t ( G " w ) |
| 41 |
39 40
|
eqtrdi |
|- ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> ( G " ( `' G " A ) ) = U_ w e. t ( G " w ) ) |
| 42 |
37 41
|
eqtr3d |
|- ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> A = U_ w e. t ( G " w ) ) |
| 43 |
42
|
imaeq2d |
|- ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> ( `' F " A ) = ( `' F " U_ w e. t ( G " w ) ) ) |
| 44 |
|
imaiun |
|- ( `' F " U_ w e. t ( G " w ) ) = U_ w e. t ( `' F " ( G " w ) ) |
| 45 |
43 44
|
eqtrdi |
|- ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> ( `' F " A ) = U_ w e. t ( `' F " ( G " w ) ) ) |
| 46 |
|
ssdomg |
|- ( K e. TopBases -> ( t C_ K -> t ~<_ K ) ) |
| 47 |
23 46
|
ax-mp |
|- ( t C_ K -> t ~<_ K ) |
| 48 |
|
omelon |
|- _om e. On |
| 49 |
|
nnenom |
|- NN ~~ _om |
| 50 |
49
|
ensymi |
|- _om ~~ NN |
| 51 |
|
isnumi |
|- ( ( _om e. On /\ _om ~~ NN ) -> NN e. dom card ) |
| 52 |
48 50 51
|
mp2an |
|- NN e. dom card |
| 53 |
|
qnnen |
|- QQ ~~ NN |
| 54 |
|
xpen |
|- ( ( QQ ~~ NN /\ QQ ~~ NN ) -> ( QQ X. QQ ) ~~ ( NN X. NN ) ) |
| 55 |
53 53 54
|
mp2an |
|- ( QQ X. QQ ) ~~ ( NN X. NN ) |
| 56 |
|
xpnnen |
|- ( NN X. NN ) ~~ NN |
| 57 |
55 56
|
entri |
|- ( QQ X. QQ ) ~~ NN |
| 58 |
57 49
|
entr2i |
|- _om ~~ ( QQ X. QQ ) |
| 59 |
|
isnumi |
|- ( ( _om e. On /\ _om ~~ ( QQ X. QQ ) ) -> ( QQ X. QQ ) e. dom card ) |
| 60 |
48 58 59
|
mp2an |
|- ( QQ X. QQ ) e. dom card |
| 61 |
|
ioof |
|- (,) : ( RR* X. RR* ) --> ~P RR |
| 62 |
|
ffun |
|- ( (,) : ( RR* X. RR* ) --> ~P RR -> Fun (,) ) |
| 63 |
61 62
|
ax-mp |
|- Fun (,) |
| 64 |
|
qssre |
|- QQ C_ RR |
| 65 |
|
ressxr |
|- RR C_ RR* |
| 66 |
64 65
|
sstri |
|- QQ C_ RR* |
| 67 |
|
xpss12 |
|- ( ( QQ C_ RR* /\ QQ C_ RR* ) -> ( QQ X. QQ ) C_ ( RR* X. RR* ) ) |
| 68 |
66 66 67
|
mp2an |
|- ( QQ X. QQ ) C_ ( RR* X. RR* ) |
| 69 |
61
|
fdmi |
|- dom (,) = ( RR* X. RR* ) |
| 70 |
68 69
|
sseqtrri |
|- ( QQ X. QQ ) C_ dom (,) |
| 71 |
|
fores |
|- ( ( Fun (,) /\ ( QQ X. QQ ) C_ dom (,) ) -> ( (,) |` ( QQ X. QQ ) ) : ( QQ X. QQ ) -onto-> ( (,) " ( QQ X. QQ ) ) ) |
| 72 |
63 70 71
|
mp2an |
|- ( (,) |` ( QQ X. QQ ) ) : ( QQ X. QQ ) -onto-> ( (,) " ( QQ X. QQ ) ) |
| 73 |
|
fodomnum |
|- ( ( QQ X. QQ ) e. dom card -> ( ( (,) |` ( QQ X. QQ ) ) : ( QQ X. QQ ) -onto-> ( (,) " ( QQ X. QQ ) ) -> ( (,) " ( QQ X. QQ ) ) ~<_ ( QQ X. QQ ) ) ) |
| 74 |
60 72 73
|
mp2 |
|- ( (,) " ( QQ X. QQ ) ) ~<_ ( QQ X. QQ ) |
| 75 |
3 74
|
eqbrtri |
|- B ~<_ ( QQ X. QQ ) |
| 76 |
|
domentr |
|- ( ( B ~<_ ( QQ X. QQ ) /\ ( QQ X. QQ ) ~~ NN ) -> B ~<_ NN ) |
| 77 |
75 57 76
|
mp2an |
|- B ~<_ NN |
| 78 |
15
|
elexi |
|- B e. _V |
| 79 |
78
|
xpdom1 |
|- ( B ~<_ NN -> ( B X. B ) ~<_ ( NN X. B ) ) |
| 80 |
77 79
|
ax-mp |
|- ( B X. B ) ~<_ ( NN X. B ) |
| 81 |
|
nnex |
|- NN e. _V |
| 82 |
81
|
xpdom2 |
|- ( B ~<_ NN -> ( NN X. B ) ~<_ ( NN X. NN ) ) |
| 83 |
77 82
|
ax-mp |
|- ( NN X. B ) ~<_ ( NN X. NN ) |
| 84 |
|
domtr |
|- ( ( ( B X. B ) ~<_ ( NN X. B ) /\ ( NN X. B ) ~<_ ( NN X. NN ) ) -> ( B X. B ) ~<_ ( NN X. NN ) ) |
| 85 |
80 83 84
|
mp2an |
|- ( B X. B ) ~<_ ( NN X. NN ) |
| 86 |
|
domentr |
|- ( ( ( B X. B ) ~<_ ( NN X. NN ) /\ ( NN X. NN ) ~~ NN ) -> ( B X. B ) ~<_ NN ) |
| 87 |
85 56 86
|
mp2an |
|- ( B X. B ) ~<_ NN |
| 88 |
|
numdom |
|- ( ( NN e. dom card /\ ( B X. B ) ~<_ NN ) -> ( B X. B ) e. dom card ) |
| 89 |
52 87 88
|
mp2an |
|- ( B X. B ) e. dom card |
| 90 |
|
eqid |
|- ( x e. B , y e. B |-> ( x X. y ) ) = ( x e. B , y e. B |-> ( x X. y ) ) |
| 91 |
|
vex |
|- x e. _V |
| 92 |
|
vex |
|- y e. _V |
| 93 |
91 92
|
xpex |
|- ( x X. y ) e. _V |
| 94 |
90 93
|
fnmpoi |
|- ( x e. B , y e. B |-> ( x X. y ) ) Fn ( B X. B ) |
| 95 |
|
dffn4 |
|- ( ( x e. B , y e. B |-> ( x X. y ) ) Fn ( B X. B ) <-> ( x e. B , y e. B |-> ( x X. y ) ) : ( B X. B ) -onto-> ran ( x e. B , y e. B |-> ( x X. y ) ) ) |
| 96 |
94 95
|
mpbi |
|- ( x e. B , y e. B |-> ( x X. y ) ) : ( B X. B ) -onto-> ran ( x e. B , y e. B |-> ( x X. y ) ) |
| 97 |
|
fodomnum |
|- ( ( B X. B ) e. dom card -> ( ( x e. B , y e. B |-> ( x X. y ) ) : ( B X. B ) -onto-> ran ( x e. B , y e. B |-> ( x X. y ) ) -> ran ( x e. B , y e. B |-> ( x X. y ) ) ~<_ ( B X. B ) ) ) |
| 98 |
89 96 97
|
mp2 |
|- ran ( x e. B , y e. B |-> ( x X. y ) ) ~<_ ( B X. B ) |
| 99 |
|
domtr |
|- ( ( ran ( x e. B , y e. B |-> ( x X. y ) ) ~<_ ( B X. B ) /\ ( B X. B ) ~<_ NN ) -> ran ( x e. B , y e. B |-> ( x X. y ) ) ~<_ NN ) |
| 100 |
98 87 99
|
mp2an |
|- ran ( x e. B , y e. B |-> ( x X. y ) ) ~<_ NN |
| 101 |
4 100
|
eqbrtri |
|- K ~<_ NN |
| 102 |
|
domtr |
|- ( ( t ~<_ K /\ K ~<_ NN ) -> t ~<_ NN ) |
| 103 |
47 101 102
|
sylancl |
|- ( t C_ K -> t ~<_ NN ) |
| 104 |
103
|
ad2antrl |
|- ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> t ~<_ NN ) |
| 105 |
4
|
eleq2i |
|- ( w e. K <-> w e. ran ( x e. B , y e. B |-> ( x X. y ) ) ) |
| 106 |
90 93
|
elrnmpo |
|- ( w e. ran ( x e. B , y e. B |-> ( x X. y ) ) <-> E. x e. B E. y e. B w = ( x X. y ) ) |
| 107 |
105 106
|
bitri |
|- ( w e. K <-> E. x e. B E. y e. B w = ( x X. y ) ) |
| 108 |
|
elin |
|- ( z e. ( ( `' ( Re o. F ) " x ) i^i ( `' ( Im o. F ) " y ) ) <-> ( z e. ( `' ( Re o. F ) " x ) /\ z e. ( `' ( Im o. F ) " y ) ) ) |
| 109 |
|
mbff |
|- ( F e. MblFn -> F : dom F --> CC ) |
| 110 |
109
|
adantr |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> F : dom F --> CC ) |
| 111 |
|
fvco3 |
|- ( ( F : dom F --> CC /\ z e. dom F ) -> ( ( Re o. F ) ` z ) = ( Re ` ( F ` z ) ) ) |
| 112 |
110 111
|
sylan |
|- ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( Re o. F ) ` z ) = ( Re ` ( F ` z ) ) ) |
| 113 |
112
|
eleq1d |
|- ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( ( Re o. F ) ` z ) e. x <-> ( Re ` ( F ` z ) ) e. x ) ) |
| 114 |
|
fvco3 |
|- ( ( F : dom F --> CC /\ z e. dom F ) -> ( ( Im o. F ) ` z ) = ( Im ` ( F ` z ) ) ) |
| 115 |
110 114
|
sylan |
|- ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( Im o. F ) ` z ) = ( Im ` ( F ` z ) ) ) |
| 116 |
115
|
eleq1d |
|- ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( ( Im o. F ) ` z ) e. y <-> ( Im ` ( F ` z ) ) e. y ) ) |
| 117 |
113 116
|
anbi12d |
|- ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( ( ( Re o. F ) ` z ) e. x /\ ( ( Im o. F ) ` z ) e. y ) <-> ( ( Re ` ( F ` z ) ) e. x /\ ( Im ` ( F ` z ) ) e. y ) ) ) |
| 118 |
110
|
ffvelcdmda |
|- ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( F ` z ) e. CC ) |
| 119 |
|
fveq2 |
|- ( w = ( F ` z ) -> ( Re ` w ) = ( Re ` ( F ` z ) ) ) |
| 120 |
|
fveq2 |
|- ( w = ( F ` z ) -> ( Im ` w ) = ( Im ` ( F ` z ) ) ) |
| 121 |
119 120
|
opeq12d |
|- ( w = ( F ` z ) -> <. ( Re ` w ) , ( Im ` w ) >. = <. ( Re ` ( F ` z ) ) , ( Im ` ( F ` z ) ) >. ) |
| 122 |
2
|
cnrecnv |
|- `' G = ( w e. CC |-> <. ( Re ` w ) , ( Im ` w ) >. ) |
| 123 |
|
opex |
|- <. ( Re ` ( F ` z ) ) , ( Im ` ( F ` z ) ) >. e. _V |
| 124 |
121 122 123
|
fvmpt |
|- ( ( F ` z ) e. CC -> ( `' G ` ( F ` z ) ) = <. ( Re ` ( F ` z ) ) , ( Im ` ( F ` z ) ) >. ) |
| 125 |
118 124
|
syl |
|- ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( `' G ` ( F ` z ) ) = <. ( Re ` ( F ` z ) ) , ( Im ` ( F ` z ) ) >. ) |
| 126 |
125
|
eleq1d |
|- ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( `' G ` ( F ` z ) ) e. ( x X. y ) <-> <. ( Re ` ( F ` z ) ) , ( Im ` ( F ` z ) ) >. e. ( x X. y ) ) ) |
| 127 |
118
|
biantrurd |
|- ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( `' G ` ( F ` z ) ) e. ( x X. y ) <-> ( ( F ` z ) e. CC /\ ( `' G ` ( F ` z ) ) e. ( x X. y ) ) ) ) |
| 128 |
126 127
|
bitr3d |
|- ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( <. ( Re ` ( F ` z ) ) , ( Im ` ( F ` z ) ) >. e. ( x X. y ) <-> ( ( F ` z ) e. CC /\ ( `' G ` ( F ` z ) ) e. ( x X. y ) ) ) ) |
| 129 |
|
opelxp |
|- ( <. ( Re ` ( F ` z ) ) , ( Im ` ( F ` z ) ) >. e. ( x X. y ) <-> ( ( Re ` ( F ` z ) ) e. x /\ ( Im ` ( F ` z ) ) e. y ) ) |
| 130 |
|
f1ocnv |
|- ( G : ( RR X. RR ) -1-1-onto-> CC -> `' G : CC -1-1-onto-> ( RR X. RR ) ) |
| 131 |
|
f1ofn |
|- ( `' G : CC -1-1-onto-> ( RR X. RR ) -> `' G Fn CC ) |
| 132 |
28 130 131
|
mp2b |
|- `' G Fn CC |
| 133 |
|
elpreima |
|- ( `' G Fn CC -> ( ( F ` z ) e. ( `' `' G " ( x X. y ) ) <-> ( ( F ` z ) e. CC /\ ( `' G ` ( F ` z ) ) e. ( x X. y ) ) ) ) |
| 134 |
132 133
|
ax-mp |
|- ( ( F ` z ) e. ( `' `' G " ( x X. y ) ) <-> ( ( F ` z ) e. CC /\ ( `' G ` ( F ` z ) ) e. ( x X. y ) ) ) |
| 135 |
|
imacnvcnv |
|- ( `' `' G " ( x X. y ) ) = ( G " ( x X. y ) ) |
| 136 |
135
|
eleq2i |
|- ( ( F ` z ) e. ( `' `' G " ( x X. y ) ) <-> ( F ` z ) e. ( G " ( x X. y ) ) ) |
| 137 |
134 136
|
bitr3i |
|- ( ( ( F ` z ) e. CC /\ ( `' G ` ( F ` z ) ) e. ( x X. y ) ) <-> ( F ` z ) e. ( G " ( x X. y ) ) ) |
| 138 |
128 129 137
|
3bitr3g |
|- ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( ( Re ` ( F ` z ) ) e. x /\ ( Im ` ( F ` z ) ) e. y ) <-> ( F ` z ) e. ( G " ( x X. y ) ) ) ) |
| 139 |
117 138
|
bitrd |
|- ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( ( ( Re o. F ) ` z ) e. x /\ ( ( Im o. F ) ` z ) e. y ) <-> ( F ` z ) e. ( G " ( x X. y ) ) ) ) |
| 140 |
139
|
pm5.32da |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( ( z e. dom F /\ ( ( ( Re o. F ) ` z ) e. x /\ ( ( Im o. F ) ` z ) e. y ) ) <-> ( z e. dom F /\ ( F ` z ) e. ( G " ( x X. y ) ) ) ) ) |
| 141 |
|
ref |
|- Re : CC --> RR |
| 142 |
|
fco |
|- ( ( Re : CC --> RR /\ F : dom F --> CC ) -> ( Re o. F ) : dom F --> RR ) |
| 143 |
141 109 142
|
sylancr |
|- ( F e. MblFn -> ( Re o. F ) : dom F --> RR ) |
| 144 |
|
ffn |
|- ( ( Re o. F ) : dom F --> RR -> ( Re o. F ) Fn dom F ) |
| 145 |
|
elpreima |
|- ( ( Re o. F ) Fn dom F -> ( z e. ( `' ( Re o. F ) " x ) <-> ( z e. dom F /\ ( ( Re o. F ) ` z ) e. x ) ) ) |
| 146 |
143 144 145
|
3syl |
|- ( F e. MblFn -> ( z e. ( `' ( Re o. F ) " x ) <-> ( z e. dom F /\ ( ( Re o. F ) ` z ) e. x ) ) ) |
| 147 |
|
imf |
|- Im : CC --> RR |
| 148 |
|
fco |
|- ( ( Im : CC --> RR /\ F : dom F --> CC ) -> ( Im o. F ) : dom F --> RR ) |
| 149 |
147 109 148
|
sylancr |
|- ( F e. MblFn -> ( Im o. F ) : dom F --> RR ) |
| 150 |
|
ffn |
|- ( ( Im o. F ) : dom F --> RR -> ( Im o. F ) Fn dom F ) |
| 151 |
|
elpreima |
|- ( ( Im o. F ) Fn dom F -> ( z e. ( `' ( Im o. F ) " y ) <-> ( z e. dom F /\ ( ( Im o. F ) ` z ) e. y ) ) ) |
| 152 |
149 150 151
|
3syl |
|- ( F e. MblFn -> ( z e. ( `' ( Im o. F ) " y ) <-> ( z e. dom F /\ ( ( Im o. F ) ` z ) e. y ) ) ) |
| 153 |
146 152
|
anbi12d |
|- ( F e. MblFn -> ( ( z e. ( `' ( Re o. F ) " x ) /\ z e. ( `' ( Im o. F ) " y ) ) <-> ( ( z e. dom F /\ ( ( Re o. F ) ` z ) e. x ) /\ ( z e. dom F /\ ( ( Im o. F ) ` z ) e. y ) ) ) ) |
| 154 |
|
anandi |
|- ( ( z e. dom F /\ ( ( ( Re o. F ) ` z ) e. x /\ ( ( Im o. F ) ` z ) e. y ) ) <-> ( ( z e. dom F /\ ( ( Re o. F ) ` z ) e. x ) /\ ( z e. dom F /\ ( ( Im o. F ) ` z ) e. y ) ) ) |
| 155 |
153 154
|
bitr4di |
|- ( F e. MblFn -> ( ( z e. ( `' ( Re o. F ) " x ) /\ z e. ( `' ( Im o. F ) " y ) ) <-> ( z e. dom F /\ ( ( ( Re o. F ) ` z ) e. x /\ ( ( Im o. F ) ` z ) e. y ) ) ) ) |
| 156 |
155
|
adantr |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( ( z e. ( `' ( Re o. F ) " x ) /\ z e. ( `' ( Im o. F ) " y ) ) <-> ( z e. dom F /\ ( ( ( Re o. F ) ` z ) e. x /\ ( ( Im o. F ) ` z ) e. y ) ) ) ) |
| 157 |
|
ffn |
|- ( F : dom F --> CC -> F Fn dom F ) |
| 158 |
|
elpreima |
|- ( F Fn dom F -> ( z e. ( `' F " ( G " ( x X. y ) ) ) <-> ( z e. dom F /\ ( F ` z ) e. ( G " ( x X. y ) ) ) ) ) |
| 159 |
109 157 158
|
3syl |
|- ( F e. MblFn -> ( z e. ( `' F " ( G " ( x X. y ) ) ) <-> ( z e. dom F /\ ( F ` z ) e. ( G " ( x X. y ) ) ) ) ) |
| 160 |
159
|
adantr |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( z e. ( `' F " ( G " ( x X. y ) ) ) <-> ( z e. dom F /\ ( F ` z ) e. ( G " ( x X. y ) ) ) ) ) |
| 161 |
140 156 160
|
3bitr4d |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( ( z e. ( `' ( Re o. F ) " x ) /\ z e. ( `' ( Im o. F ) " y ) ) <-> z e. ( `' F " ( G " ( x X. y ) ) ) ) ) |
| 162 |
108 161
|
bitrid |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( z e. ( ( `' ( Re o. F ) " x ) i^i ( `' ( Im o. F ) " y ) ) <-> z e. ( `' F " ( G " ( x X. y ) ) ) ) ) |
| 163 |
162
|
eqrdv |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( ( `' ( Re o. F ) " x ) i^i ( `' ( Im o. F ) " y ) ) = ( `' F " ( G " ( x X. y ) ) ) ) |
| 164 |
|
ismbfcn |
|- ( F : dom F --> CC -> ( F e. MblFn <-> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) ) ) |
| 165 |
109 164
|
syl |
|- ( F e. MblFn -> ( F e. MblFn <-> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) ) ) |
| 166 |
165
|
ibi |
|- ( F e. MblFn -> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) ) |
| 167 |
166
|
simpld |
|- ( F e. MblFn -> ( Re o. F ) e. MblFn ) |
| 168 |
|
ismbf |
|- ( ( Re o. F ) : dom F --> RR -> ( ( Re o. F ) e. MblFn <-> A. x e. ran (,) ( `' ( Re o. F ) " x ) e. dom vol ) ) |
| 169 |
143 168
|
syl |
|- ( F e. MblFn -> ( ( Re o. F ) e. MblFn <-> A. x e. ran (,) ( `' ( Re o. F ) " x ) e. dom vol ) ) |
| 170 |
167 169
|
mpbid |
|- ( F e. MblFn -> A. x e. ran (,) ( `' ( Re o. F ) " x ) e. dom vol ) |
| 171 |
170
|
adantr |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> A. x e. ran (,) ( `' ( Re o. F ) " x ) e. dom vol ) |
| 172 |
|
imassrn |
|- ( (,) " ( QQ X. QQ ) ) C_ ran (,) |
| 173 |
3 172
|
eqsstri |
|- B C_ ran (,) |
| 174 |
|
simprl |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> x e. B ) |
| 175 |
173 174
|
sselid |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> x e. ran (,) ) |
| 176 |
|
rsp |
|- ( A. x e. ran (,) ( `' ( Re o. F ) " x ) e. dom vol -> ( x e. ran (,) -> ( `' ( Re o. F ) " x ) e. dom vol ) ) |
| 177 |
171 175 176
|
sylc |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( `' ( Re o. F ) " x ) e. dom vol ) |
| 178 |
166
|
simprd |
|- ( F e. MblFn -> ( Im o. F ) e. MblFn ) |
| 179 |
|
ismbf |
|- ( ( Im o. F ) : dom F --> RR -> ( ( Im o. F ) e. MblFn <-> A. y e. ran (,) ( `' ( Im o. F ) " y ) e. dom vol ) ) |
| 180 |
149 179
|
syl |
|- ( F e. MblFn -> ( ( Im o. F ) e. MblFn <-> A. y e. ran (,) ( `' ( Im o. F ) " y ) e. dom vol ) ) |
| 181 |
178 180
|
mpbid |
|- ( F e. MblFn -> A. y e. ran (,) ( `' ( Im o. F ) " y ) e. dom vol ) |
| 182 |
181
|
adantr |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> A. y e. ran (,) ( `' ( Im o. F ) " y ) e. dom vol ) |
| 183 |
|
simprr |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> y e. B ) |
| 184 |
173 183
|
sselid |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> y e. ran (,) ) |
| 185 |
|
rsp |
|- ( A. y e. ran (,) ( `' ( Im o. F ) " y ) e. dom vol -> ( y e. ran (,) -> ( `' ( Im o. F ) " y ) e. dom vol ) ) |
| 186 |
182 184 185
|
sylc |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( `' ( Im o. F ) " y ) e. dom vol ) |
| 187 |
|
inmbl |
|- ( ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " y ) e. dom vol ) -> ( ( `' ( Re o. F ) " x ) i^i ( `' ( Im o. F ) " y ) ) e. dom vol ) |
| 188 |
177 186 187
|
syl2anc |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( ( `' ( Re o. F ) " x ) i^i ( `' ( Im o. F ) " y ) ) e. dom vol ) |
| 189 |
163 188
|
eqeltrrd |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( `' F " ( G " ( x X. y ) ) ) e. dom vol ) |
| 190 |
|
imaeq2 |
|- ( w = ( x X. y ) -> ( G " w ) = ( G " ( x X. y ) ) ) |
| 191 |
190
|
imaeq2d |
|- ( w = ( x X. y ) -> ( `' F " ( G " w ) ) = ( `' F " ( G " ( x X. y ) ) ) ) |
| 192 |
191
|
eleq1d |
|- ( w = ( x X. y ) -> ( ( `' F " ( G " w ) ) e. dom vol <-> ( `' F " ( G " ( x X. y ) ) ) e. dom vol ) ) |
| 193 |
189 192
|
syl5ibrcom |
|- ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( w = ( x X. y ) -> ( `' F " ( G " w ) ) e. dom vol ) ) |
| 194 |
193
|
rexlimdvva |
|- ( F e. MblFn -> ( E. x e. B E. y e. B w = ( x X. y ) -> ( `' F " ( G " w ) ) e. dom vol ) ) |
| 195 |
107 194
|
biimtrid |
|- ( F e. MblFn -> ( w e. K -> ( `' F " ( G " w ) ) e. dom vol ) ) |
| 196 |
195
|
ralrimiv |
|- ( F e. MblFn -> A. w e. K ( `' F " ( G " w ) ) e. dom vol ) |
| 197 |
|
ssralv |
|- ( t C_ K -> ( A. w e. K ( `' F " ( G " w ) ) e. dom vol -> A. w e. t ( `' F " ( G " w ) ) e. dom vol ) ) |
| 198 |
196 197
|
mpan9 |
|- ( ( F e. MblFn /\ t C_ K ) -> A. w e. t ( `' F " ( G " w ) ) e. dom vol ) |
| 199 |
198
|
ad2ant2r |
|- ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> A. w e. t ( `' F " ( G " w ) ) e. dom vol ) |
| 200 |
|
iunmbl2 |
|- ( ( t ~<_ NN /\ A. w e. t ( `' F " ( G " w ) ) e. dom vol ) -> U_ w e. t ( `' F " ( G " w ) ) e. dom vol ) |
| 201 |
104 199 200
|
syl2anc |
|- ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> U_ w e. t ( `' F " ( G " w ) ) e. dom vol ) |
| 202 |
45 201
|
eqeltrd |
|- ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> ( `' F " A ) e. dom vol ) |
| 203 |
27 202
|
exlimddv |
|- ( ( F e. MblFn /\ A e. J ) -> ( `' F " A ) e. dom vol ) |