Metamath Proof Explorer

Theorem refsumcn

Description: A finite sum of continuous real functions, from a common topological space, is continuous. The class expression for B normally contains free variables k and x to index it. See fsumcn for the analogous theorem on continuous complex functions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses refsumcn.1 
|- F/ x ph
refsumcn.2 
|- K = ( topGen ` ran (,) )
refsumcn.3 
|- ( ph -> J e. ( TopOn ` X ) )
refsumcn.4 
|- ( ph -> A e. Fin )
refsumcn.5 
|- ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )
Assertion refsumcn 
|- ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 refsumcn.1 
 |-  F/ x ph
2 refsumcn.2 
 |-  K = ( topGen ` ran (,) )
3 refsumcn.3 
 |-  ( ph -> J e. ( TopOn ` X ) )
4 refsumcn.4 
 |-  ( ph -> A e. Fin )
5 refsumcn.5 
 |-  ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )
6 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
7 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
8 2 7 eqtri 
 |-  K = ( ( TopOpen ` CCfld ) |`t RR )
9 8 oveq2i 
 |-  ( J Cn K ) = ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) )
10 5 9 eleqtrdi 
 |-  ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) ) )
11 6 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
12 11 a1i 
 |-  ( ( ph /\ k e. A ) -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
13 3 adantr 
 |-  ( ( ph /\ k e. A ) -> J e. ( TopOn ` X ) )
14 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
15 2 14 eqeltri 
 |-  K e. ( TopOn ` RR )
16 15 a1i 
 |-  ( ( ph /\ k e. A ) -> K e. ( TopOn ` RR ) )
17 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` RR ) /\ ( x e. X |-> B ) e. ( J Cn K ) ) -> ( x e. X |-> B ) : X --> RR )
18 13 16 5 17 syl3anc 
 |-  ( ( ph /\ k e. A ) -> ( x e. X |-> B ) : X --> RR )
19 18 frnd 
 |-  ( ( ph /\ k e. A ) -> ran ( x e. X |-> B ) C_ RR )
20 ax-resscn 
 |-  RR C_ CC
21 20 a1i 
 |-  ( ( ph /\ k e. A ) -> RR C_ CC )
22 cnrest2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran ( x e. X |-> B ) C_ RR /\ RR C_ CC ) -> ( ( x e. X |-> B ) e. ( J Cn ( TopOpen ` CCfld ) ) <-> ( x e. X |-> B ) e. ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
23 12 19 21 22 syl3anc 
 |-  ( ( ph /\ k e. A ) -> ( ( x e. X |-> B ) e. ( J Cn ( TopOpen ` CCfld ) ) <-> ( x e. X |-> B ) e. ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
24 10 23 mpbird 
 |-  ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn ( TopOpen ` CCfld ) ) )
25 6 3 4 24 fsumcnf 
 |-  ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn ( TopOpen ` CCfld ) ) )
26 11 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
27 4 adantr 
 |-  ( ( ph /\ x e. X ) -> A e. Fin )
28 simpll 
 |-  ( ( ( ph /\ x e. X ) /\ k e. A ) -> ph )
29 simpr 
 |-  ( ( ( ph /\ x e. X ) /\ k e. A ) -> k e. A )
30 28 29 jca 
 |-  ( ( ( ph /\ x e. X ) /\ k e. A ) -> ( ph /\ k e. A ) )
31 simplr 
 |-  ( ( ( ph /\ x e. X ) /\ k e. A ) -> x e. X )
32 eqid 
 |-  ( x e. X |-> B ) = ( x e. X |-> B )
33 32 fmpt 
 |-  ( A. x e. X B e. RR <-> ( x e. X |-> B ) : X --> RR )
34 18 33 sylibr 
 |-  ( ( ph /\ k e. A ) -> A. x e. X B e. RR )
35 rsp 
 |-  ( A. x e. X B e. RR -> ( x e. X -> B e. RR ) )
36 34 35 syl 
 |-  ( ( ph /\ k e. A ) -> ( x e. X -> B e. RR ) )
37 30 31 36 sylc 
 |-  ( ( ( ph /\ x e. X ) /\ k e. A ) -> B e. RR )
38 27 37 fsumrecl 
 |-  ( ( ph /\ x e. X ) -> sum_ k e. A B e. RR )
39 38 ex 
 |-  ( ph -> ( x e. X -> sum_ k e. A B e. RR ) )
40 1 39 ralrimi 
 |-  ( ph -> A. x e. X sum_ k e. A B e. RR )
41 eqid 
 |-  ( x e. X |-> sum_ k e. A B ) = ( x e. X |-> sum_ k e. A B )
42 41 fnmpt 
 |-  ( A. x e. X sum_ k e. A B e. RR -> ( x e. X |-> sum_ k e. A B ) Fn X )
43 40 42 syl 
 |-  ( ph -> ( x e. X |-> sum_ k e. A B ) Fn X )
44 nfcv 
 |-  F/_ x X
