Metamath Proof Explorer


Theorem sumeq2w

Description: Equality theorem for sum, when the class expressions B and C are equal everywhere. Proved using only Extensionality. (Contributed by Mario Carneiro, 24-Jun-2014) (Revised by Mario Carneiro, 13-Jun-2019)

Ref Expression
Assertion sumeq2w k B = C k A B = k A C

Proof

Step Hyp Ref Expression
1 csbeq2 k B = C n / k B = n / k C
2 1 ifeq1d k B = C if n A n / k B 0 = if n A n / k C 0
3 2 mpteq2dv k B = C n if n A n / k B 0 = n if n A n / k C 0
4 3 seqeq3d k B = C seq m + n if n A n / k B 0 = seq m + n if n A n / k C 0
5 4 breq1d k B = C seq m + n if n A n / k B 0 x seq m + n if n A n / k C 0 x
6 5 anbi2d k B = C 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
7 6 rexbidv k B = C 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
8 csbeq2 k B = C f n / k B = f n / k C
9 8 mpteq2dv k B = C n f n / k B = n f n / k C
10 9 seqeq3d k B = C seq 1 + n f n / k B = seq 1 + n f n / k C
11 10 fveq1d k B = C seq 1 + n f n / k B m = seq 1 + n f n / k C m
12 11 eqeq2d k B = C x = seq 1 + n f n / k B m x = seq 1 + n f n / k C m
13 12 anbi2d k B = C 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
14 13 exbidv k B = C 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
15 14 rexbidv k B = C 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
16 7 15 orbi12d k B = C 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
17 16 iotabidv k B = C ι 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
18 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
19 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
20 17 18 19 3eqtr4g k B = C k A B = k A C