Metamath Proof Explorer


Theorem sumss

Description: Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014)

Ref Expression
Hypotheses sumss.1 φ A B
sumss.2 φ k A C
sumss.3 φ k B A C = 0
sumss.4 φ B M
Assertion sumss φ k A C = k B C

Proof

Step Hyp Ref Expression
1 sumss.1 φ A B
2 sumss.2 φ k A C
3 sumss.3 φ k B A C = 0
4 sumss.4 φ B M
5 eqid M = M
6 simpr φ M M
7 1 4 sstrd φ A M
8 7 adantr φ M A M
9 nfcv _ k m
10 nffvmpt1 _ k k M if k A C 0 m
11 nfv k m A
12 nffvmpt1 _ k k A C m
13 nfcv _ k 0
14 11 12 13 nfif _ k if m A k A C m 0
15 10 14 nfeq k k M if k A C 0 m = if m A k A C m 0
16 fveq2 k = m k M if k A C 0 k = k M if k A C 0 m
17 eleq1w k = m k A m A
18 fveq2 k = m k A C k = k A C m
19 17 18 ifbieq1d k = m if k A k A C k 0 = if m A k A C m 0
20 16 19 eqeq12d k = m k M if k A C 0 k = if k A k A C k 0 k M if k A C 0 m = if m A k A C m 0
21 eqid k M if k A C 0 = k M if k A C 0
22 21 fvmpt2i k M k M if k A C 0 k = I if k A C 0
23 iftrue k A if k A C 0 = C
24 23 fveq2d k A I if k A C 0 = I C
25 22 24 sylan9eq k M k A k M if k A C 0 k = I C
26 iftrue k A if k A k A C k 0 = k A C k
27 eqid k A C = k A C
28 27 fvmpt2i k A k A C k = I C
29 26 28 eqtrd k A if k A k A C k 0 = I C
30 29 adantl k M k A if k A k A C k 0 = I C
31 25 30 eqtr4d k M k A k M if k A C 0 k = if k A k A C k 0
32 iffalse ¬ k A if k A C 0 = 0
33 32 fveq2d ¬ k A I if k A C 0 = I 0
34 0z 0
35 fvi 0 I 0 = 0
36 34 35 ax-mp I 0 = 0
37 33 36 syl6eq ¬ k A I if k A C 0 = 0
38 22 37 sylan9eq k M ¬ k A k M if k A C 0 k = 0
39 iffalse ¬ k A if k A k A C k 0 = 0
40 39 adantl k M ¬ k A if k A k A C k 0 = 0
41 38 40 eqtr4d k M ¬ k A k M if k A C 0 k = if k A k A C k 0
42 31 41 pm2.61dan k M k M if k A C 0 k = if k A k A C k 0
43 9 15 20 42 vtoclgaf m M k M if k A C 0 m = if m A k A C m 0
44 43 adantl φ M m M k M if k A C 0 m = if m A k A C m 0
45 2 fmpttd φ k A C : A
46 45 adantr φ M k A C : A
47 46 ffvelrnda φ M m A k A C m
48 5 6 8 44 47 zsum φ M m A k A C m = seq M + k M if k A C 0
49 4 adantr φ M B M
50 nfv k φ
51 nfv k m B
52 nffvmpt1 _ k k B C m
53 51 52 13 nfif _ k if m B k B C m 0
54 10 53 nfeq k k M if k A C 0 m = if m B k B C m 0
55 50 54 nfim k φ k M if k A C 0 m = if m B k B C m 0
56 eleq1w k = m k B m B
57 fveq2 k = m k B C k = k B C m
58 56 57 ifbieq1d k = m if k B k B C k 0 = if m B k B C m 0
59 16 58 eqeq12d k = m k M if k A C 0 k = if k B k B C k 0 k M if k A C 0 m = if m B k B C m 0
60 59 imbi2d k = m φ k M if k A C 0 k = if k B k B C k 0 φ k M if k A C 0 m = if m B k B C m 0
61 25 adantll φ k M k A k M if k A C 0 k = I C
62 1 adantr φ k M A B
63 62 sselda φ k M k A k B
64 iftrue k B if k B k B C k 0 = k B C k
65 eqid k B C = k B C
66 65 fvmpt2i k B k B C k = I C
67 64 66 eqtrd k B if k B k B C k 0 = I C
68 63 67 syl φ k M k A if k B k B C k 0 = I C
69 61 68 eqtr4d φ k M k A k M if k A C 0 k = if k B k B C k 0
70 38 adantll φ k M ¬ k A k M if k A C 0 k = 0
71 67 ad2antrl φ k B ¬ k A if k B k B C k 0 = I C
72 eldif k B A k B ¬ k A
73 3 fveq2d φ k B A I C = I 0
74 0cn 0
75 fvi 0 I 0 = 0
76 74 75 ax-mp I 0 = 0
77 73 76 syl6eq φ k B A I C = 0
78 72 77 sylan2br φ k B ¬ k A I C = 0
79 71 78 eqtrd φ k B ¬ k A if k B k B C k 0 = 0
80 79 expr φ k B ¬ k A if k B k B C k 0 = 0
81 iffalse ¬ k B if k B k B C k 0 = 0
82 81 adantl φ ¬ k B if k B k B C k 0 = 0
83 82 a1d φ ¬ k B ¬ k A if k B k B C k 0 = 0
84 80 83 pm2.61dan φ ¬ k A if k B k B C k 0 = 0
85 84 adantr φ k M ¬ k A if k B k B C k 0 = 0
86 85 imp φ k M ¬ k A if k B k B C k 0 = 0
87 70 86 eqtr4d φ k M ¬ k A k M if k A C 0 k = if k B k B C k 0
88 69 87 pm2.61dan φ k M k M if k A C 0 k = if k B k B C k 0
89 88 expcom k M φ k M if k A C 0 k = if k B k B C k 0
90 9 55 60 89 vtoclgaf m M φ k M if k A C 0 m = if m B k B C m 0
91 90 impcom φ m M k M if k A C 0 m = if m B k B C m 0
92 91 adantlr φ M m M k M if k A C 0 m = if m B k B C m 0
93 2 ex φ k A C
94 93 adantr φ k B k A C
95 3 74 eqeltrdi φ k B A C
96 72 95 sylan2br φ k B ¬ k A C
97 96 expr φ k B ¬ k A C
98 94 97 pm2.61d φ k B C
99 98 fmpttd φ k B C : B
100 99 adantr φ M k B C : B
101 100 ffvelrnda φ M m B k B C m
102 5 6 49 92 101 zsum φ M m B k B C m = seq M + k M if k A C 0
103 48 102 eqtr4d φ M m A k A C m = m B k B C m
104 sumfc m A k A C m = k A C
105 sumfc m B k B C m = k B C
106 103 104 105 3eqtr3g φ M k A C = k B C
107 1 adantr φ ¬ M A B
108 uzf : 𝒫
109 108 fdmi dom =
110 109 eleq2i M dom M
111 ndmfv ¬ M dom M =
112 110 111 sylnbir ¬ M M =
113 112 sseq2d ¬ M B M B
114 4 113 syl5ib ¬ M φ B
115 114 impcom φ ¬ M B
116 107 115 sstrd φ ¬ M A
117 ss0 A A =
118 116 117 syl φ ¬ M A =
119 ss0 B B =
120 115 119 syl φ ¬ M B =
121 118 120 eqtr4d φ ¬ M A = B
122 121 sumeq1d φ ¬ M k A C = k B C
123 106 122 pm2.61dan φ k A C = k B C