Metamath Proof Explorer

Theorem sumeq2ii

Description: Equality theorem for sum, with the class expressions B and C guarded by _I to be always sets. (Contributed by Mario Carneiro, 13-Jun-2019)

Ref Expression
Assertion sumeq2ii 
|- ( A. k e. A ( _I ` B ) = ( _I ` C ) -> sum_ k e. A B = sum_ k e. A C )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. ZZ ) -> m e. ZZ )
2 simpr 
 |-  ( ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. ZZ ) /\ x e. ( ZZ>= ` m ) ) /\ n e. A ) -> n e. A )
3 simplll 
 |-  ( ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. ZZ ) /\ x e. ( ZZ>= ` m ) ) /\ n e. A ) -> A. k e. A ( _I ` B ) = ( _I ` C ) )
4 nfcv 
 |-  F/_ k _I
5 nfcsb1v 
 |-  F/_ k [_ n / k ]_ B
6 4 5 nffv 
 |-  F/_ k ( _I ` [_ n / k ]_ B )
7 nfcsb1v 
 |-  F/_ k [_ n / k ]_ C
8 4 7 nffv 
 |-  F/_ k ( _I ` [_ n / k ]_ C )
9 6 8 nfeq 
 |-  F/ k ( _I ` [_ n / k ]_ B ) = ( _I ` [_ n / k ]_ C )
10 csbeq1a 
 |-  ( k = n -> B = [_ n / k ]_ B )
11 10 fveq2d 
 |-  ( k = n -> ( _I ` B ) = ( _I ` [_ n / k ]_ B ) )
12 csbeq1a 
 |-  ( k = n -> C = [_ n / k ]_ C )
13 12 fveq2d 
 |-  ( k = n -> ( _I ` C ) = ( _I ` [_ n / k ]_ C ) )
14 11 13 eqeq12d 
 |-  ( k = n -> ( ( _I ` B ) = ( _I ` C ) <-> ( _I ` [_ n / k ]_ B ) = ( _I ` [_ n / k ]_ C ) ) )
15 9 14 rspc 
 |-  ( n e. A -> ( A. k e. A ( _I ` B ) = ( _I ` C ) -> ( _I ` [_ n / k ]_ B ) = ( _I ` [_ n / k ]_ C ) ) )
16 2 3 15 sylc 
 |-  ( ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. ZZ ) /\ x e. ( ZZ>= ` m ) ) /\ n e. A ) -> ( _I ` [_ n / k ]_ B ) = ( _I ` [_ n / k ]_ C ) )
17 16 ifeq1da 
 |-  ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. ZZ ) /\ x e. ( ZZ>= ` m ) ) -> if ( n e. A , ( _I ` [_ n / k ]_ B ) , ( _I ` 0 ) ) = if ( n e. A , ( _I ` [_ n / k ]_ C ) , ( _I ` 0 ) ) )
18 fvif 
 |-  ( _I ` if ( n e. A , [_ n / k ]_ B , 0 ) ) = if ( n e. A , ( _I ` [_ n / k ]_ B ) , ( _I ` 0 ) )
19 fvif 
 |-  ( _I ` if ( n e. A , [_ n / k ]_ C , 0 ) ) = if ( n e. A , ( _I ` [_ n / k ]_ C ) , ( _I ` 0 ) )
20 17 18 19 3eqtr4g 
 |-  ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. ZZ ) /\ x e. ( ZZ>= ` m ) ) -> ( _I ` if ( n e. A , [_ n / k ]_ B , 0 ) ) = ( _I ` if ( n e. A , [_ n / k ]_ C , 0 ) ) )
21 20 mpteq2dv 
 |-  ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. ZZ ) /\ x e. ( ZZ>= ` m ) ) -> ( n e. ZZ |-> ( _I ` if ( n e. A , [_ n / k ]_ B , 0 ) ) ) = ( n e. ZZ |-> ( _I ` if ( n e. A , [_ n / k ]_ C , 0 ) ) ) )
