Metamath Proof Explorer

Theorem fsum

Description: The value of a sum over a nonempty finite set. (Contributed by Mario Carneiro, 20-Apr-2014) (Revised by Mario Carneiro, 13-Jun-2019)

Ref Expression
Hypotheses fsum.1 
|- ( k = ( F ` n ) -> B = C )
fsum.2 
|- ( ph -> M e. NN )
fsum.3 
|- ( ph -> F : ( 1 ... M ) -1-1-onto-> A )
fsum.4 
|- ( ( ph /\ k e. A ) -> B e. CC )
fsum.5 
|- ( ( ph /\ n e. ( 1 ... M ) ) -> ( G ` n ) = C )
Assertion fsum 
|- ( ph -> sum_ k e. A B = ( seq 1 ( + , G ) ` M ) )

Proof

Step Hyp Ref Expression
1 fsum.1 
 |-  ( k = ( F ` n ) -> B = C )
2 fsum.2 
 |-  ( ph -> M e. NN )
3 fsum.3 
 |-  ( ph -> F : ( 1 ... M ) -1-1-onto-> A )
4 fsum.4 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
5 fsum.5 
 |-  ( ( ph /\ n e. ( 1 ... M ) ) -> ( G ` n ) = C )
6 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 ) ) ) )
7 fvex 
 |-  ( seq 1 ( + , G ) ` M ) e. _V
8 eleq1w 
 |-  ( n = j -> ( n e. A <-> j e. A ) )
9 csbeq1 
 |-  ( n = j -> [_ n / k ]_ B = [_ j / k ]_ B )
10 8 9 ifbieq1d 
 |-  ( n = j -> if ( n e. A , [_ n / k ]_ B , 0 ) = if ( j e. A , [_ j / k ]_ B , 0 ) )
11 10 cbvmptv 
 |-  ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) = ( j e. ZZ |-> if ( j e. A , [_ j / k ]_ B , 0 ) )
12 4 ralrimiva 
 |-  ( ph -> A. k e. A B e. CC )
13 nfcsb1v 
 |-  F/_ k [_ j / k ]_ B
14 13 nfel1 
 |-  F/ k [_ j / k ]_ B e. CC
15 csbeq1a 
 |-  ( k = j -> B = [_ j / k ]_ B )
16 15 eleq1d 
 |-  ( k = j -> ( B e. CC <-> [_ j / k ]_ B e. CC ) )
17 14 16 rspc 
 |-  ( j e. A -> ( A. k e. A B e. CC -> [_ j / k ]_ B e. CC ) )
18 12 17 mpan9 
 |-  ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC )
19 fveq2 
 |-  ( n = i -> ( f ` n ) = ( f ` i ) )
20 19 csbeq1d 
 |-  ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / k ]_ B )
21 csbcow 
 |-  [_ ( f ` i ) / j ]_ [_ j / k ]_ B = [_ ( f ` i ) / k ]_ B
22 20 21 eqtr4di 
 |-  ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / j ]_ [_ j / k ]_ B )
23 22 cbvmptv 
 |-  ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( i e. NN |-> [_ ( f ` i ) / j ]_ [_ j / k ]_ B )
24 11 18 23 summo 
 |-  ( ph -> E* 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 ) ) ) )
25 f1of 
 |-  ( F : ( 1 ... M ) -1-1-onto-> A -> F : ( 1 ... M ) --> A )
26 3 25 syl 
 |-  ( ph -> F : ( 1 ... M ) --> A )
27 ovex 
 |-  ( 1 ... M ) e. _V
28 fex 
 |-  ( ( F : ( 1 ... M ) --> A /\ ( 1 ... M ) e. _V ) -> F e. _V )
29 26 27 28 sylancl 
 |-  ( ph -> F e. _V )
30 nnuz 
 |-  NN = ( ZZ>= ` 1 )
31 2 30 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
32 elfznn 
 |-  ( n e. ( 1 ... M ) -> n e. NN )
33 fvex 
 |-  ( G ` n ) e. _V
34 5 33 eqeltrrdi 
 |-  ( ( ph /\ n e. ( 1 ... M ) ) -> C e. _V )
35 eqid 
 |-  ( n e. NN |-> C ) = ( n e. NN |-> C )
36 35 fvmpt2 
 |-  ( ( n e. NN /\ C e. _V ) -> ( ( n e. NN |-> C ) ` n ) = C )
37 32 34 36 syl2an2 
 |-  ( ( ph /\ n e. ( 1 ... M ) ) -> ( ( n e. NN |-> C ) ` n ) = C )
38 5 37 eqtr4d 
 |-  ( ( ph /\ n e. ( 1 ... M ) ) -> ( G ` n ) = ( ( n e. NN |-> C ) ` n ) )
39 38 ralrimiva 
 |-  ( ph -> A. n e. ( 1 ... M ) ( G ` n ) = ( ( n e. NN |-> C ) ` n ) )
40 nffvmpt1 
 |-  F/_ n ( ( n e. NN |-> C ) ` k )
41 40 nfeq2 
 |-  F/ n ( G ` k ) = ( ( n e. NN |-> C ) ` k )
42 fveq2 
 |-  ( n = k -> ( G ` n ) = ( G ` k ) )
43 fveq2 
 |-  ( n = k -> ( ( n e. NN |-> C ) ` n ) = ( ( n e. NN |-> C ) ` k ) )
44 42 43 eqeq12d 
 |-  ( n = k -> ( ( G ` n ) = ( ( n e. NN |-> C ) ` n ) <-> ( G ` k ) = ( ( n e. NN |-> C ) ` k ) ) )
45 41 44 rspc 
 |-  ( k e. ( 1 ... M ) -> ( A. n e. ( 1 ... M ) ( G ` n ) = ( ( n e. NN |-> C ) ` n ) -> ( G ` k ) = ( ( n e. NN |-> C ) ` k ) ) )
46 39 45 mpan9 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( G ` k ) = ( ( n e. NN |-> C ) ` k ) )
47 31 46 seqfveq 
 |-  ( ph -> ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> C ) ) ` M ) )
48 3 47 jca 
 |-  ( ph -> ( F : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> C ) ) ` M ) ) )
