Step | Hyp | Ref
| Expression |
1 | | 0cn 11208 |
. . . . . . . 8
β’ 0 β
β |
2 | | fsumrelem.3 |
. . . . . . . . 9
β’ πΉ:ββΆβ |
3 | 2 | ffvelcdmi 7085 |
. . . . . . . 8
β’ (0 β
β β (πΉβ0)
β β) |
4 | 1, 3 | ax-mp 5 |
. . . . . . 7
β’ (πΉβ0) β
β |
5 | 4 | addridi 11403 |
. . . . . 6
β’ ((πΉβ0) + 0) = (πΉβ0) |
6 | | fvoveq1 7434 |
. . . . . . . . 9
β’ (π₯ = 0 β (πΉβ(π₯ + π¦)) = (πΉβ(0 + π¦))) |
7 | | fveq2 6891 |
. . . . . . . . . 10
β’ (π₯ = 0 β (πΉβπ₯) = (πΉβ0)) |
8 | 7 | oveq1d 7426 |
. . . . . . . . 9
β’ (π₯ = 0 β ((πΉβπ₯) + (πΉβπ¦)) = ((πΉβ0) + (πΉβπ¦))) |
9 | 6, 8 | eqeq12d 2748 |
. . . . . . . 8
β’ (π₯ = 0 β ((πΉβ(π₯ + π¦)) = ((πΉβπ₯) + (πΉβπ¦)) β (πΉβ(0 + π¦)) = ((πΉβ0) + (πΉβπ¦)))) |
10 | | oveq2 7419 |
. . . . . . . . . . 11
β’ (π¦ = 0 β (0 + π¦) = (0 + 0)) |
11 | | 00id 11391 |
. . . . . . . . . . 11
β’ (0 + 0) =
0 |
12 | 10, 11 | eqtrdi 2788 |
. . . . . . . . . 10
β’ (π¦ = 0 β (0 + π¦) = 0) |
13 | 12 | fveq2d 6895 |
. . . . . . . . 9
β’ (π¦ = 0 β (πΉβ(0 + π¦)) = (πΉβ0)) |
14 | | fveq2 6891 |
. . . . . . . . . 10
β’ (π¦ = 0 β (πΉβπ¦) = (πΉβ0)) |
15 | 14 | oveq2d 7427 |
. . . . . . . . 9
β’ (π¦ = 0 β ((πΉβ0) + (πΉβπ¦)) = ((πΉβ0) + (πΉβ0))) |
16 | 13, 15 | eqeq12d 2748 |
. . . . . . . 8
β’ (π¦ = 0 β ((πΉβ(0 + π¦)) = ((πΉβ0) + (πΉβπ¦)) β (πΉβ0) = ((πΉβ0) + (πΉβ0)))) |
17 | | fsumrelem.4 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β (πΉβ(π₯ + π¦)) = ((πΉβπ₯) + (πΉβπ¦))) |
18 | 9, 16, 17 | vtocl2ga 3566 |
. . . . . . 7
β’ ((0
β β β§ 0 β β) β (πΉβ0) = ((πΉβ0) + (πΉβ0))) |
19 | 1, 1, 18 | mp2an 690 |
. . . . . 6
β’ (πΉβ0) = ((πΉβ0) + (πΉβ0)) |
20 | 5, 19 | eqtr2i 2761 |
. . . . 5
β’ ((πΉβ0) + (πΉβ0)) = ((πΉβ0) + 0) |
21 | 4, 4, 1 | addcani 11409 |
. . . . 5
β’ (((πΉβ0) + (πΉβ0)) = ((πΉβ0) + 0) β (πΉβ0) = 0) |
22 | 20, 21 | mpbi 229 |
. . . 4
β’ (πΉβ0) = 0 |
23 | | sumeq1 15637 |
. . . . . 6
β’ (π΄ = β
β Ξ£π β π΄ π΅ = Ξ£π β β
π΅) |
24 | | sum0 15669 |
. . . . . 6
β’
Ξ£π β
β
π΅ =
0 |
25 | 23, 24 | eqtrdi 2788 |
. . . . 5
β’ (π΄ = β
β Ξ£π β π΄ π΅ = 0) |
26 | 25 | fveq2d 6895 |
. . . 4
β’ (π΄ = β
β (πΉβΞ£π β π΄ π΅) = (πΉβ0)) |
27 | | sumeq1 15637 |
. . . . 5
β’ (π΄ = β
β Ξ£π β π΄ (πΉβπ΅) = Ξ£π β β
(πΉβπ΅)) |
28 | | sum0 15669 |
. . . . 5
β’
Ξ£π β
β
(πΉβπ΅) = 0 |
29 | 27, 28 | eqtrdi 2788 |
. . . 4
β’ (π΄ = β
β Ξ£π β π΄ (πΉβπ΅) = 0) |
30 | 22, 26, 29 | 3eqtr4a 2798 |
. . 3
β’ (π΄ = β
β (πΉβΞ£π β π΄ π΅) = Ξ£π β π΄ (πΉβπ΅)) |
31 | 30 | a1i 11 |
. 2
β’ (π β (π΄ = β
β (πΉβΞ£π β π΄ π΅) = Ξ£π β π΄ (πΉβπ΅))) |
32 | | addcl 11194 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β) β (π₯ + π¦) β β) |
33 | 32 | adantl 482 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ (π₯ β β β§ π¦ β β)) β (π₯ + π¦) β β) |
34 | | fsumre.2 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π΅ β β) |
35 | 34 | fmpttd 7116 |
. . . . . . . . . . 11
β’ (π β (π β π΄ β¦ π΅):π΄βΆβ) |
36 | 35 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ π΅):π΄βΆβ) |
37 | | simprr 771 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))β1-1-ontoβπ΄) |
38 | | f1of 6833 |
. . . . . . . . . . 11
β’ (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β π:(1...(β―βπ΄))βΆπ΄) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))βΆπ΄) |
40 | | fco 6741 |
. . . . . . . . . 10
β’ (((π β π΄ β¦ π΅):π΄βΆβ β§ π:(1...(β―βπ΄))βΆπ΄) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆβ) |
41 | 36, 39, 40 | syl2anc 584 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆβ) |
42 | 41 | ffvelcdmda 7086 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ₯) β β) |
43 | | simprl 769 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
β) |
44 | | nnuz 12867 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
45 | 43, 44 | eleqtrdi 2843 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
(β€β₯β1)) |
46 | 17 | adantl 482 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ (π₯ β β β§ π¦ β β)) β (πΉβ(π₯ + π¦)) = ((πΉβπ₯) + (πΉβπ¦))) |
47 | 39 | ffvelcdmda 7086 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β (πβπ₯) β π΄) |
48 | | simpr 485 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β π β π΄) |
49 | | eqid 2732 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β¦ π΅) = (π β π΄ β¦ π΅) |
50 | 49 | fvmpt2 7009 |
. . . . . . . . . . . . . . 15
β’ ((π β π΄ β§ π΅ β β) β ((π β π΄ β¦ π΅)βπ) = π΅) |
51 | 48, 34, 50 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) = π΅) |
52 | 51 | fveq2d 6895 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β (πΉβ((π β π΄ β¦ π΅)βπ)) = (πΉβπ΅)) |
53 | | fvex 6904 |
. . . . . . . . . . . . . 14
β’ (πΉβπ΅) β V |
54 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β¦ (πΉβπ΅)) = (π β π΄ β¦ (πΉβπ΅)) |
55 | 54 | fvmpt2 7009 |
. . . . . . . . . . . . . 14
β’ ((π β π΄ β§ (πΉβπ΅) β V) β ((π β π΄ β¦ (πΉβπ΅))βπ) = (πΉβπ΅)) |
56 | 48, 53, 55 | sylancl 586 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β ((π β π΄ β¦ (πΉβπ΅))βπ) = (πΉβπ΅)) |
57 | 52, 56 | eqtr4d 2775 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β (πΉβ((π β π΄ β¦ π΅)βπ)) = ((π β π΄ β¦ (πΉβπ΅))βπ)) |
58 | 57 | ralrimiva 3146 |
. . . . . . . . . . 11
β’ (π β βπ β π΄ (πΉβ((π β π΄ β¦ π΅)βπ)) = ((π β π΄ β¦ (πΉβπ΅))βπ)) |
59 | 58 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β βπ β π΄ (πΉβ((π β π΄ β¦ π΅)βπ)) = ((π β π΄ β¦ (πΉβπ΅))βπ)) |
60 | | nfcv 2903 |
. . . . . . . . . . . . 13
β’
β²ππΉ |
61 | | nffvmpt1 6902 |
. . . . . . . . . . . . 13
β’
β²π((π β π΄ β¦ π΅)β(πβπ₯)) |
62 | 60, 61 | nffv 6901 |
. . . . . . . . . . . 12
β’
β²π(πΉβ((π β π΄ β¦ π΅)β(πβπ₯))) |
63 | | nffvmpt1 6902 |
. . . . . . . . . . . 12
β’
β²π((π β π΄ β¦ (πΉβπ΅))β(πβπ₯)) |
64 | 62, 63 | nfeq 2916 |
. . . . . . . . . . 11
β’
β²π(πΉβ((π β π΄ β¦ π΅)β(πβπ₯))) = ((π β π΄ β¦ (πΉβπ΅))β(πβπ₯)) |
65 | | 2fveq3 6896 |
. . . . . . . . . . . 12
β’ (π = (πβπ₯) β (πΉβ((π β π΄ β¦ π΅)βπ)) = (πΉβ((π β π΄ β¦ π΅)β(πβπ₯)))) |
66 | | fveq2 6891 |
. . . . . . . . . . . 12
β’ (π = (πβπ₯) β ((π β π΄ β¦ (πΉβπ΅))βπ) = ((π β π΄ β¦ (πΉβπ΅))β(πβπ₯))) |
67 | 65, 66 | eqeq12d 2748 |
. . . . . . . . . . 11
β’ (π = (πβπ₯) β ((πΉβ((π β π΄ β¦ π΅)βπ)) = ((π β π΄ β¦ (πΉβπ΅))βπ) β (πΉβ((π β π΄ β¦ π΅)β(πβπ₯))) = ((π β π΄ β¦ (πΉβπ΅))β(πβπ₯)))) |
68 | 64, 67 | rspc 3600 |
. . . . . . . . . 10
β’ ((πβπ₯) β π΄ β (βπ β π΄ (πΉβ((π β π΄ β¦ π΅)βπ)) = ((π β π΄ β¦ (πΉβπ΅))βπ) β (πΉβ((π β π΄ β¦ π΅)β(πβπ₯))) = ((π β π΄ β¦ (πΉβπ΅))β(πβπ₯)))) |
69 | 47, 59, 68 | sylc 65 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β (πΉβ((π β π΄ β¦ π΅)β(πβπ₯))) = ((π β π΄ β¦ (πΉβπ΅))β(πβπ₯))) |
70 | | fvco3 6990 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π₯ β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ₯) = ((π β π΄ β¦ π΅)β(πβπ₯))) |
71 | 39, 70 | sylan 580 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ₯) = ((π β π΄ β¦ π΅)β(πβπ₯))) |
72 | 71 | fveq2d 6895 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β (πΉβ(((π β π΄ β¦ π΅) β π)βπ₯)) = (πΉβ((π β π΄ β¦ π΅)β(πβπ₯)))) |
73 | | fvco3 6990 |
. . . . . . . . . 10
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π₯ β (1...(β―βπ΄))) β (((π β π΄ β¦ (πΉβπ΅)) β π)βπ₯) = ((π β π΄ β¦ (πΉβπ΅))β(πβπ₯))) |
74 | 39, 73 | sylan 580 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β (((π β π΄ β¦ (πΉβπ΅)) β π)βπ₯) = ((π β π΄ β¦ (πΉβπ΅))β(πβπ₯))) |
75 | 69, 72, 74 | 3eqtr4d 2782 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β (πΉβ(((π β π΄ β¦ π΅) β π)βπ₯)) = (((π β π΄ β¦ (πΉβπ΅)) β π)βπ₯)) |
76 | 33, 42, 45, 46, 75 | seqhomo 14017 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (πΉβ(seq1( + , ((π β π΄ β¦ π΅) β π))β(β―βπ΄))) = (seq1( + , ((π β π΄ β¦ (πΉβπ΅)) β π))β(β―βπ΄))) |
77 | | fveq2 6891 |
. . . . . . . . 9
β’ (π = (πβπ₯) β ((π β π΄ β¦ π΅)βπ) = ((π β π΄ β¦ π΅)β(πβπ₯))) |
78 | 36 | ffvelcdmda 7086 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) β β) |
79 | 77, 43, 37, 78, 71 | fsum 15668 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) = (seq1( + , ((π β π΄ β¦ π΅) β π))β(β―βπ΄))) |
80 | 79 | fveq2d 6895 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (πΉβΞ£π β π΄ ((π β π΄ β¦ π΅)βπ)) = (πΉβ(seq1( + , ((π β π΄ β¦ π΅) β π))β(β―βπ΄)))) |
81 | | fveq2 6891 |
. . . . . . . 8
β’ (π = (πβπ₯) β ((π β π΄ β¦ (πΉβπ΅))βπ) = ((π β π΄ β¦ (πΉβπ΅))β(πβπ₯))) |
82 | 2 | ffvelcdmi 7085 |
. . . . . . . . . . . 12
β’ (π΅ β β β (πΉβπ΅) β β) |
83 | 34, 82 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β (πΉβπ΅) β β) |
84 | 83 | fmpttd 7116 |
. . . . . . . . . 10
β’ (π β (π β π΄ β¦ (πΉβπ΅)):π΄βΆβ) |
85 | 84 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ (πΉβπ΅)):π΄βΆβ) |
86 | 85 | ffvelcdmda 7086 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ (πΉβπ΅))βπ) β β) |
87 | 81, 43, 37, 86, 74 | fsum 15668 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β Ξ£π β π΄ ((π β π΄ β¦ (πΉβπ΅))βπ) = (seq1( + , ((π β π΄ β¦ (πΉβπ΅)) β π))β(β―βπ΄))) |
88 | 76, 80, 87 | 3eqtr4d 2782 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (πΉβΞ£π β π΄ ((π β π΄ β¦ π΅)βπ)) = Ξ£π β π΄ ((π β π΄ β¦ (πΉβπ΅))βπ)) |
89 | | sumfc 15657 |
. . . . . . 7
β’
Ξ£π β
π΄ ((π β π΄ β¦ π΅)βπ) = Ξ£π β π΄ π΅ |
90 | 89 | fveq2i 6894 |
. . . . . 6
β’ (πΉβΞ£π β π΄ ((π β π΄ β¦ π΅)βπ)) = (πΉβΞ£π β π΄ π΅) |
91 | | sumfc 15657 |
. . . . . 6
β’
Ξ£π β
π΄ ((π β π΄ β¦ (πΉβπ΅))βπ) = Ξ£π β π΄ (πΉβπ΅) |
92 | 88, 90, 91 | 3eqtr3g 2795 |
. . . . 5
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (πΉβΞ£π β π΄ π΅) = Ξ£π β π΄ (πΉβπ΅)) |
93 | 92 | expr 457 |
. . . 4
β’ ((π β§ (β―βπ΄) β β) β (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β (πΉβΞ£π β π΄ π΅) = Ξ£π β π΄ (πΉβπ΅))) |
94 | 93 | exlimdv 1936 |
. . 3
β’ ((π β§ (β―βπ΄) β β) β
(βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄ β (πΉβΞ£π β π΄ π΅) = Ξ£π β π΄ (πΉβπ΅))) |
95 | 94 | expimpd 454 |
. 2
β’ (π β (((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β (πΉβΞ£π β π΄ π΅) = Ξ£π β π΄ (πΉβπ΅))) |
96 | | fsumre.1 |
. . 3
β’ (π β π΄ β Fin) |
97 | | fz1f1o 15658 |
. . 3
β’ (π΄ β Fin β (π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
98 | 96, 97 | syl 17 |
. 2
β’ (π β (π΄ = β
β¨ ((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
99 | 31, 95, 98 | mpjaod 858 |
1
β’ (π β (πΉβΞ£π β π΄ π΅) = Ξ£π β π΄ (πΉβπ΅)) |