Metamath Proof Explorer

Theorem fsumcn

Description: A finite sum of functions to complex numbers from a common topological space is continuous. The class expression for B normally contains free variables k and x to index it. (Contributed by NM, 8-Aug-2007) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses fsumcn.3 
|- K = ( TopOpen ` CCfld )
fsumcn.4 
|- ( ph -> J e. ( TopOn ` X ) )
fsumcn.5 
|- ( ph -> A e. Fin )
fsumcn.6 
|- ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )
Assertion fsumcn 
|- ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 fsumcn.3 
 |-  K = ( TopOpen ` CCfld )
2 fsumcn.4 
 |-  ( ph -> J e. ( TopOn ` X ) )
3 fsumcn.5 
 |-  ( ph -> A e. Fin )
4 fsumcn.6 
 |-  ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )
5 ssid 
 |-  A C_ A
6 sseq1 
 |-  ( w = (/) -> ( w C_ A <-> (/) C_ A ) )
7 sumeq1 
 |-  ( w = (/) -> sum_ k e. w B = sum_ k e. (/) B )
8 7 mpteq2dv 
 |-  ( w = (/) -> ( x e. X |-> sum_ k e. w B ) = ( x e. X |-> sum_ k e. (/) B ) )
9 8 eleq1d 
 |-  ( w = (/) -> ( ( x e. X |-> sum_ k e. w B ) e. ( J Cn K ) <-> ( x e. X |-> sum_ k e. (/) B ) e. ( J Cn K ) ) )
10 6 9 imbi12d 
 |-  ( w = (/) -> ( ( w C_ A -> ( x e. X |-> sum_ k e. w B ) e. ( J Cn K ) ) <-> ( (/) C_ A -> ( x e. X |-> sum_ k e. (/) B ) e. ( J Cn K ) ) ) )
11 10 imbi2d 
 |-  ( w = (/) -> ( ( ph -> ( w C_ A -> ( x e. X |-> sum_ k e. w B ) e. ( J Cn K ) ) ) <-> ( ph -> ( (/) C_ A -> ( x e. X |-> sum_ k e. (/) B ) e. ( J Cn K ) ) ) ) )
12 sseq1 
 |-  ( w = y -> ( w C_ A <-> y C_ A ) )
13 sumeq1 
 |-  ( w = y -> sum_ k e. w B = sum_ k e. y B )
14 13 mpteq2dv 
 |-  ( w = y -> ( x e. X |-> sum_ k e. w B ) = ( x e. X |-> sum_ k e. y B ) )
15 14 eleq1d 
 |-  ( w = y -> ( ( x e. X |-> sum_ k e. w B ) e. ( J Cn K ) <-> ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) )
16 12 15 imbi12d 
 |-  ( w = y -> ( ( w C_ A -> ( x e. X |-> sum_ k e. w B ) e. ( J Cn K ) ) <-> ( y C_ A -> ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) ) )
17 16 imbi2d 
 |-  ( w = y -> ( ( ph -> ( w C_ A -> ( x e. X |-> sum_ k e. w B ) e. ( J Cn K ) ) ) <-> ( ph -> ( y C_ A -> ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) ) ) )
18 sseq1 
 |-  ( w = ( y u. { z } ) -> ( w C_ A <-> ( y u. { z } ) C_ A ) )
19 sumeq1 
 |-  ( w = ( y u. { z } ) -> sum_ k e. w B = sum_ k e. ( y u. { z } ) B )
20 19 mpteq2dv 
 |-  ( w = ( y u. { z } ) -> ( x e. X |-> sum_ k e. w B ) = ( x e. X |-> sum_ k e. ( y u. { z } ) B ) )
21 20 eleq1d 
 |-  ( w = ( y u. { z } ) -> ( ( x e. X |-> sum_ k e. w B ) e. ( J Cn K ) <-> ( x e. X |-> sum_ k e. ( y u. { z } ) B ) e. ( J Cn K ) ) )
22 18 21 imbi12d 
 |-  ( w = ( y u. { z } ) -> ( ( w C_ A -> ( x e. X |-> sum_ k e. w B ) e. ( J Cn K ) ) <-> ( ( y u. { z } ) C_ A -> ( x e. X |-> sum_ k e. ( y u. { z } ) B ) e. ( J Cn K ) ) ) )
23 22 imbi2d 
 |-  ( w = ( y u. { z } ) -> ( ( ph -> ( w C_ A -> ( x e. X |-> sum_ k e. w B ) e. ( J Cn K ) ) ) <-> ( ph -> ( ( y u. { z } ) C_ A -> ( x e. X |-> sum_ k e. ( y u. { z } ) B ) e. ( J Cn K ) ) ) ) )
24 sseq1 
 |-  ( w = A -> ( w C_ A <-> A C_ A ) )
