Metamath Proof Explorer


Theorem fsumconst

Description: The sum of constant terms ( k is not free in B ). (Contributed by NM, 24-Dec-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Assertion fsumconst A Fin B k A B = A B

Proof

Step Hyp Ref Expression
1 mul02 B 0 B = 0
2 1 adantl A Fin B 0 B = 0
3 2 eqcomd A Fin B 0 = 0 B
4 sumeq1 A = k A B = k B
5 sum0 k B = 0
6 4 5 eqtrdi A = k A B = 0
7 fveq2 A = A =
8 hash0 = 0
9 7 8 eqtrdi A = A = 0
10 9 oveq1d A = A B = 0 B
11 6 10 eqeq12d A = k A B = A B 0 = 0 B
12 3 11 syl5ibrcom A Fin B A = k A B = A B
13 eqidd k = f n B = B
14 simprl A Fin B A f : 1 A 1-1 onto A A
15 simprr A Fin B A f : 1 A 1-1 onto A f : 1 A 1-1 onto A
16 simpllr A Fin B A f : 1 A 1-1 onto A k A B
17 simplr A Fin B A f : 1 A 1-1 onto A B
18 elfznn n 1 A n
19 fvconst2g B n × B n = B
20 17 18 19 syl2an A Fin B A f : 1 A 1-1 onto A n 1 A × B n = B
21 13 14 15 16 20 fsum A Fin B A f : 1 A 1-1 onto A k A B = seq 1 + × B A
22 ser1const B A seq 1 + × B A = A B
23 22 ad2ant2lr A Fin B A f : 1 A 1-1 onto A seq 1 + × B A = A B
24 21 23 eqtrd A Fin B A f : 1 A 1-1 onto A k A B = A B
25 24 expr A Fin B A f : 1 A 1-1 onto A k A B = A B
26 25 exlimdv A Fin B A f f : 1 A 1-1 onto A k A B = A B
27 26 expimpd A Fin B A f f : 1 A 1-1 onto A k A B = A B
28 fz1f1o A Fin A = A f f : 1 A 1-1 onto A
29 28 adantr A Fin B A = A f f : 1 A 1-1 onto A
30 12 27 29 mpjaod A Fin B k A B = A B