Metamath Proof Explorer

Theorem sumsnd

Description: A sum of a singleton is the term. The deduction version of sumsn . (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses sumsnd.1 
|- ( ph -> F/_ k B )
sumsnd.2 
|- F/ k ph
sumsnd.3 
|- ( ( ph /\ k = M ) -> A = B )
sumsnd.4 
|- ( ph -> M e. V )
sumsnd.5 
|- ( ph -> B e. CC )
Assertion sumsnd 
|- ( ph -> sum_ k e. { M } A = B )

Proof

Step Hyp Ref Expression
1 sumsnd.1 
 |-  ( ph -> F/_ k B )
2 sumsnd.2 
 |-  F/ k ph
3 sumsnd.3 
 |-  ( ( ph /\ k = M ) -> A = B )
4 sumsnd.4 
 |-  ( ph -> M e. V )
5 sumsnd.5 
 |-  ( ph -> B e. CC )
6 csbeq1a 
 |-  ( k = m -> A = [_ m / k ]_ A )
7 nfcv 
 |-  F/_ m A
8 nfcsb1v 
 |-  F/_ k [_ m / k ]_ A
9 6 7 8 cbvsum 
 |-  sum_ k e. { M } A = sum_ m e. { M } [_ m / k ]_ A
10 csbeq1 
 |-  ( m = ( { <. 1 , M >. } ` n ) -> [_ m / k ]_ A = [_ ( { <. 1 , M >. } ` n ) / k ]_ A )
11 1nn 
 |-  1 e. NN
12 11 a1i 
 |-  ( ph -> 1 e. NN )
13 f1osng 
 |-  ( ( 1 e. NN /\ M e. V ) -> { <. 1 , M >. } : { 1 } -1-1-onto-> { M } )
14 11 4 13 sylancr 
 |-  ( ph -> { <. 1 , M >. } : { 1 } -1-1-onto-> { M } )
15 1z 
 |-  1 e. ZZ
16 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
17 f1oeq2 
 |-  ( ( 1 ... 1 ) = { 1 } -> ( { <. 1 , M >. } : ( 1 ... 1 ) -1-1-onto-> { M } <-> { <. 1 , M >. } : { 1 } -1-1-onto-> { M } ) )
18 15 16 17 mp2b 
 |-  ( { <. 1 , M >. } : ( 1 ... 1 ) -1-1-onto-> { M } <-> { <. 1 , M >. } : { 1 } -1-1-onto-> { M } )
19 14 18 sylibr 
 |-  ( ph -> { <. 1 , M >. } : ( 1 ... 1 ) -1-1-onto-> { M } )
20 elsni 
 |-  ( m e. { M } -> m = M )
21 20 adantl 
 |-  ( ( ph /\ m e. { M } ) -> m = M )
22 21 csbeq1d 
 |-  ( ( ph /\ m e. { M } ) -> [_ m / k ]_ A = [_ M / k ]_ A )
23 2 1 4 3 csbiedf 
 |-  ( ph -> [_ M / k ]_ A = B )
24 23 adantr 
 |-  ( ( ph /\ m e. { M } ) -> [_ M / k ]_ A = B )
25 5 adantr 
 |-  ( ( ph /\ m e. { M } ) -> B e. CC )
26 24 25 eqeltrd 
 |-  ( ( ph /\ m e. { M } ) -> [_ M / k ]_ A e. CC )
27 22 26 eqeltrd 
 |-  ( ( ph /\ m e. { M } ) -> [_ m / k ]_ A e. CC )
28 23 adantr 
 |-  ( ( ph /\ n e. ( 1 ... 1 ) ) -> [_ M / k ]_ A = B )
29 elfz1eq 
 |-  ( n e. ( 1 ... 1 ) -> n = 1 )
30 29 fveq2d 
 |-  ( n e. ( 1 ... 1 ) -> ( { <. 1 , M >. } ` n ) = ( { <. 1 , M >. } ` 1 ) )
31 fvsng 
 |-  ( ( 1 e. NN /\ M e. V ) -> ( { <. 1 , M >. } ` 1 ) = M )
32 11 4 31 sylancr 
 |-  ( ph -> ( { <. 1 , M >. } ` 1 ) = M )
33 30 32 sylan9eqr 
 |-  ( ( ph /\ n e. ( 1 ... 1 ) ) -> ( { <. 1 , M >. } ` n ) = M )
34 33 csbeq1d 
 |-  ( ( ph /\ n e. ( 1 ... 1 ) ) -> [_ ( { <. 1 , M >. } ` n ) / k ]_ A = [_ M / k ]_ A )
35 29 fveq2d 
 |-  ( n e. ( 1 ... 1 ) -> ( { <. 1 , B >. } ` n ) = ( { <. 1 , B >. } ` 1 ) )
36 fvsng 
 |-  ( ( 1 e. NN /\ B e. CC ) -> ( { <. 1 , B >. } ` 1 ) = B )
37 11 5 36 sylancr 
 |-  ( ph -> ( { <. 1 , B >. } ` 1 ) = B )
38 35 37 sylan9eqr 
 |-  ( ( ph /\ n e. ( 1 ... 1 ) ) -> ( { <. 1 , B >. } ` n ) = B )
39 28 34 38 3eqtr4rd 
 |-  ( ( ph /\ n e. ( 1 ... 1 ) ) -> ( { <. 1 , B >. } ` n ) = [_ ( { <. 1 , M >. } ` n ) / k ]_ A )
40 10 12 19 27 39 fsum 
 |-  ( ph -> sum_ m e. { M } [_ m / k ]_ A = ( seq 1 ( + , { <. 1 , B >. } ) ` 1 ) )
41 9 40 eqtrid 
 |-  ( ph -> sum_ k e. { M } A = ( seq 1 ( + , { <. 1 , B >. } ) ` 1 ) )
42 15 37 seq1i 
 |-  ( ph -> ( seq 1 ( + , { <. 1 , B >. } ) ` 1 ) = B )
43 41 42 eqtrd 
 |-  ( ph -> sum_ k e. { M } A = B )