25 sumeq1 
 |-  ( w = A -> sum_ k e. w B = sum_ k e. A B )
26 25 mpteq2dv 
 |-  ( w = A -> ( x e. X |-> sum_ k e. w B ) = ( x e. X |-> sum_ k e. A B ) )
27 26 eleq1d 
 |-  ( w = A -> ( ( x e. X |-> sum_ k e. w B ) e. ( J Cn K ) <-> ( x e. X |-> sum_ k e. A B ) e. ( J Cn K ) ) )
28 24 27 imbi12d 
 |-  ( w = A -> ( ( w C_ A -> ( x e. X |-> sum_ k e. w B ) e. ( J Cn K ) ) <-> ( A C_ A -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn K ) ) ) )
29 28 imbi2d 
 |-  ( w = A -> ( ( ph -> ( w C_ A -> ( x e. X |-> sum_ k e. w B ) e. ( J Cn K ) ) ) <-> ( ph -> ( A C_ A -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn K ) ) ) ) )
30 sum0 
 |-  sum_ k e. (/) B = 0
31 30 mpteq2i 
 |-  ( x e. X |-> sum_ k e. (/) B ) = ( x e. X |-> 0 )
32 1 cnfldtopon 
 |-  K e. ( TopOn ` CC )
33 32 a1i 
 |-  ( ph -> K e. ( TopOn ` CC ) )
34 0cnd 
 |-  ( ph -> 0 e. CC )
35 2 33 34 cnmptc 
 |-  ( ph -> ( x e. X |-> 0 ) e. ( J Cn K ) )
36 31 35 eqeltrid 
 |-  ( ph -> ( x e. X |-> sum_ k e. (/) B ) e. ( J Cn K ) )
37 36 a1d 
 |-  ( ph -> ( (/) C_ A -> ( x e. X |-> sum_ k e. (/) B ) e. ( J Cn K ) ) )
38 ssun1 
 |-  y C_ ( y u. { z } )
39 sstr 
 |-  ( ( y C_ ( y u. { z } ) /\ ( y u. { z } ) C_ A ) -> y C_ A )
40 38 39 mpan 
 |-  ( ( y u. { z } ) C_ A -> y C_ A )
41 40 imim1i 
 |-  ( ( y C_ A -> ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) -> ( ( y u. { z } ) C_ A -> ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) )
42 simplr 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) -> -. z e. y )
43 disjsn 
 |-  ( ( y i^i { z } ) = (/) <-> -. z e. y )
44 42 43 sylibr 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) -> ( y i^i { z } ) = (/) )
45 eqidd 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) -> ( y u. { z } ) = ( y u. { z } ) )
46 3 ad2antrr 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) -> A e. Fin )
47 simprl 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) -> ( y u. { z } ) C_ A )
48 46 47 ssfid 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) -> ( y u. { z } ) e. Fin )
49 simplll 
 |-  ( ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) /\ k e. ( y u. { z } ) ) -> ph )
50 47 sselda 
 |-  ( ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) /\ k e. ( y u. { z } ) ) -> k e. A )
51 simplrr 
 |-  ( ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) /\ k e. ( y u. { z } ) ) -> x e. X )
52 2 adantr 
 |-  ( ( ph /\ k e. A ) -> J e. ( TopOn ` X ) )
53 32 a1i 
 |-  ( ( ph /\ k e. A ) -> K e. ( TopOn ` CC ) )
