Metamath Proof Explorer

Theorem sumsnf

Description: A sum of a singleton is the term. A version of sumsn using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

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