22 21 fveq1d 
 |-  ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. ZZ ) /\ x e. ( ZZ>= ` m ) ) -> ( ( n e. ZZ |-> ( _I ` if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ` x ) = ( ( n e. ZZ |-> ( _I ` if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ` x ) )
23 eqid 
 |-  ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) )
24 eqid 
 |-  ( n e. ZZ |-> ( _I ` if ( n e. A , [_ n / k ]_ B , 0 ) ) ) = ( n e. ZZ |-> ( _I ` if ( n e. A , [_ n / k ]_ B , 0 ) ) )
25 23 24 fvmptex 
 |-  ( ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ` x ) = ( ( n e. ZZ |-> ( _I ` if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ` x )
26 eqid 
 |-  ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) )
27 eqid 
 |-  ( n e. ZZ |-> ( _I ` if ( n e. A , [_ n / k ]_ C , 0 ) ) ) = ( n e. ZZ |-> ( _I ` if ( n e. A , [_ n / k ]_ C , 0 ) ) )
28 26 27 fvmptex 
 |-  ( ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ` x ) = ( ( n e. ZZ |-> ( _I ` if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ` x )
29 22 25 28 3eqtr4g 
 |-  ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. ZZ ) /\ x e. ( ZZ>= ` m ) ) -> ( ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ` x ) = ( ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ` x ) )
30 1 29 seqfeq 
 |-  ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. ZZ ) -> seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) = seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) )
31 30 breq1d 
 |-  ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. ZZ ) -> ( seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x <-> seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) )
32 31 anbi2d 
 |-  ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. ZZ ) -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) <-> ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) ) )
33 32 rexbidva 
 |-  ( A. k e. A ( _I ` B ) = ( _I ` C ) -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) <-> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) ) )
34 simplr 
 |-  ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> m e. NN )
35 nnuz 
 |-  NN = ( ZZ>= ` 1 )
36 34 35 eleqtrdi 
 |-  ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> m e. ( ZZ>= ` 1 ) )
37 f1of 
 |-  ( f : ( 1 ... m ) -1-1-onto-> A -> f : ( 1 ... m ) --> A )
38 37 ad2antlr 
 |-  ( ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ x e. ( 1 ... m ) ) -> f : ( 1 ... m ) --> A )
39 ffvelrn 
 |-  ( ( f : ( 1 ... m ) --> A /\ x e. ( 1 ... m ) ) -> ( f ` x ) e. A )
40 38 39 sylancom 
 |-  ( ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ x e. ( 1 ... m ) ) -> ( f ` x ) e. A )
41 simplll 
 |-  ( ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ x e. ( 1 ... m ) ) -> A. k e. A ( _I ` B ) = ( _I ` C ) )