54 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` CC ) /\ ( x e. X |-> B ) e. ( J Cn K ) ) -> ( x e. X |-> B ) : X --> CC )
55 52 53 4 54 syl3anc 
 |-  ( ( ph /\ k e. A ) -> ( x e. X |-> B ) : X --> CC )
56 eqid 
 |-  ( x e. X |-> B ) = ( x e. X |-> B )
57 56 fmpt 
 |-  ( A. x e. X B e. CC <-> ( x e. X |-> B ) : X --> CC )
58 55 57 sylibr 
 |-  ( ( ph /\ k e. A ) -> A. x e. X B e. CC )
59 rsp 
 |-  ( A. x e. X B e. CC -> ( x e. X -> B e. CC ) )
60 58 59 syl 
 |-  ( ( ph /\ k e. A ) -> ( x e. X -> B e. CC ) )
61 60 imp 
 |-  ( ( ( ph /\ k e. A ) /\ x e. X ) -> B e. CC )
62 49 50 51 61 syl21anc 
 |-  ( ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) /\ k e. ( y u. { z } ) ) -> B e. CC )
63 44 45 48 62 fsumsplit 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) -> sum_ k e. ( y u. { z } ) B = ( sum_ k e. y B + sum_ k e. { z } B ) )
64 simpr 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( y u. { z } ) C_ A ) -> ( y u. { z } ) C_ A )
65 64 unssbd 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( y u. { z } ) C_ A ) -> { z } C_ A )
66 vex 
 |-  z e. _V
67 66 snss 
 |-  ( z e. A <-> { z } C_ A )
68 65 67 sylibr 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( y u. { z } ) C_ A ) -> z e. A )
69 68 adantrr 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) -> z e. A )
70 60 impancom 
 |-  ( ( ph /\ x e. X ) -> ( k e. A -> B e. CC ) )
71 70 ralrimiv 
 |-  ( ( ph /\ x e. X ) -> A. k e. A B e. CC )
72 71 ad2ant2rl 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) -> A. k e. A B e. CC )
73 nfcsb1v 
 |-  F/_ k [_ z / k ]_ B
74 73 nfel1 
 |-  F/ k [_ z / k ]_ B e. CC
75 csbeq1a 
 |-  ( k = z -> B = [_ z / k ]_ B )
76 75 eleq1d 
 |-  ( k = z -> ( B e. CC <-> [_ z / k ]_ B e. CC ) )
77 74 76 rspc 
 |-  ( z e. A -> ( A. k e. A B e. CC -> [_ z / k ]_ B e. CC ) )
78 69 72 77 sylc 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) -> [_ z / k ]_ B e. CC )
79 sumsns 
 |-  ( ( z e. A /\ [_ z / k ]_ B e. CC ) -> sum_ k e. { z } B = [_ z / k ]_ B )
80 69 78 79 syl2anc 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) -> sum_ k e. { z } B = [_ z / k ]_ B )
81 80 oveq2d 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) -> ( sum_ k e. y B + sum_ k e. { z } B ) = ( sum_ k e. y B + [_ z / k ]_ B ) )
82 63 81 eqtrd 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ x e. X ) ) -> sum_ k e. ( y u. { z } ) B = ( sum_ k e. y B + [_ z / k ]_ B ) )
83 82 anassrs 
 |-  ( ( ( ( ph /\ -. z e. y ) /\ ( y u. { z } ) C_ A ) /\ x e. X ) -> sum_ k e. ( y u. { z } ) B = ( sum_ k e. y B + [_ z / k ]_ B ) )
84 83 mpteq2dva 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( y u. { z } ) C_ A ) -> ( x e. X |-> sum_ k e. ( y u. { z } ) B ) = ( x e. X |-> ( sum_ k e. y B + [_ z / k ]_ B ) ) )
85 84 adantrr 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) ) -> ( x e. X |-> sum_ k e. ( y u. { z } ) B ) = ( x e. X |-> ( sum_ k e. y B + [_ z / k ]_ B ) ) )
86 nfcv 
 |-  F/_ w ( sum_ k e. y B + [_ z / k ]_ B )
87 nfcv 
 |-  F/_ x y
88 nfcsb1v 
 |-  F/_ x [_ w / x ]_ B
89 87 88 nfsum 
 |-  F/_ x sum_ k e. y [_ w / x ]_ B
90 nfcv 
 |-  F/_ x +
91 nfcv 
 |-  F/_ x z
92 91 88 nfcsbw 
 |-  F/_ x [_ z / k ]_ [_ w / x ]_ B
93 89 90 92 nfov 
 |-  F/_ x ( sum_ k e. y [_ w / x ]_ B + [_ z / k ]_ [_ w / x ]_ B )
94 csbeq1a 
 |-  ( x = w -> B = [_ w / x ]_ B )
95 94 sumeq2sdv 
 |-  ( x = w -> sum_ k e. y B = sum_ k e. y [_ w / x ]_ B )
96 94 csbeq2dv 
 |-  ( x = w -> [_ z / k ]_ B = [_ z / k ]_ [_ w / x ]_ B )
97 95 96 oveq12d 
 |-  ( x = w -> ( sum_ k e. y B + [_ z / k ]_ B ) = ( sum_ k e. y [_ w / x ]_ B + [_ z / k ]_ [_ w / x ]_ B ) )
98 86 93 97 cbvmpt 
 |-  ( x e. X |-> ( sum_ k e. y B + [_ z / k ]_ B ) ) = ( w e. X |-> ( sum_ k e. y [_ w / x ]_ B + [_ z / k ]_ [_ w / x ]_ B ) )
99 85 98 eqtrdi 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) ) -> ( x e. X |-> sum_ k e. ( y u. { z } ) B ) = ( w e. X |-> ( sum_ k e. y [_ w / x ]_ B + [_ z / k ]_ [_ w / x ]_ B ) ) )
100 2 ad2antrr 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) ) -> J e. ( TopOn ` X ) )
101 nfcv 
 |-  F/_ w sum_ k e. y B
