Metamath Proof Explorer


Theorem sumeq2sdv

Description: Equality deduction for sum. (Contributed by NM, 3-Jan-2006) (Proof shortened by Glauco Siliprandi, 5-Apr-2020) Avoid axioms. (Revised by GG, 14-Aug-2025)

Ref Expression
Hypothesis sumeq2sdv.1 φ B = C
Assertion sumeq2sdv φ k A B = k A C

Proof

Step Hyp Ref Expression
1 sumeq2sdv.1 φ B = C
2 1 csbeq2dv φ n / k B = n / k C
3 2 ifeq1d φ if n A n / k B 0 = if n A n / k C 0
4 3 mpteq2dv φ n if n A n / k B 0 = n if n A n / k C 0
5 4 seqeq3d φ seq m + n if n A n / k B 0 = seq m + n if n A n / k C 0
6 5 breq1d φ seq m + n if n A n / k B 0 x seq m + n if n A n / k C 0 x
7 6 anbi2d φ A m seq m + n if n A n / k B 0 x A m seq m + n if n A n / k C 0 x
8 7 rexbidv φ m A m seq m + n if n A n / k B 0 x m A m seq m + n if n A n / k C 0 x
9 1 csbeq2dv φ f n / k B = f n / k C
10 9 mpteq2dv φ n f n / k B = n f n / k C
11 10 seqeq3d φ seq 1 + n f n / k B = seq 1 + n f n / k C
12 11 fveq1d φ seq 1 + n f n / k B m = seq 1 + n f n / k C m
13 12 eqeq2d φ x = seq 1 + n f n / k B m x = seq 1 + n f n / k C m
14 13 anbi2d φ f : 1 m 1-1 onto A x = seq 1 + n f n / k B m f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
15 14 exbidv φ f f : 1 m 1-1 onto A x = seq 1 + n f n / k B m f f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
16 15 rexbidv φ m f f : 1 m 1-1 onto A x = seq 1 + n f n / k B m m f f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
17 8 16 orbi12d φ m A m seq m + n if n A n / k B 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / k B m m A m seq m + n if n A n / k C 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
18 17 iotabidv φ ι x | m A m seq m + n if n A n / k B 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / k B m = ι x | m A m seq m + n if n A n / k C 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
19 df-sum k A B = ι x | m A m seq m + n if n A n / k B 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / k B m
20 df-sum k A C = ι x | m A m seq m + n if n A n / k C 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
21 18 19 20 3eqtr4g φ k A B = k A C