Metamath Proof Explorer

Theorem fsumo1

Description: The finite sum of eventually bounded functions (where the index set B does not depend on x ) is eventually bounded. (Contributed by Mario Carneiro, 30-Apr-2016) (Proof shortened by Mario Carneiro, 22-May-2016)

Ref Expression
Hypotheses fsumo1.1 
|- ( ph -> A C_ RR )
fsumo1.2 
|- ( ph -> B e. Fin )
fsumo1.3 
|- ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. V )
fsumo1.4 
|- ( ( ph /\ k e. B ) -> ( x e. A |-> C ) e. O(1) )
Assertion fsumo1 
|- ( ph -> ( x e. A |-> sum_ k e. B C ) e. O(1) )

Proof

Step Hyp Ref Expression
1 fsumo1.1 
 |-  ( ph -> A C_ RR )
2 fsumo1.2 
 |-  ( ph -> B e. Fin )
3 fsumo1.3 
 |-  ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. V )
4 fsumo1.4 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> C ) e. O(1) )
5 ssid 
 |-  B C_ B
6 sseq1 
 |-  ( w = (/) -> ( w C_ B <-> (/) C_ B ) )
7 sumeq1 
 |-  ( w = (/) -> sum_ k e. w C = sum_ k e. (/) C )
8 sum0 
 |-  sum_ k e. (/) C = 0
9 7 8 eqtrdi 
 |-  ( w = (/) -> sum_ k e. w C = 0 )
10 9 mpteq2dv 
 |-  ( w = (/) -> ( x e. A |-> sum_ k e. w C ) = ( x e. A |-> 0 ) )
11 10 eleq1d 
 |-  ( w = (/) -> ( ( x e. A |-> sum_ k e. w C ) e. O(1) <-> ( x e. A |-> 0 ) e. O(1) ) )
12 6 11 imbi12d 
 |-  ( w = (/) -> ( ( w C_ B -> ( x e. A |-> sum_ k e. w C ) e. O(1) ) <-> ( (/) C_ B -> ( x e. A |-> 0 ) e. O(1) ) ) )
13 12 imbi2d 
 |-  ( w = (/) -> ( ( ph -> ( w C_ B -> ( x e. A |-> sum_ k e. w C ) e. O(1) ) ) <-> ( ph -> ( (/) C_ B -> ( x e. A |-> 0 ) e. O(1) ) ) ) )
14 sseq1 
 |-  ( w = y -> ( w C_ B <-> y C_ B ) )
15 sumeq1 
 |-  ( w = y -> sum_ k e. w C = sum_ k e. y C )
16 15 mpteq2dv 
 |-  ( w = y -> ( x e. A |-> sum_ k e. w C ) = ( x e. A |-> sum_ k e. y C ) )
17 16 eleq1d 
 |-  ( w = y -> ( ( x e. A |-> sum_ k e. w C ) e. O(1) <-> ( x e. A |-> sum_ k e. y C ) e. O(1) ) )
18 14 17 imbi12d 
 |-  ( w = y -> ( ( w C_ B -> ( x e. A |-> sum_ k e. w C ) e. O(1) ) <-> ( y C_ B -> ( x e. A |-> sum_ k e. y C ) e. O(1) ) ) )
19 18 imbi2d 
 |-  ( w = y -> ( ( ph -> ( w C_ B -> ( x e. A |-> sum_ k e. w C ) e. O(1) ) ) <-> ( ph -> ( y C_ B -> ( x e. A |-> sum_ k e. y C ) e. O(1) ) ) ) )
20 sseq1 
 |-  ( w = ( y u. { z } ) -> ( w C_ B <-> ( y u. { z } ) C_ B ) )
21 sumeq1 
 |-  ( w = ( y u. { z } ) -> sum_ k e. w C = sum_ k e. ( y u. { z } ) C )
22 21 mpteq2dv 
 |-  ( w = ( y u. { z } ) -> ( x e. A |-> sum_ k e. w C ) = ( x e. A |-> sum_ k e. ( y u. { z } ) C ) )
23 22 eleq1d 
 |-  ( w = ( y u. { z } ) -> ( ( x e. A |-> sum_ k e. w C ) e. O(1) <-> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) e. O(1) ) )
24 20 23 imbi12d 
 |-  ( w = ( y u. { z } ) -> ( ( w C_ B -> ( x e. A |-> sum_ k e. w C ) e. O(1) ) <-> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) e. O(1) ) ) )
25 24 imbi2d 
 |-  ( w = ( y u. { z } ) -> ( ( ph -> ( w C_ B -> ( x e. A |-> sum_ k e. w C ) e. O(1) ) ) <-> ( ph -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) e. O(1) ) ) ) )
26 sseq1 
 |-  ( w = B -> ( w C_ B <-> B C_ B ) )
27 sumeq1 
 |-  ( w = B -> sum_ k e. w C = sum_ k e. B C )
28 27 mpteq2dv 
 |-  ( w = B -> ( x e. A |-> sum_ k e. w C ) = ( x e. A |-> sum_ k e. B C ) )