102 101 89 95 cbvmpt 
 |-  ( x e. X |-> sum_ k e. y B ) = ( w e. X |-> sum_ k e. y [_ w / x ]_ B )
103 simprr 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) ) -> ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) )
104 102 103 eqeltrrid 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) ) -> ( w e. X |-> sum_ k e. y [_ w / x ]_ B ) e. ( J Cn K ) )
105 nfcv 
 |-  F/_ w [_ z / k ]_ B
106 105 92 96 cbvmpt 
 |-  ( x e. X |-> [_ z / k ]_ B ) = ( w e. X |-> [_ z / k ]_ [_ w / x ]_ B )
107 68 adantrr 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) ) -> z e. A )
108 4 ralrimiva 
 |-  ( ph -> A. k e. A ( x e. X |-> B ) e. ( J Cn K ) )
109 108 ad2antrr 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) ) -> A. k e. A ( x e. X |-> B ) e. ( J Cn K ) )
110 nfcv 
 |-  F/_ k X
111 110 73 nfmpt 
 |-  F/_ k ( x e. X |-> [_ z / k ]_ B )
112 111 nfel1 
 |-  F/ k ( x e. X |-> [_ z / k ]_ B ) e. ( J Cn K )
113 75 mpteq2dv 
 |-  ( k = z -> ( x e. X |-> B ) = ( x e. X |-> [_ z / k ]_ B ) )
114 113 eleq1d 
 |-  ( k = z -> ( ( x e. X |-> B ) e. ( J Cn K ) <-> ( x e. X |-> [_ z / k ]_ B ) e. ( J Cn K ) ) )
115 112 114 rspc 
 |-  ( z e. A -> ( A. k e. A ( x e. X |-> B ) e. ( J Cn K ) -> ( x e. X |-> [_ z / k ]_ B ) e. ( J Cn K ) ) )
116 107 109 115 sylc 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) ) -> ( x e. X |-> [_ z / k ]_ B ) e. ( J Cn K ) )
117 106 116 eqeltrrid 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) ) -> ( w e. X |-> [_ z / k ]_ [_ w / x ]_ B ) e. ( J Cn K ) )
118 1 addcn 
 |-  + e. ( ( K tX K ) Cn K )
119 118 a1i 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) ) -> + e. ( ( K tX K ) Cn K ) )
120 100 104 117 119 cnmpt12f 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) ) -> ( w e. X |-> ( sum_ k e. y [_ w / x ]_ B + [_ z / k ]_ [_ w / x ]_ B ) ) e. ( J Cn K ) )
121 99 120 eqeltrd 
 |-  ( ( ( ph /\ -. z e. y ) /\ ( ( y u. { z } ) C_ A /\ ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) ) -> ( x e. X |-> sum_ k e. ( y u. { z } ) B ) e. ( J Cn K ) )
122 121 exp32 
 |-  ( ( ph /\ -. z e. y ) -> ( ( y u. { z } ) C_ A -> ( ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) -> ( x e. X |-> sum_ k e. ( y u. { z } ) B ) e. ( J Cn K ) ) ) )
123 122 a2d 
 |-  ( ( ph /\ -. z e. y ) -> ( ( ( y u. { z } ) C_ A -> ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) -> ( ( y u. { z } ) C_ A -> ( x e. X |-> sum_ k e. ( y u. { z } ) B ) e. ( J Cn K ) ) ) )
124 41 123 syl5 
 |-  ( ( ph /\ -. z e. y ) -> ( ( y C_ A -> ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) -> ( ( y u. { z } ) C_ A -> ( x e. X |-> sum_ k e. ( y u. { z } ) B ) e. ( J Cn K ) ) ) )
125 124 expcom 
 |-  ( -. z e. y -> ( ph -> ( ( y C_ A -> ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) -> ( ( y u. { z } ) C_ A -> ( x e. X |-> sum_ k e. ( y u. { z } ) B ) e. ( J Cn K ) ) ) ) )
126 125 adantl 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ph -> ( ( y C_ A -> ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) -> ( ( y u. { z } ) C_ A -> ( x e. X |-> sum_ k e. ( y u. { z } ) B ) e. ( J Cn K ) ) ) ) )
127 126 a2d 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ph -> ( y C_ A -> ( x e. X |-> sum_ k e. y B ) e. ( J Cn K ) ) ) -> ( ph -> ( ( y u. { z } ) C_ A -> ( x e. X |-> sum_ k e. ( y u. { z } ) B ) e. ( J Cn K ) ) ) ) )
128 11 17 23 29 37 127 findcard2s 
 |-  ( A e. Fin -> ( ph -> ( A C_ A -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn K ) ) ) )
129 3 128 mpcom 
 |-  ( ph -> ( A C_ A -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn K ) ) )
130 5 129 mpi 
 |-  ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn K ) )