Metamath Proof Explorer

Theorem fsumcncf

Description: The finite sum of continuous complex function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fsumcncf.x 
|- ( ph -> X C_ CC )
fsumcncf.a 
|- ( ph -> A e. Fin )
fsumcncf.cncf 
|- ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( X -cn-> CC ) )
Assertion fsumcncf 
|- ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( X -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 fsumcncf.x 
 |-  ( ph -> X C_ CC )
2 fsumcncf.a 
 |-  ( ph -> A e. Fin )
3 fsumcncf.cncf 
 |-  ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( X -cn-> CC ) )
4 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
5 4 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
6 5 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
7 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ X C_ CC ) -> ( ( TopOpen ` CCfld ) |`t X ) e. ( TopOn ` X ) )
8 6 1 7 syl2anc 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t X ) e. ( TopOn ` X ) )
9 ssidd 
 |-  ( ph -> CC C_ CC )
10 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t X ) = ( ( TopOpen ` CCfld ) |`t X )
11 4 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
12 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
13 12 restid 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
14 11 13 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
15 14 eqcomi 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
16 4 10 15 cncfcn 
 |-  ( ( X C_ CC /\ CC C_ CC ) -> ( X -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t X ) Cn ( TopOpen ` CCfld ) ) )
17 1 9 16 syl2anc 
 |-  ( ph -> ( X -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t X ) Cn ( TopOpen ` CCfld ) ) )
18 17 adantr 
 |-  ( ( ph /\ k e. A ) -> ( X -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t X ) Cn ( TopOpen ` CCfld ) ) )
19 3 18 eleqtrd 
 |-  ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( ( ( TopOpen ` CCfld ) |`t X ) Cn ( TopOpen ` CCfld ) ) )
20 4 8 2 19 fsumcnf 
 |-  ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( ( ( TopOpen ` CCfld ) |`t X ) Cn ( TopOpen ` CCfld ) ) )
21 20 17 eleqtrrd 
 |-  ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( X -cn-> CC ) )