Step | Hyp | Ref
| Expression |
1 | | fsummulc2.2 |
. . . 4
β’ (π β πΆ β β) |
2 | 1 | mul01d 11361 |
. . 3
β’ (π β (πΆ Β· 0) = 0) |
3 | | sumeq1 15580 |
. . . . . 6
β’ (π΄ = β
β Ξ£π β π΄ π΅ = Ξ£π β β
π΅) |
4 | | sum0 15613 |
. . . . . 6
β’
Ξ£π β
β
π΅ =
0 |
5 | 3, 4 | eqtrdi 2793 |
. . . . 5
β’ (π΄ = β
β Ξ£π β π΄ π΅ = 0) |
6 | 5 | oveq2d 7378 |
. . . 4
β’ (π΄ = β
β (πΆ Β· Ξ£π β π΄ π΅) = (πΆ Β· 0)) |
7 | | sumeq1 15580 |
. . . . 5
β’ (π΄ = β
β Ξ£π β π΄ (πΆ Β· π΅) = Ξ£π β β
(πΆ Β· π΅)) |
8 | | sum0 15613 |
. . . . 5
β’
Ξ£π β
β
(πΆ Β· π΅) = 0 |
9 | 7, 8 | eqtrdi 2793 |
. . . 4
β’ (π΄ = β
β Ξ£π β π΄ (πΆ Β· π΅) = 0) |
10 | 6, 9 | eqeq12d 2753 |
. . 3
β’ (π΄ = β
β ((πΆ Β· Ξ£π β π΄ π΅) = Ξ£π β π΄ (πΆ Β· π΅) β (πΆ Β· 0) = 0)) |
11 | 2, 10 | syl5ibrcom 247 |
. 2
β’ (π β (π΄ = β
β (πΆ Β· Ξ£π β π΄ π΅) = Ξ£π β π΄ (πΆ Β· π΅))) |
12 | | addcl 11140 |
. . . . . . . . 9
β’ ((π β β β§ π β β) β (π + π) β β) |
13 | 12 | adantl 483 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ (π β β β§ π β β)) β (π + π) β β) |
14 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β πΆ β β) |
15 | | adddi 11147 |
. . . . . . . . . 10
β’ ((πΆ β β β§ π β β β§ π β β) β (πΆ Β· (π + π)) = ((πΆ Β· π) + (πΆ Β· π))) |
16 | 15 | 3expb 1121 |
. . . . . . . . 9
β’ ((πΆ β β β§ (π β β β§ π β β)) β (πΆ Β· (π + π)) = ((πΆ Β· π) + (πΆ Β· π))) |
17 | 14, 16 | sylan 581 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ (π β β β§ π β β)) β (πΆ Β· (π + π)) = ((πΆ Β· π) + (πΆ Β· π))) |
18 | | simprl 770 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
β) |
19 | | nnuz 12813 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
20 | 18, 19 | eleqtrdi 2848 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
(β€β₯β1)) |
21 | | fsummulc2.3 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π΅ β β) |
22 | 21 | fmpttd 7068 |
. . . . . . . . . . 11
β’ (π β (π β π΄ β¦ π΅):π΄βΆβ) |
23 | 22 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (π β π΄ β¦ π΅):π΄βΆβ) |
24 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))β1-1-ontoβπ΄) |
25 | 24 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β π:(1...(β―βπ΄))β1-1-ontoβπ΄) |
26 | | f1of 6789 |
. . . . . . . . . . 11
β’ (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β π:(1...(β―βπ΄))βΆπ΄) |
27 | 25, 26 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β π:(1...(β―βπ΄))βΆπ΄) |
28 | | fco 6697 |
. . . . . . . . . 10
β’ (((π β π΄ β¦ π΅):π΄βΆβ β§ π:(1...(β―βπ΄))βΆπ΄) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆβ) |
29 | 23, 27, 28 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆβ) |
30 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β π β (1...(β―βπ΄))) |
31 | 29, 30 | ffvelcdmd 7041 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) β β) |
32 | 27, 30 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (πβπ) β π΄) |
33 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β π β π΄) |
34 | 1 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β πΆ β β) |
35 | 34, 21 | mulcld 11182 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β (πΆ Β· π΅) β β) |
36 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β¦ (πΆ Β· π΅)) = (π β π΄ β¦ (πΆ Β· π΅)) |
37 | 36 | fvmpt2 6964 |
. . . . . . . . . . . . . 14
β’ ((π β π΄ β§ (πΆ Β· π΅) β β) β ((π β π΄ β¦ (πΆ Β· π΅))βπ) = (πΆ Β· π΅)) |
38 | 33, 35, 37 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β ((π β π΄ β¦ (πΆ Β· π΅))βπ) = (πΆ Β· π΅)) |
39 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β¦ π΅) = (π β π΄ β¦ π΅) |
40 | 39 | fvmpt2 6964 |
. . . . . . . . . . . . . . 15
β’ ((π β π΄ β§ π΅ β β) β ((π β π΄ β¦ π΅)βπ) = π΅) |
41 | 33, 21, 40 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) = π΅) |
42 | 41 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β (πΆ Β· ((π β π΄ β¦ π΅)βπ)) = (πΆ Β· π΅)) |
43 | 38, 42 | eqtr4d 2780 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β ((π β π΄ β¦ (πΆ Β· π΅))βπ) = (πΆ Β· ((π β π΄ β¦ π΅)βπ))) |
44 | 43 | ralrimiva 3144 |
. . . . . . . . . . 11
β’ (π β βπ β π΄ ((π β π΄ β¦ (πΆ Β· π΅))βπ) = (πΆ Β· ((π β π΄ β¦ π΅)βπ))) |
45 | 44 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β βπ β π΄ ((π β π΄ β¦ (πΆ Β· π΅))βπ) = (πΆ Β· ((π β π΄ β¦ π΅)βπ))) |
46 | | nffvmpt1 6858 |
. . . . . . . . . . . 12
β’
β²π((π β π΄ β¦ (πΆ Β· π΅))β(πβπ)) |
47 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²ππΆ |
48 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²π
Β· |
49 | | nffvmpt1 6858 |
. . . . . . . . . . . . 13
β’
β²π((π β π΄ β¦ π΅)β(πβπ)) |
50 | 47, 48, 49 | nfov 7392 |
. . . . . . . . . . . 12
β’
β²π(πΆ Β· ((π β π΄ β¦ π΅)β(πβπ))) |
51 | 46, 50 | nfeq 2921 |
. . . . . . . . . . 11
β’
β²π((π β π΄ β¦ (πΆ Β· π΅))β(πβπ)) = (πΆ Β· ((π β π΄ β¦ π΅)β(πβπ))) |
52 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β ((π β π΄ β¦ (πΆ Β· π΅))βπ) = ((π β π΄ β¦ (πΆ Β· π΅))β(πβπ))) |
53 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β ((π β π΄ β¦ π΅)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
54 | 53 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β (πΆ Β· ((π β π΄ β¦ π΅)βπ)) = (πΆ Β· ((π β π΄ β¦ π΅)β(πβπ)))) |
55 | 52, 54 | eqeq12d 2753 |
. . . . . . . . . . 11
β’ (π = (πβπ) β (((π β π΄ β¦ (πΆ Β· π΅))βπ) = (πΆ Β· ((π β π΄ β¦ π΅)βπ)) β ((π β π΄ β¦ (πΆ Β· π΅))β(πβπ)) = (πΆ Β· ((π β π΄ β¦ π΅)β(πβπ))))) |
56 | 51, 55 | rspc 3572 |
. . . . . . . . . 10
β’ ((πβπ) β π΄ β (βπ β π΄ ((π β π΄ β¦ (πΆ Β· π΅))βπ) = (πΆ Β· ((π β π΄ β¦ π΅)βπ)) β ((π β π΄ β¦ (πΆ Β· π΅))β(πβπ)) = (πΆ Β· ((π β π΄ β¦ π΅)β(πβπ))))) |
57 | 32, 45, 56 | sylc 65 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β ((π β π΄ β¦ (πΆ Β· π΅))β(πβπ)) = (πΆ Β· ((π β π΄ β¦ π΅)β(πβπ)))) |
58 | 26 | ad2antll 728 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))βΆπ΄) |
59 | | fvco3 6945 |
. . . . . . . . . 10
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ) = ((π β π΄ β¦ (πΆ Β· π΅))β(πβπ))) |
60 | 58, 59 | sylan 581 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ) = ((π β π΄ β¦ (πΆ Β· π΅))β(πβπ))) |
61 | | fvco3 6945 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
62 | 58, 61 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
63 | 62 | oveq2d 7378 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (πΆ Β· (((π β π΄ β¦ π΅) β π)βπ)) = (πΆ Β· ((π β π΄ β¦ π΅)β(πβπ)))) |
64 | 57, 60, 63 | 3eqtr4d 2787 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ) = (πΆ Β· (((π β π΄ β¦ π΅) β π)βπ))) |
65 | 13, 17, 20, 31, 64 | seqdistr 13966 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (seq1( + , ((π β π΄ β¦ (πΆ Β· π΅)) β π))β(β―βπ΄)) = (πΆ Β· (seq1( + , ((π β π΄ β¦ π΅) β π))β(β―βπ΄)))) |
66 | | fveq2 6847 |
. . . . . . . 8
β’ (π = (πβπ) β ((π β π΄ β¦ (πΆ Β· π΅))βπ) = ((π β π΄ β¦ (πΆ Β· π΅))β(πβπ))) |
67 | 35 | fmpttd 7068 |
. . . . . . . . . 10
β’ (π β (π β π΄ β¦ (πΆ Β· π΅)):π΄βΆβ) |
68 | 67 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ (πΆ Β· π΅)):π΄βΆβ) |
69 | 68 | ffvelcdmda 7040 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ (πΆ Β· π΅))βπ) β β) |
70 | 66, 18, 24, 69, 60 | fsum 15612 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β Ξ£π β π΄ ((π β π΄ β¦ (πΆ Β· π΅))βπ) = (seq1( + , ((π β π΄ β¦ (πΆ Β· π΅)) β π))β(β―βπ΄))) |
71 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = (πβπ) β ((π β π΄ β¦ π΅)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
72 | 22 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ π΅):π΄βΆβ) |
73 | 72 | ffvelcdmda 7040 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) β β) |
74 | 71, 18, 24, 73, 62 | fsum 15612 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) = (seq1( + , ((π β π΄ β¦ π΅) β π))β(β―βπ΄))) |
75 | 74 | oveq2d 7378 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (πΆ Β· Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ)) = (πΆ Β· (seq1( + , ((π β π΄ β¦ π΅) β π))β(β―βπ΄)))) |
76 | 65, 70, 75 | 3eqtr4rd 2788 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (πΆ Β· Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ)) = Ξ£π β π΄ ((π β π΄ β¦ (πΆ Β· π΅))βπ)) |
77 | | sumfc 15601 |
. . . . . . 7
β’
Ξ£π β
π΄ ((π β π΄ β¦ π΅)βπ) = Ξ£π β π΄ π΅ |
78 | 77 | oveq2i 7373 |
. . . . . 6
β’ (πΆ Β· Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ)) = (πΆ Β· Ξ£π β π΄ π΅) |
79 | | sumfc 15601 |
. . . . . 6
β’
Ξ£π β
π΄ ((π β π΄ β¦ (πΆ Β· π΅))βπ) = Ξ£π β π΄ (πΆ Β· π΅) |
80 | 76, 78, 79 | 3eqtr3g 2800 |
. . . . 5
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (πΆ Β· Ξ£π β π΄ π΅) = Ξ£π β π΄ (πΆ Β· π΅)) |
81 | 80 | expr 458 |
. . . 4
β’ ((π β§ (β―βπ΄) β β) β (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β (πΆ Β· Ξ£π β π΄ π΅) = Ξ£π β π΄ (πΆ Β· π΅))) |
82 | 81 | exlimdv 1937 |
. . 3
β’ ((π β§ (β―βπ΄) β β) β
(βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄ β (πΆ Β· Ξ£π β π΄ π΅) = Ξ£π β π΄ (πΆ Β· π΅))) |
83 | 82 | expimpd 455 |
. 2
β’ (π β (((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β (πΆ Β· Ξ£π β π΄ π΅) = Ξ£π β π΄ (πΆ Β· π΅))) |
84 | | fsummulc2.1 |
. . 3
β’ (π β π΄ β Fin) |
85 | | fz1f1o 15602 |
. . 3
β’ (π΄ β Fin β (π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
86 | 84, 85 | syl 17 |
. 2
β’ (π β (π΄ = β
β¨ ((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
87 | 11, 83, 86 | mpjaod 859 |
1
β’ (π β (πΆ Β· Ξ£π β π΄ π΅) = Ξ£π β π΄ (πΆ Β· π΅)) |