42 nfcsb1v 
 |-  F/_ k [_ ( f ` x ) / k ]_ ( _I ` B )
43 nfcsb1v 
 |-  F/_ k [_ ( f ` x ) / k ]_ ( _I ` C )
44 42 43 nfeq 
 |-  F/ k [_ ( f ` x ) / k ]_ ( _I ` B ) = [_ ( f ` x ) / k ]_ ( _I ` C )
45 csbeq1a 
 |-  ( k = ( f ` x ) -> ( _I ` B ) = [_ ( f ` x ) / k ]_ ( _I ` B ) )
46 csbeq1a 
 |-  ( k = ( f ` x ) -> ( _I ` C ) = [_ ( f ` x ) / k ]_ ( _I ` C ) )
47 45 46 eqeq12d 
 |-  ( k = ( f ` x ) -> ( ( _I ` B ) = ( _I ` C ) <-> [_ ( f ` x ) / k ]_ ( _I ` B ) = [_ ( f ` x ) / k ]_ ( _I ` C ) ) )
48 44 47 rspc 
 |-  ( ( f ` x ) e. A -> ( A. k e. A ( _I ` B ) = ( _I ` C ) -> [_ ( f ` x ) / k ]_ ( _I ` B ) = [_ ( f ` x ) / k ]_ ( _I ` C ) ) )
49 40 41 48 sylc 
 |-  ( ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ x e. ( 1 ... m ) ) -> [_ ( f ` x ) / k ]_ ( _I ` B ) = [_ ( f ` x ) / k ]_ ( _I ` C ) )
50 fvex 
 |-  ( f ` x ) e. _V
51 csbfv2g 
 |-  ( ( f ` x ) e. _V -> [_ ( f ` x ) / k ]_ ( _I ` B ) = ( _I ` [_ ( f ` x ) / k ]_ B ) )
52 50 51 ax-mp 
 |-  [_ ( f ` x ) / k ]_ ( _I ` B ) = ( _I ` [_ ( f ` x ) / k ]_ B )
53 csbfv2g 
 |-  ( ( f ` x ) e. _V -> [_ ( f ` x ) / k ]_ ( _I ` C ) = ( _I ` [_ ( f ` x ) / k ]_ C ) )
54 50 53 ax-mp 
 |-  [_ ( f ` x ) / k ]_ ( _I ` C ) = ( _I ` [_ ( f ` x ) / k ]_ C )
55 49 52 54 3eqtr3g 
 |-  ( ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ x e. ( 1 ... m ) ) -> ( _I ` [_ ( f ` x ) / k ]_ B ) = ( _I ` [_ ( f ` x ) / k ]_ C ) )
56 elfznn 
 |-  ( x e. ( 1 ... m ) -> x e. NN )
57 56 adantl 
 |-  ( ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ x e. ( 1 ... m ) ) -> x e. NN )
58 fveq2 
 |-  ( n = x -> ( f ` n ) = ( f ` x ) )
59 58 csbeq1d 
 |-  ( n = x -> [_ ( f ` n ) / k ]_ B = [_ ( f ` x ) / k ]_ B )
60 eqid 
 |-  ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( n e. NN |-> [_ ( f ` n ) / k ]_ B )
61 59 60 fvmpti 
 |-  ( x e. NN -> ( ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ` x ) = ( _I ` [_ ( f ` x ) / k ]_ B ) )
62 57 61 syl 
 |-  ( ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ x e. ( 1 ... m ) ) -> ( ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ` x ) = ( _I ` [_ ( f ` x ) / k ]_ B ) )
63 58 csbeq1d 
 |-  ( n = x -> [_ ( f ` n ) / k ]_ C = [_ ( f ` x ) / k ]_ C )
64 eqid 
 |-  ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) = ( n e. NN |-> [_ ( f ` n ) / k ]_ C )
65 63 64 fvmpti 
 |-  ( x e. NN -> ( ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ` x ) = ( _I ` [_ ( f ` x ) / k ]_ C ) )
66 57 65 syl 
 |-  ( ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ x e. ( 1 ... m ) ) -> ( ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ` x ) = ( _I ` [_ ( f ` x ) / k ]_ C ) )
67 55 62 66 3eqtr4d 
 |-  ( ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ x e. ( 1 ... m ) ) -> ( ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ` x ) = ( ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ` x ) )
68 36 67 seqfveq 
 |-  ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) )
69 68 eqeq2d 
 |-  ( ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) <-> x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) )
70 69 pm5.32da 
 |-  ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. NN ) -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )
71 70 exbidv 
 |-  ( ( A. k e. A ( _I ` B ) = ( _I ` C ) /\ m e. NN ) -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )
72 71 rexbidva 
 |-  ( A. k e. A ( _I ` B ) = ( _I ` C ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )
73 33 72 orbi12d 
 |-  ( A. k e. A ( _I ` B ) = ( _I ` C ) -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) <-> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) ) )
74 73 iotabidv 
 |-  ( A. k e. A ( _I ` B ) = ( _I ` C ) -> ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) ) )
75 df-sum 
 |-  sum_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
76 df-sum 
 |-  sum_ k e. A C = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )
77 74 75 76 3eqtr4g 
 |-  ( A. k e. A ( _I ` B ) = ( _I ` C ) -> sum_ k e. A B = sum_ k e. A C )