29 28 eleq1d 
 |-  ( w = B -> ( ( x e. A |-> sum_ k e. w C ) e. O(1) <-> ( x e. A |-> sum_ k e. B C ) e. O(1) ) )
30 26 29 imbi12d 
 |-  ( w = B -> ( ( w C_ B -> ( x e. A |-> sum_ k e. w C ) e. O(1) ) <-> ( B C_ B -> ( x e. A |-> sum_ k e. B C ) e. O(1) ) ) )
31 30 imbi2d 
 |-  ( w = B -> ( ( ph -> ( w C_ B -> ( x e. A |-> sum_ k e. w C ) e. O(1) ) ) <-> ( ph -> ( B C_ B -> ( x e. A |-> sum_ k e. B C ) e. O(1) ) ) ) )
32 0cn 
 |-  0 e. CC
33 o1const 
 |-  ( ( A C_ RR /\ 0 e. CC ) -> ( x e. A |-> 0 ) e. O(1) )
34 1 32 33 sylancl 
 |-  ( ph -> ( x e. A |-> 0 ) e. O(1) )
35 34 a1d 
 |-  ( ph -> ( (/) C_ B -> ( x e. A |-> 0 ) e. O(1) ) )
36 ssun1 
 |-  y C_ ( y u. { z } )
37 sstr 
 |-  ( ( y C_ ( y u. { z } ) /\ ( y u. { z } ) C_ B ) -> y C_ B )
38 36 37 mpan 
 |-  ( ( y u. { z } ) C_ B -> y C_ B )
39 38 imim1i 
 |-  ( ( y C_ B -> ( x e. A |-> sum_ k e. y C ) e. O(1) ) -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. y C ) e. O(1) ) )
40 simprl 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> -. z e. y )
41 disjsn 
 |-  ( ( y i^i { z } ) = (/) <-> -. z e. y )
42 40 41 sylibr 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( y i^i { z } ) = (/) )
43 42 adantr 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> ( y i^i { z } ) = (/) )
44 eqidd 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> ( y u. { z } ) = ( y u. { z } ) )
45 2 adantr 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> B e. Fin )
46 simprr 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( y u. { z } ) C_ B )
47 45 46 ssfid 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( y u. { z } ) e. Fin )
48 47 adantr 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> ( y u. { z } ) e. Fin )
49 46 sselda 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ k e. ( y u. { z } ) ) -> k e. B )
50 49 adantlr 
 |-  ( ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) /\ k e. ( y u. { z } ) ) -> k e. B )
51 3 anass1rs 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) -> C e. V )
52 51 4 o1mptrcl 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) -> C e. CC )
53 52 an32s 
 |-  ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. CC )
54 53 adantllr 
 |-  ( ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) /\ k e. B ) -> C e. CC )
55 50 54 syldan 
 |-  ( ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) /\ k e. ( y u. { z } ) ) -> C e. CC )
56 43 44 48 55 fsumsplit 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ k e. ( y u. { z } ) C = ( sum_ k e. y C + sum_ k e. { z } C ) )
57 nfcv 
 |-  F/_ w C
58 nfcsb1v 
 |-  F/_ k [_ w / k ]_ C
59 csbeq1a 
 |-  ( k = w -> C = [_ w / k ]_ C )
60 57 58 59 cbvsumi 
 |-  sum_ k e. { z } C = sum_ w e. { z } [_ w / k ]_ C
61 46 unssbd 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> { z } C_ B )
62 vex 
 |-  z e. _V
63 62 snss 
 |-  ( z e. B <-> { z } C_ B )
64 61 63 sylibr 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> z e. B )
65 64 adantr 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> z e. B )
66 54 ralrimiva 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> A. k e. B C e. CC )
67 nfcsb1v 
 |-  F/_ k [_ z / k ]_ C
68 67 nfel1 
 |-  F/ k [_ z / k ]_ C e. CC
69 csbeq1a 
 |-  ( k = z -> C = [_ z / k ]_ C )
70 69 eleq1d 
 |-  ( k = z -> ( C e. CC <-> [_ z / k ]_ C e. CC ) )
71 68 70 rspc 
 |-  ( z e. B -> ( A. k e. B C e. CC -> [_ z / k ]_ C e. CC ) )
72 65 66 71 sylc 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> [_ z / k ]_ C e. CC )
73 csbeq1 
 |-  ( w = z -> [_ w / k ]_ C = [_ z / k ]_ C )
74 73 sumsn 
 |-  ( ( z e. B /\ [_ z / k ]_ C e. CC ) -> sum_ w e. { z } [_ w / k ]_ C = [_ z / k ]_ C )
75 65 72 74 syl2anc 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ w e. { z } [_ w / k ]_ C = [_ z / k ]_ C )
76 60 75 syl5eq 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ k e. { z } C = [_ z / k ]_ C )
77 76 oveq2d 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> ( sum_ k e. y C + sum_ k e. { z } C ) = ( sum_ k e. y C + [_ z / k ]_ C ) )
78 56 77 eqtrd 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ k e. ( y u. { z } ) C = ( sum_ k e. y C + [_ z / k ]_ C ) )
79 78 mpteq2dva 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) = ( x e. A |-> ( sum_ k e. y C + [_ z / k ]_ C ) ) )
80 1 adantr 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> A C_ RR )
81 reex 
 |-  RR e. _V
