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 φ S
fsumcllem.2 φ x S y S x + y S
fsumcllem.3 φ A Fin
fsumcllem.4 φ k A B S
fsumcl2lem.5 φ A
Assertion fsumcl2lem φ k A B S

Proof

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