Metamath Proof Explorer


Theorem fsumcllem

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 NM, 9-Nov-2005) (Revised 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
fsumcllem.5 φ 0 S
Assertion fsumcllem φ 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 fsumcllem.5 φ 0 S
6 simpr φ A = A =
7 6 sumeq1d φ A = k A B = k B
8 sum0 k B = 0
9 7 8 eqtrdi φ A = k A B = 0
10 5 adantr φ A = 0 S
11 9 10 eqeltrd φ A = k A B S
12 1 adantr φ A S
13 2 adantlr φ A x S y S x + y S
14 3 adantr φ A A Fin
15 4 adantlr φ A k A B S
16 simpr φ A A
17 12 13 14 15 16 fsumcl2lem φ A k A B S
18 11 17 pm2.61dane φ k A B S