Metamath Proof Explorer


Theorem fsumadd

Description: The sum of two finite sums. (Contributed by NM, 14-Nov-2005) (Revised by Mario Carneiro, 22-Apr-2014)

Ref Expression
Hypotheses fsumadd.1 φAFin
fsumadd.2 φkAB
fsumadd.3 φkAC
Assertion fsumadd φkAB+C=kAB+kAC

Proof

Step Hyp Ref Expression
1 fsumadd.1 φAFin
2 fsumadd.2 φkAB
3 fsumadd.3 φkAC
4 00id 0+0=0
5 sum0 kB=0
6 sum0 kC=0
7 5 6 oveq12i kB+kC=0+0
8 sum0 kB+C=0
9 4 7 8 3eqtr4ri kB+C=kB+kC
10 sumeq1 A=kAB+C=kB+C
11 sumeq1 A=kAB=kB
12 sumeq1 A=kAC=kC
13 11 12 oveq12d A=kAB+kAC=kB+kC
14 9 10 13 3eqtr4a A=kAB+C=kAB+kAC
15 14 a1i φA=kAB+C=kAB+kAC
16 simprl φAf:1A1-1 ontoAA
17 nnuz =1
18 16 17 eleqtrdi φAf:1A1-1 ontoAA1
19 2 adantlr φAf:1A1-1 ontoAkAB
20 19 fmpttd φAf:1A1-1 ontoAkAB:A
21 simprr φAf:1A1-1 ontoAf:1A1-1 ontoA
22 f1of f:1A1-1 ontoAf:1AA
23 21 22 syl φAf:1A1-1 ontoAf:1AA
24 fco kAB:Af:1AAkABf:1A
25 20 23 24 syl2anc φAf:1A1-1 ontoAkABf:1A
26 25 ffvelrnda φAf:1A1-1 ontoAn1AkABfn
27 3 adantlr φAf:1A1-1 ontoAkAC
28 27 fmpttd φAf:1A1-1 ontoAkAC:A
29 fco kAC:Af:1AAkACf:1A
30 28 23 29 syl2anc φAf:1A1-1 ontoAkACf:1A
31 30 ffvelrnda φAf:1A1-1 ontoAn1AkACfn
32 23 ffvelrnda φAf:1A1-1 ontoAn1AfnA
33 ovex B+CV
34 eqid kAB+C=kAB+C
35 34 fvmpt2 kAB+CVkAB+Ck=B+C
36 33 35 mpan2 kAkAB+Ck=B+C
37 36 adantl φkAkAB+Ck=B+C
38 simpr φkAkA
39 eqid kAB=kAB
40 39 fvmpt2 kABkABk=B
41 38 2 40 syl2anc φkAkABk=B
42 eqid kAC=kAC
43 42 fvmpt2 kACkACk=C
44 38 3 43 syl2anc φkAkACk=C
45 41 44 oveq12d φkAkABk+kACk=B+C
46 37 45 eqtr4d φkAkAB+Ck=kABk+kACk
47 46 ralrimiva φkAkAB+Ck=kABk+kACk
48 47 ad2antrr φAf:1A1-1 ontoAn1AkAkAB+Ck=kABk+kACk
49 nffvmpt1 _kkAB+Cfn
50 nffvmpt1 _kkABfn
51 nfcv _k+
52 nffvmpt1 _kkACfn
53 50 51 52 nfov _kkABfn+kACfn
54 49 53 nfeq kkAB+Cfn=kABfn+kACfn
55 fveq2 k=fnkAB+Ck=kAB+Cfn
56 fveq2 k=fnkABk=kABfn
57 fveq2 k=fnkACk=kACfn
58 56 57 oveq12d k=fnkABk+kACk=kABfn+kACfn
59 55 58 eqeq12d k=fnkAB+Ck=kABk+kACkkAB+Cfn=kABfn+kACfn
60 54 59 rspc fnAkAkAB+Ck=kABk+kACkkAB+Cfn=kABfn+kACfn
61 32 48 60 sylc φAf:1A1-1 ontoAn1AkAB+Cfn=kABfn+kACfn
62 fvco3 f:1AAn1AkAB+Cfn=kAB+Cfn
63 23 62 sylan φAf:1A1-1 ontoAn1AkAB+Cfn=kAB+Cfn
64 fvco3 f:1AAn1AkABfn=kABfn
65 23 64 sylan φAf:1A1-1 ontoAn1AkABfn=kABfn
66 fvco3 f:1AAn1AkACfn=kACfn
67 23 66 sylan φAf:1A1-1 ontoAn1AkACfn=kACfn
68 65 67 oveq12d φAf:1A1-1 ontoAn1AkABfn+kACfn=kABfn+kACfn
69 61 63 68 3eqtr4d φAf:1A1-1 ontoAn1AkAB+Cfn=kABfn+kACfn
70 18 26 31 69 seradd φAf:1A1-1 ontoAseq1+kAB+CfA=seq1+kABfA+seq1+kACfA
71 fveq2 m=fnkAB+Cm=kAB+Cfn
72 19 27 addcld φAf:1A1-1 ontoAkAB+C
73 72 fmpttd φAf:1A1-1 ontoAkAB+C:A
74 73 ffvelrnda φAf:1A1-1 ontoAmAkAB+Cm
75 71 16 21 74 63 fsum φAf:1A1-1 ontoAmAkAB+Cm=seq1+kAB+CfA
76 fveq2 m=fnkABm=kABfn
77 20 ffvelrnda φAf:1A1-1 ontoAmAkABm
78 76 16 21 77 65 fsum φAf:1A1-1 ontoAmAkABm=seq1+kABfA
79 fveq2 m=fnkACm=kACfn
80 28 ffvelrnda φAf:1A1-1 ontoAmAkACm
81 79 16 21 80 67 fsum φAf:1A1-1 ontoAmAkACm=seq1+kACfA
82 78 81 oveq12d φAf:1A1-1 ontoAmAkABm+mAkACm=seq1+kABfA+seq1+kACfA
83 70 75 82 3eqtr4d φAf:1A1-1 ontoAmAkAB+Cm=mAkABm+mAkACm
84 sumfc mAkAB+Cm=kAB+C
85 sumfc mAkABm=kAB
86 sumfc mAkACm=kAC
87 85 86 oveq12i mAkABm+mAkACm=kAB+kAC
88 83 84 87 3eqtr3g φAf:1A1-1 ontoAkAB+C=kAB+kAC
89 88 expr φAf:1A1-1 ontoAkAB+C=kAB+kAC
90 89 exlimdv φAff:1A1-1 ontoAkAB+C=kAB+kAC
91 90 expimpd φAff:1A1-1 ontoAkAB+C=kAB+kAC
92 fz1f1o AFinA=Aff:1A1-1 ontoA
93 1 92 syl φA=Aff:1A1-1 ontoA
94 15 91 93 mpjaod φkAB+C=kAB+kAC