| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fprodadd2cncf.k |
|- F/ k ph |
| 2 |
|
fprodadd2cncf.a |
|- ( ph -> A e. Fin ) |
| 3 |
|
fprodadd2cncf.b |
|- ( ( ph /\ k e. A ) -> B e. CC ) |
| 4 |
|
fprodadd2cncf.f |
|- F = ( x e. CC |-> prod_ k e. A ( B + x ) ) |
| 5 |
4
|
a1i |
|- ( ph -> F = ( x e. CC |-> prod_ k e. A ( B + x ) ) ) |
| 6 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
| 7 |
6
|
cnfldtopon |
|- ( TopOpen ` CCfld ) e. ( TopOn ` CC ) |
| 8 |
7
|
a1i |
|- ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) |
| 9 |
|
eqid |
|- ( x e. CC |-> ( B + x ) ) = ( x e. CC |-> ( B + x ) ) |
| 10 |
3 9
|
add2cncf |
|- ( ( ph /\ k e. A ) -> ( x e. CC |-> ( B + x ) ) e. ( CC -cn-> CC ) ) |
| 11 |
6
|
cncfcn1 |
|- ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) |
| 12 |
11
|
a1i |
|- ( ( ph /\ k e. A ) -> ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) ) |
| 13 |
10 12
|
eleqtrd |
|- ( ( ph /\ k e. A ) -> ( x e. CC |-> ( B + x ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) ) |
| 14 |
1 6 8 2 13
|
fprodcn |
|- ( ph -> ( x e. CC |-> prod_ k e. A ( B + x ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) ) |
| 15 |
5 14
|
eqeltrd |
|- ( ph -> F e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) ) |
| 16 |
11
|
a1i |
|- ( ph -> ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) ) |
| 17 |
16
|
eqcomd |
|- ( ph -> ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) = ( CC -cn-> CC ) ) |
| 18 |
15 17
|
eleqtrd |
|- ( ph -> F e. ( CC -cn-> CC ) ) |