49 f1oeq1 
 |-  ( f = F -> ( f : ( 1 ... M ) -1-1-onto-> A <-> F : ( 1 ... M ) -1-1-onto-> A ) )
50 fveq1 
 |-  ( f = F -> ( f ` n ) = ( F ` n ) )
51 50 csbeq1d 
 |-  ( f = F -> [_ ( f ` n ) / k ]_ B = [_ ( F ` n ) / k ]_ B )
52 fvex 
 |-  ( F ` n ) e. _V
53 52 1 csbie 
 |-  [_ ( F ` n ) / k ]_ B = C
54 51 53 syl6eq 
 |-  ( f = F -> [_ ( f ` n ) / k ]_ B = C )
55 54 mpteq2dv 
 |-  ( f = F -> ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( n e. NN |-> C ) )
56 55 seqeq3d 
 |-  ( f = F -> seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) = seq 1 ( + , ( n e. NN |-> C ) ) )
57 56 fveq1d 
 |-  ( f = F -> ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) = ( seq 1 ( + , ( n e. NN |-> C ) ) ` M ) )
58 57 eqeq2d 
 |-  ( f = F -> ( ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) <-> ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> C ) ) ` M ) ) )
59 49 58 anbi12d 
 |-  ( f = F -> ( ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) <-> ( F : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> C ) ) ` M ) ) ) )
60 29 48 59 spcedv 
 |-  ( ph -> E. f ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) )
61 oveq2 
 |-  ( m = M -> ( 1 ... m ) = ( 1 ... M ) )
62 61 f1oeq2d 
 |-  ( m = M -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... M ) -1-1-onto-> A ) )
63 fveq2 
 |-  ( m = M -> ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) )
64 63 eqeq2d 
 |-  ( m = M -> ( ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) <-> ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) )
65 62 64 anbi12d 
 |-  ( m = M -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) ) )
66 65 exbidv 
 |-  ( m = M -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> E. f ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) ) )
67 66 rspcev 
 |-  ( ( M e. NN /\ E. f ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) ) -> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
68 2 60 67 syl2anc 
 |-  ( ph -> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
69 68 olcd 
 |-  ( ph -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
70 breq2 
 |-  ( x = ( seq 1 ( + , G ) ` M ) -> ( 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 ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , G ) ` M ) ) )
71 70 anbi2d 
 |-  ( x = ( seq 1 ( + , G ) ` M ) -> ( ( 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 ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , G ) ` M ) ) ) )
72 71 rexbidv 
 |-  ( x = ( seq 1 ( + , G ) ` M ) -> ( 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 ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , G ) ` M ) ) ) )
73 eqeq1 
 |-  ( x = ( seq 1 ( + , G ) ` M ) -> ( x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) <-> ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
74 73 anbi2d 
 |-  ( x = ( seq 1 ( + , G ) ` M ) -> ( ( 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 /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
75 74 exbidv 
 |-  ( x = ( seq 1 ( + , G ) ` M ) -> ( 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 /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
76 75 rexbidv 
 |-  ( x = ( seq 1 ( + , G ) ` M ) -> ( 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 /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
77 72 76 orbi12d 
 |-  ( x = ( seq 1 ( + , G ) ` M ) -> ( ( 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 ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) )
78 77 moi2 
 |-  ( ( ( ( seq 1 ( + , G ) ` M ) e. _V /\ E* 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 ) ) ) ) /\ ( ( 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 ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) ) -> x = ( seq 1 ( + , G ) ` M ) )
79 7 78 mpanl1 
 |-  ( ( E* 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 ) ) ) /\ ( ( 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 ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) ) -> x = ( seq 1 ( + , G ) ` M ) )
80 79 ancom2s 
 |-  ( ( E* 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 ) ) ) /\ ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( 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 ]_ 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 ) ) ) ) ) -> x = ( seq 1 ( + , G ) ` M ) )
81 80 expr 
 |-  ( ( E* 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 ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( + , G ) ` M ) = ( 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 ]_ 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 ) ) ) -> x = ( seq 1 ( + , G ) ` M ) ) )
82 24 69 81 syl2anc 
 |-  ( ph -> ( ( 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 ) ) ) -> x = ( seq 1 ( + , G ) ` M ) ) )
83 69 77 syl5ibrcom 
 |-  ( ph -> ( x = ( seq 1 ( + , G ) ` M ) -> ( 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 ) ) ) ) )
84 82 83 impbid 
 |-  ( ph -> ( ( 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 ) ) ) <-> x = ( seq 1 ( + , G ) ` M ) ) )
85 84 adantr 
 |-  ( ( ph /\ ( seq 1 ( + , G ) ` M ) e. _V ) -> ( ( 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 ) ) ) <-> x = ( seq 1 ( + , G ) ` M ) ) )
86 85 iota5 
 |-  ( ( ph /\ ( seq 1 ( + , G ) ` M ) e. _V ) -> ( 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 ) ) ) ) = ( seq 1 ( + , G ) ` M ) )
87 7 86 mpan2 
 |-  ( ph -> ( 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 ) ) ) ) = ( seq 1 ( + , G ) ` M ) )
88 6 87 syl5eq 
 |-  ( ph -> sum_ k e. A B = ( seq 1 ( + , G ) ` M ) )