Metamath Proof Explorer


Theorem fsumrelem

Description: Lemma for fsumre , fsumim , and fsumcj . (Contributed by Mario Carneiro, 25-Jul-2014) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Hypotheses fsumre.1 φ A Fin
fsumre.2 φ k A B
fsumrelem.3 F :
fsumrelem.4 x y F x + y = F x + F y
Assertion fsumrelem φ F k A B = k A F B

Proof

Step Hyp Ref Expression
1 fsumre.1 φ A Fin
2 fsumre.2 φ k A B
3 fsumrelem.3 F :
4 fsumrelem.4 x y F x + y = F x + F y
5 0cn 0
6 3 ffvelrni 0 F 0
7 5 6 ax-mp F 0
8 7 addid1i F 0 + 0 = F 0
9 fvoveq1 x = 0 F x + y = F 0 + y
10 fveq2 x = 0 F x = F 0
11 10 oveq1d x = 0 F x + F y = F 0 + F y
12 9 11 eqeq12d x = 0 F x + y = F x + F y F 0 + y = F 0 + F y
13 oveq2 y = 0 0 + y = 0 + 0
14 00id 0 + 0 = 0
15 13 14 eqtrdi y = 0 0 + y = 0
16 15 fveq2d y = 0 F 0 + y = F 0
17 fveq2 y = 0 F y = F 0
18 17 oveq2d y = 0 F 0 + F y = F 0 + F 0
19 16 18 eqeq12d y = 0 F 0 + y = F 0 + F y F 0 = F 0 + F 0
20 12 19 4 vtocl2ga 0 0 F 0 = F 0 + F 0
21 5 5 20 mp2an F 0 = F 0 + F 0
22 8 21 eqtr2i F 0 + F 0 = F 0 + 0
23 7 7 5 addcani F 0 + F 0 = F 0 + 0 F 0 = 0
24 22 23 mpbi F 0 = 0
25 sumeq1 A = k A B = k B
26 sum0 k B = 0
27 25 26 eqtrdi A = k A B = 0
28 27 fveq2d A = F k A B = F 0
29 sumeq1 A = k A F B = k F B
30 sum0 k F B = 0
31 29 30 eqtrdi A = k A F B = 0
32 24 28 31 3eqtr4a A = F k A B = k A F B
33 32 a1i φ A = F k A B = k A F B
34 addcl x y x + y
35 34 adantl φ A f : 1 A 1-1 onto A x y x + y
36 2 fmpttd φ k A B : A
37 36 adantr φ A f : 1 A 1-1 onto A k A B : A
38 simprr φ A f : 1 A 1-1 onto A f : 1 A 1-1 onto A
39 f1of f : 1 A 1-1 onto A f : 1 A A
40 38 39 syl φ A f : 1 A 1-1 onto A f : 1 A A
41 fco k A B : A f : 1 A A k A B f : 1 A
42 37 40 41 syl2anc φ A f : 1 A 1-1 onto A k A B f : 1 A
43 42 ffvelrnda φ A f : 1 A 1-1 onto A x 1 A k A B f x
44 simprl φ A f : 1 A 1-1 onto A A
45 nnuz = 1
46 44 45 eleqtrdi φ A f : 1 A 1-1 onto A A 1
47 4 adantl φ A f : 1 A 1-1 onto A x y F x + y = F x + F y
48 40 ffvelrnda φ A f : 1 A 1-1 onto A x 1 A f x A
49 simpr φ k A k A
50 eqid k A B = k A B
51 50 fvmpt2 k A B k A B k = B
52 49 2 51 syl2anc φ k A k A B k = B
53 52 fveq2d φ k A F k A B k = F B
54 fvex F B V
55 eqid k A F B = k A F B
56 55 fvmpt2 k A F B V k A F B k = F B
57 49 54 56 sylancl φ k A k A F B k = F B
58 53 57 eqtr4d φ k A F k A B k = k A F B k
59 58 ralrimiva φ k A F k A B k = k A F B k
60 59 ad2antrr φ A f : 1 A 1-1 onto A x 1 A k A F k A B k = k A F B k
61 nfcv _ k F
62 nffvmpt1 _ k k A B f x
63 61 62 nffv _ k F k A B f x
64 nffvmpt1 _ k k A F B f x
65 63 64 nfeq k F k A B f x = k A F B f x
66 2fveq3 k = f x F k A B k = F k A B f x
67 fveq2 k = f x k A F B k = k A F B f x
68 66 67 eqeq12d k = f x F k A B k = k A F B k F k A B f x = k A F B f x
69 65 68 rspc f x A k A F k A B k = k A F B k F k A B f x = k A F B f x
70 48 60 69 sylc φ A f : 1 A 1-1 onto A x 1 A F k A B f x = k A F B f x
71 fvco3 f : 1 A A x 1 A k A B f x = k A B f x
72 40 71 sylan φ A f : 1 A 1-1 onto A x 1 A k A B f x = k A B f x
73 72 fveq2d φ A f : 1 A 1-1 onto A x 1 A F k A B f x = F k A B f x
74 fvco3 f : 1 A A x 1 A k A F B f x = k A F B f x
75 40 74 sylan φ A f : 1 A 1-1 onto A x 1 A k A F B f x = k A F B f x
76 70 73 75 3eqtr4d φ A f : 1 A 1-1 onto A x 1 A F k A B f x = k A F B f x
77 35 43 46 47 76 seqhomo φ A f : 1 A 1-1 onto A F seq 1 + k A B f A = seq 1 + k A F B f A
78 fveq2 m = f x k A B m = k A B f x
79 37 ffvelrnda φ A f : 1 A 1-1 onto A m A k A B m
80 78 44 38 79 72 fsum φ A f : 1 A 1-1 onto A m A k A B m = seq 1 + k A B f A
81 80 fveq2d φ A f : 1 A 1-1 onto A F m A k A B m = F seq 1 + k A B f A
82 fveq2 m = f x k A F B m = k A F B f x
83 3 ffvelrni B F B
84 2 83 syl φ k A F B
85 84 fmpttd φ k A F B : A
86 85 adantr φ A f : 1 A 1-1 onto A k A F B : A
87 86 ffvelrnda φ A f : 1 A 1-1 onto A m A k A F B m
88 82 44 38 87 75 fsum φ A f : 1 A 1-1 onto A m A k A F B m = seq 1 + k A F B f A
89 77 81 88 3eqtr4d φ A f : 1 A 1-1 onto A F m A k A B m = m A k A F B m
90 sumfc m A k A B m = k A B
91 90 fveq2i F m A k A B m = F k A B
92 sumfc m A k A F B m = k A F B
93 89 91 92 3eqtr3g φ A f : 1 A 1-1 onto A F k A B = k A F B
94 93 expr φ A f : 1 A 1-1 onto A F k A B = k A F B
95 94 exlimdv φ A f f : 1 A 1-1 onto A F k A B = k A F B
96 95 expimpd φ A f f : 1 A 1-1 onto A F k A B = k A F B
97 fz1f1o A Fin A = A f f : 1 A 1-1 onto A
98 1 97 syl φ A = A f f : 1 A 1-1 onto A
99 33 96 98 mpjaod φ F k A B = k A F B