Step |
Hyp |
Ref |
Expression |
1 |
|
cbvsum.1 |
|- ( j = k -> B = C ) |
2 |
1
|
cbvcsbv |
|- [_ n / j ]_ B = [_ n / k ]_ C |
3 |
2
|
a1i |
|- ( T. -> [_ n / j ]_ B = [_ n / k ]_ C ) |
4 |
3
|
ifeq1d |
|- ( T. -> if ( n e. A , [_ n / j ]_ B , 0 ) = if ( n e. A , [_ n / k ]_ C , 0 ) ) |
5 |
4
|
mpteq2dv |
|- ( T. -> ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) |
6 |
5
|
seqeq3d |
|- ( T. -> seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) ) = seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ) |
7 |
6
|
breq1d |
|- ( T. -> ( seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) ) ~~> x <-> seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) ) |
8 |
7
|
mptru |
|- ( seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) ) ~~> x <-> seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) |
9 |
8
|
anbi2i |
|- ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) ) ~~> x ) <-> ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) ) |
10 |
9
|
rexbii |
|- ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ 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 ) ) |
11 |
1
|
cbvcsbv |
|- [_ ( f ` n ) / j ]_ B = [_ ( f ` n ) / k ]_ C |
12 |
11
|
mpteq2i |
|- ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) = ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) |
13 |
12
|
a1i |
|- ( T. -> ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) = ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) |
14 |
13
|
seqeq3d |
|- ( T. -> seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) = seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ) |
15 |
14
|
mptru |
|- seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) = seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) |
16 |
15
|
fveq1i |
|- ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) |
17 |
16
|
eqeq2i |
|- ( x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) <-> x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) |
18 |
17
|
anbi2i |
|- ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) |
19 |
18
|
exbii |
|- ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) |
20 |
19
|
rexbii |
|- ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ 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 ) ) ) |
21 |
10 20
|
orbi12i |
|- ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ 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 ) ) ) ) |
22 |
21
|
iotabii |
|- ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ 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 ) ) ) ) |
23 |
|
df-sum |
|- sum_ j e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) ) ) ) |
24 |
|
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 ) ) ) ) |
25 |
22 23 24
|
3eqtr4i |
|- sum_ j e. A B = sum_ k e. A C |