Metamath Proof Explorer

Theorem fprodsub2cncf

Description: F is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses fprodsub2cncf.k 
|- F/ k ph
fprodsub2cncf.a 
|- ( ph -> A e. Fin )
fprodsub2cncf.b 
|- ( ( ph /\ k e. A ) -> B e. CC )
fprodsub2cncf.f 
|- F = ( x e. CC |-> prod_ k e. A ( B - x ) )
Assertion fprodsub2cncf 
|- ( ph -> F e. ( CC -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 fprodsub2cncf.k 
 |-  F/ k ph
2 fprodsub2cncf.a 
 |-  ( ph -> A e. Fin )
3 fprodsub2cncf.b 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
4 fprodsub2cncf.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 sub2cncfd 
 |-  ( ( 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 ) )