82 81 ssex 
 |-  ( A C_ RR -> A e. _V )
83 80 82 syl 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> A e. _V )
84 sumex 
 |-  sum_ k e. y C e. _V
85 84 a1i 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ k e. y C e. _V )
86 eqidd 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( x e. A |-> sum_ k e. y C ) = ( x e. A |-> sum_ k e. y C ) )
87 eqidd 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( x e. A |-> [_ z / k ]_ C ) = ( x e. A |-> [_ z / k ]_ C ) )
88 83 85 72 86 87 offval2 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( ( x e. A |-> sum_ k e. y C ) oF + ( x e. A |-> [_ z / k ]_ C ) ) = ( x e. A |-> ( sum_ k e. y C + [_ z / k ]_ C ) ) )
89 79 88 eqtr4d 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) = ( ( x e. A |-> sum_ k e. y C ) oF + ( x e. A |-> [_ z / k ]_ C ) ) )
90 89 adantr 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) e. O(1) ) -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) = ( ( x e. A |-> sum_ k e. y C ) oF + ( x e. A |-> [_ z / k ]_ C ) ) )
91 id 
 |-  ( ( x e. A |-> sum_ k e. y C ) e. O(1) -> ( x e. A |-> sum_ k e. y C ) e. O(1) )
92 4 ralrimiva 
 |-  ( ph -> A. k e. B ( x e. A |-> C ) e. O(1) )
93 92 adantr 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> A. k e. B ( x e. A |-> C ) e. O(1) )
94 nfcv 
 |-  F/_ k A
95 94 67 nfmpt 
 |-  F/_ k ( x e. A |-> [_ z / k ]_ C )
96 95 nfel1 
 |-  F/ k ( x e. A |-> [_ z / k ]_ C ) e. O(1)
97 69 mpteq2dv 
 |-  ( k = z -> ( x e. A |-> C ) = ( x e. A |-> [_ z / k ]_ C ) )
98 97 eleq1d 
 |-  ( k = z -> ( ( x e. A |-> C ) e. O(1) <-> ( x e. A |-> [_ z / k ]_ C ) e. O(1) ) )
99 96 98 rspc 
 |-  ( z e. B -> ( A. k e. B ( x e. A |-> C ) e. O(1) -> ( x e. A |-> [_ z / k ]_ C ) e. O(1) ) )
100 64 93 99 sylc 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( x e. A |-> [_ z / k ]_ C ) e. O(1) )
101 o1add 
 |-  ( ( ( x e. A |-> sum_ k e. y C ) e. O(1) /\ ( x e. A |-> [_ z / k ]_ C ) e. O(1) ) -> ( ( x e. A |-> sum_ k e. y C ) oF + ( x e. A |-> [_ z / k ]_ C ) ) e. O(1) )
102 91 100 101 syl2anr 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) e. O(1) ) -> ( ( x e. A |-> sum_ k e. y C ) oF + ( x e. A |-> [_ z / k ]_ C ) ) e. O(1) )
103 90 102 eqeltrd 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) e. O(1) ) -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) e. O(1) )
104 103 ex 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( ( x e. A |-> sum_ k e. y C ) e. O(1) -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) e. O(1) ) )
105 104 expr 
 |-  ( ( ph /\ -. z e. y ) -> ( ( y u. { z } ) C_ B -> ( ( x e. A |-> sum_ k e. y C ) e. O(1) -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) e. O(1) ) ) )
106 105 a2d 
 |-  ( ( ph /\ -. z e. y ) -> ( ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. y C ) e. O(1) ) -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) e. O(1) ) ) )
107 39 106 syl5 
 |-  ( ( ph /\ -. z e. y ) -> ( ( y C_ B -> ( x e. A |-> sum_ k e. y C ) e. O(1) ) -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) e. O(1) ) ) )
108 107 expcom 
 |-  ( -. z e. y -> ( ph -> ( ( y C_ B -> ( x e. A |-> sum_ k e. y C ) e. O(1) ) -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) e. O(1) ) ) ) )
109 108 a2d 
 |-  ( -. z e. y -> ( ( ph -> ( y C_ B -> ( x e. A |-> sum_ k e. y C ) e. O(1) ) ) -> ( ph -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) e. O(1) ) ) ) )
110 109 adantl 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ph -> ( y C_ B -> ( x e. A |-> sum_ k e. y C ) e. O(1) ) ) -> ( ph -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) e. O(1) ) ) ) )
111 13 19 25 31 35 110 findcard2s 
 |-  ( B e. Fin -> ( ph -> ( B C_ B -> ( x e. A |-> sum_ k e. B C ) e. O(1) ) ) )
112 2 111 mpcom 
 |-  ( ph -> ( B C_ B -> ( x e. A |-> sum_ k e. B C ) e. O(1) ) )
113 5 112 mpi 
 |-  ( ph -> ( x e. A |-> sum_ k e. B C ) e. O(1) )