45 nfcv 
 |-  F/_ x y
46 nfmpt1 
 |-  F/_ x ( x e. X |-> sum_ k e. A B )
47 44 45 46 fvelrnbf 
 |-  ( ( x e. X |-> sum_ k e. A B ) Fn X -> ( y e. ran ( x e. X |-> sum_ k e. A B ) <-> E. x e. X ( ( x e. X |-> sum_ k e. A B ) ` x ) = y ) )
48 43 47 syl 
 |-  ( ph -> ( y e. ran ( x e. X |-> sum_ k e. A B ) <-> E. x e. X ( ( x e. X |-> sum_ k e. A B ) ` x ) = y ) )
49 48 biimpa 
 |-  ( ( ph /\ y e. ran ( x e. X |-> sum_ k e. A B ) ) -> E. x e. X ( ( x e. X |-> sum_ k e. A B ) ` x ) = y )
50 46 nfrn 
 |-  F/_ x ran ( x e. X |-> sum_ k e. A B )
51 50 nfcri 
 |-  F/ x y e. ran ( x e. X |-> sum_ k e. A B )
52 1 51 nfan 
 |-  F/ x ( ph /\ y e. ran ( x e. X |-> sum_ k e. A B ) )
53 nfcv 
 |-  F/_ x RR
54 53 nfcri 
 |-  F/ x y e. RR
55 simpr 
 |-  ( ( ph /\ x e. X ) -> x e. X )
56 55 38 jca 
 |-  ( ( ph /\ x e. X ) -> ( x e. X /\ sum_ k e. A B e. RR ) )
57 41 fvmpt2 
 |-  ( ( x e. X /\ sum_ k e. A B e. RR ) -> ( ( x e. X |-> sum_ k e. A B ) ` x ) = sum_ k e. A B )
58 56 57 syl 
 |-  ( ( ph /\ x e. X ) -> ( ( x e. X |-> sum_ k e. A B ) ` x ) = sum_ k e. A B )
59 58 3adant3 
 |-  ( ( ph /\ x e. X /\ ( ( x e. X |-> sum_ k e. A B ) ` x ) = y ) -> ( ( x e. X |-> sum_ k e. A B ) ` x ) = sum_ k e. A B )
60 simp3 
 |-  ( ( ph /\ x e. X /\ ( ( x e. X |-> sum_ k e. A B ) ` x ) = y ) -> ( ( x e. X |-> sum_ k e. A B ) ` x ) = y )
61 59 60 eqtr3d 
 |-  ( ( ph /\ x e. X /\ ( ( x e. X |-> sum_ k e. A B ) ` x ) = y ) -> sum_ k e. A B = y )
62 38 3adant3 
 |-  ( ( ph /\ x e. X /\ ( ( x e. X |-> sum_ k e. A B ) ` x ) = y ) -> sum_ k e. A B e. RR )
63 61 62 eqeltrrd 
 |-  ( ( ph /\ x e. X /\ ( ( x e. X |-> sum_ k e. A B ) ` x ) = y ) -> y e. RR )
64 63 3adant1r 
 |-  ( ( ( ph /\ y e. ran ( x e. X |-> sum_ k e. A B ) ) /\ x e. X /\ ( ( x e. X |-> sum_ k e. A B ) ` x ) = y ) -> y e. RR )
65 64 3exp 
 |-  ( ( ph /\ y e. ran ( x e. X |-> sum_ k e. A B ) ) -> ( x e. X -> ( ( ( x e. X |-> sum_ k e. A B ) ` x ) = y -> y e. RR ) ) )
66 52 54 65 rexlimd 
 |-  ( ( ph /\ y e. ran ( x e. X |-> sum_ k e. A B ) ) -> ( E. x e. X ( ( x e. X |-> sum_ k e. A B ) ` x ) = y -> y e. RR ) )
67 49 66 mpd 
 |-  ( ( ph /\ y e. ran ( x e. X |-> sum_ k e. A B ) ) -> y e. RR )
68 67 ex 
 |-  ( ph -> ( y e. ran ( x e. X |-> sum_ k e. A B ) -> y e. RR ) )
69 68 ssrdv 
 |-  ( ph -> ran ( x e. X |-> sum_ k e. A B ) C_ RR )
70 20 a1i 
 |-  ( ph -> RR C_ CC )
71 cnrest2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran ( x e. X |-> sum_ k e. A B ) C_ RR /\ RR C_ CC ) -> ( ( x e. X |-> sum_ k e. A B ) e. ( J Cn ( TopOpen ` CCfld ) ) <-> ( x e. X |-> sum_ k e. A B ) e. ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
72 26 69 70 71 syl3anc 
 |-  ( ph -> ( ( x e. X |-> sum_ k e. A B ) e. ( J Cn ( TopOpen ` CCfld ) ) <-> ( x e. X |-> sum_ k e. A B ) e. ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
73 25 72 mpbid 
 |-  ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) ) )
74 73 9 eleqtrrdi 
 |-  ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn K ) )