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 φ A
fsumo1.2 φ B Fin
fsumo1.3 φ x A k B C V
fsumo1.4 φ k B x A C 𝑂1
Assertion fsumo1 φ x A k B C 𝑂1

Proof

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