Metamath Proof Explorer

Theorem fsumcl2lem

Description: - Lemma for finite sum closures. (The "-" before "Lemma" forces the math content to be displayed in the Statement List - NM 11-Feb-2008.) (Contributed by Mario Carneiro, 3-Jun-2014)

Ref Expression
Hypotheses fsumcllem.1 
|- ( ph -> S C_ CC )
fsumcllem.2 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
fsumcllem.3 
|- ( ph -> A e. Fin )
fsumcllem.4 
|- ( ( ph /\ k e. A ) -> B e. S )
fsumcl2lem.5 
|- ( ph -> A =/= (/) )
Assertion fsumcl2lem 
|- ( ph -> sum_ k e. A B e. S )

Proof

Step Hyp Ref Expression
1 fsumcllem.1 
 |-  ( ph -> S C_ CC )
2 fsumcllem.2 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
3 fsumcllem.3 
 |-  ( ph -> A e. Fin )
4 fsumcllem.4 
 |-  ( ( ph /\ k e. A ) -> B e. S )
5 fsumcl2lem.5 
 |-  ( ph -> A =/= (/) )
6 5 a1d 
 |-  ( ph -> ( -. sum_ k e. A B e. S -> A =/= (/) ) )
7 6 necon4bd 
 |-  ( ph -> ( A = (/) -> sum_ k e. A B e. S ) )
8 sumfc 
 |-  sum_ m e. A ( ( k e. A |-> B ) ` m ) = sum_ k e. A B
9 fveq2 
 |-  ( m = ( f ` x ) -> ( ( k e. A |-> B ) ` m ) = ( ( k e. A |-> B ) ` ( f ` x ) ) )
10 simprl 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. NN )
11 simprr 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
12 1 ad2antrr 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. A ) -> S C_ CC )
13 4 fmpttd 
 |-  ( ph -> ( k e. A |-> B ) : A --> S )
14 13 adantr 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( k e. A |-> B ) : A --> S )
15 14 ffvelrnda 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. A ) -> ( ( k e. A |-> B ) ` m ) e. S )
16 12 15 sseldd 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. A ) -> ( ( k e. A |-> B ) ` m ) e. CC )
17 f1of 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) --> A )
18 11 17 syl 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) --> A )
19 fvco3 
 |-  ( ( f : ( 1 ... ( # ` A ) ) --> A /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` x ) = ( ( k e. A |-> B ) ` ( f ` x ) ) )
20 18 19 sylan 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` x ) = ( ( k e. A |-> B ) ` ( f ` x ) ) )
21 9 10 11 16 20 fsum 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> sum_ m e. A ( ( k e. A |-> B ) ` m ) = ( seq 1 ( + , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) )
22 8 21 eqtr3id 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> sum_ k e. A B = ( seq 1 ( + , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) )
23 nnuz 
 |-  NN = ( ZZ>= ` 1 )
24 10 23 eleqtrdi 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. ( ZZ>= ` 1 ) )
25 fco 
 |-  ( ( ( k e. A |-> B ) : A --> S /\ f : ( 1 ... ( # ` A ) ) --> A ) -> ( ( k e. A |-> B ) o. f ) : ( 1 ... ( # ` A ) ) --> S )
26 14 18 25 syl2anc 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> B ) o. f ) : ( 1 ... ( # ` A ) ) --> S )
27 26 ffvelrnda 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` x ) e. S )
28 2 adantlr 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
29 24 27 28 seqcl 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( seq 1 ( + , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) e. S )
30 22 29 eqeltrd 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> sum_ k e. A B e. S )
31 30 expr 
 |-  ( ( ph /\ ( # ` A ) e. NN ) -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> sum_ k e. A B e. S ) )
32 31 exlimdv 
 |-  ( ( ph /\ ( # ` A ) e. NN ) -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> sum_ k e. A B e. S ) )
33 32 expimpd 
 |-  ( ph -> ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> sum_ k e. A B e. S ) )
34 fz1f1o 
 |-  ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
35 3 34 syl 
 |-  ( ph -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
36 7 33 35 mpjaod 
 |-  ( ph -> sum_ k e. A B e. S )