Step |
Hyp |
Ref |
Expression |
1 |
|
iblidicc.a |
|- ( ph -> A e. RR ) |
2 |
|
iblidicc.b |
|- ( ph -> B e. RR ) |
3 |
|
iccssre |
|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR ) |
4 |
1 2 3
|
syl2anc |
|- ( ph -> ( A [,] B ) C_ RR ) |
5 |
|
ax-resscn |
|- RR C_ CC |
6 |
4 5
|
sstrdi |
|- ( ph -> ( A [,] B ) C_ CC ) |
7 |
|
ssid |
|- CC C_ CC |
8 |
|
cncfmptid |
|- ( ( ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC ) ) |
9 |
6 7 8
|
sylancl |
|- ( ph -> ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC ) ) |
10 |
|
cniccibl |
|- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> x ) e. L^1 ) |
11 |
1 2 9 10
|
syl3anc |
|- ( ph -> ( x e. ( A [,] B ) |-> x ) e. L^1 ) |