Step | Hyp | Ref
| Expression |
1 | | sumss.1 |
. . . . 5
β’ (π β π΄ β π΅) |
2 | 1 | adantr 482 |
. . . 4
β’ ((π β§ π΅ = β
) β π΄ β π΅) |
3 | | sumss.2 |
. . . . 5
β’ ((π β§ π β π΄) β πΆ β β) |
4 | 3 | adantlr 714 |
. . . 4
β’ (((π β§ π΅ = β
) β§ π β π΄) β πΆ β β) |
5 | | sumss.3 |
. . . . 5
β’ ((π β§ π β (π΅ β π΄)) β πΆ = 0) |
6 | 5 | adantlr 714 |
. . . 4
β’ (((π β§ π΅ = β
) β§ π β (π΅ β π΄)) β πΆ = 0) |
7 | | simpr 486 |
. . . . 5
β’ ((π β§ π΅ = β
) β π΅ = β
) |
8 | | 0ss 4357 |
. . . . 5
β’ β
β (β€β₯β0) |
9 | 7, 8 | eqsstrdi 3999 |
. . . 4
β’ ((π β§ π΅ = β
) β π΅ β
(β€β₯β0)) |
10 | 2, 4, 6, 9 | sumss 15614 |
. . 3
β’ ((π β§ π΅ = β
) β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) |
11 | 10 | ex 414 |
. 2
β’ (π β (π΅ = β
β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ)) |
12 | | cnvimass 6034 |
. . . . . . . . 9
β’ (β‘π β π΄) β dom π |
13 | | simprr 772 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π:(1...(β―βπ΅))β1-1-ontoβπ΅) |
14 | | f1of 6785 |
. . . . . . . . . 10
β’ (π:(1...(β―βπ΅))β1-1-ontoβπ΅ β π:(1...(β―βπ΅))βΆπ΅) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π:(1...(β―βπ΅))βΆπ΅) |
16 | 12, 15 | fssdm 6689 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (β‘π β π΄) β (1...(β―βπ΅))) |
17 | 15 | ffnd 6670 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π Fn (1...(β―βπ΅))) |
18 | | elpreima 7009 |
. . . . . . . . . . . 12
β’ (π Fn (1...(β―βπ΅)) β (π β (β‘π β π΄) β (π β (1...(β―βπ΅)) β§ (πβπ) β π΄))) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π β (β‘π β π΄) β (π β (1...(β―βπ΅)) β§ (πβπ) β π΄))) |
20 | 15 | ffvelcdmda 7036 |
. . . . . . . . . . . . 13
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β (1...(β―βπ΅))) β (πβπ) β π΅) |
21 | 20 | ex 414 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π β (1...(β―βπ΅)) β (πβπ) β π΅)) |
22 | 21 | adantrd 493 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β ((π β (1...(β―βπ΅)) β§ (πβπ) β π΄) β (πβπ) β π΅)) |
23 | 19, 22 | sylbid 239 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π β (β‘π β π΄) β (πβπ) β π΅)) |
24 | 23 | imp 408 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β (β‘π β π΄)) β (πβπ) β π΅) |
25 | 3 | ex 414 |
. . . . . . . . . . . . . 14
β’ (π β (π β π΄ β πΆ β β)) |
26 | 25 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β (π β π΄ β πΆ β β)) |
27 | | eldif 3921 |
. . . . . . . . . . . . . . 15
β’ (π β (π΅ β π΄) β (π β π΅ β§ Β¬ π β π΄)) |
28 | | 0cn 11152 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β |
29 | 5, 28 | eqeltrdi 2842 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π΅ β π΄)) β πΆ β β) |
30 | 27, 29 | sylan2br 596 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ Β¬ π β π΄)) β πΆ β β) |
31 | 30 | expr 458 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β (Β¬ π β π΄ β πΆ β β)) |
32 | 26, 31 | pm2.61d 179 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β πΆ β β) |
33 | 32 | fmpttd 7064 |
. . . . . . . . . . 11
β’ (π β (π β π΅ β¦ πΆ):π΅βΆβ) |
34 | 33 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π β π΅ β¦ πΆ):π΅βΆβ) |
35 | 34 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ (πβπ) β π΅) β ((π β π΅ β¦ πΆ)β(πβπ)) β β) |
36 | 24, 35 | syldan 592 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β (β‘π β π΄)) β ((π β π΅ β¦ πΆ)β(πβπ)) β β) |
37 | | eldifi 4087 |
. . . . . . . . . . . 12
β’ (π β
((1...(β―βπ΅))
β (β‘π β π΄)) β π β (1...(β―βπ΅))) |
38 | 37, 20 | sylan2 594 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β (πβπ) β π΅) |
39 | | eldifn 4088 |
. . . . . . . . . . . . 13
β’ (π β
((1...(β―βπ΅))
β (β‘π β π΄)) β Β¬ π β (β‘π β π΄)) |
40 | 39 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β Β¬ π β (β‘π β π΄)) |
41 | 37 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β π β (1...(β―βπ΅))) |
42 | 19 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β (π β (β‘π β π΄) β (π β (1...(β―βπ΅)) β§ (πβπ) β π΄))) |
43 | 41, 42 | mpbirand 706 |
. . . . . . . . . . . 12
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β (π β (β‘π β π΄) β (πβπ) β π΄)) |
44 | 40, 43 | mtbid 324 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β Β¬ (πβπ) β π΄) |
45 | 38, 44 | eldifd 3922 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β (πβπ) β (π΅ β π΄)) |
46 | | difss 4092 |
. . . . . . . . . . . . 13
β’ (π΅ β π΄) β π΅ |
47 | | resmpt 5992 |
. . . . . . . . . . . . 13
β’ ((π΅ β π΄) β π΅ β ((π β π΅ β¦ πΆ) βΎ (π΅ β π΄)) = (π β (π΅ β π΄) β¦ πΆ)) |
48 | 46, 47 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((π β π΅ β¦ πΆ) βΎ (π΅ β π΄)) = (π β (π΅ β π΄) β¦ πΆ) |
49 | 48 | fveq1i 6844 |
. . . . . . . . . . 11
β’ (((π β π΅ β¦ πΆ) βΎ (π΅ β π΄))β(πβπ)) = ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) |
50 | | fvres 6862 |
. . . . . . . . . . 11
β’ ((πβπ) β (π΅ β π΄) β (((π β π΅ β¦ πΆ) βΎ (π΅ β π΄))β(πβπ)) = ((π β π΅ β¦ πΆ)β(πβπ))) |
51 | 49, 50 | eqtr3id 2787 |
. . . . . . . . . 10
β’ ((πβπ) β (π΅ β π΄) β ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) = ((π β π΅ β¦ πΆ)β(πβπ))) |
52 | 45, 51 | syl 17 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) = ((π β π΅ β¦ πΆ)β(πβπ))) |
53 | | c0ex 11154 |
. . . . . . . . . . . . . . 15
β’ 0 β
V |
54 | 53 | elsn2 4626 |
. . . . . . . . . . . . . 14
β’ (πΆ β {0} β πΆ = 0) |
55 | 5, 54 | sylibr 233 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΅ β π΄)) β πΆ β {0}) |
56 | 55 | fmpttd 7064 |
. . . . . . . . . . . 12
β’ (π β (π β (π΅ β π΄) β¦ πΆ):(π΅ β π΄)βΆ{0}) |
57 | 56 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β (π β (π΅ β π΄) β¦ πΆ):(π΅ β π΄)βΆ{0}) |
58 | 57, 45 | ffvelcdmd 7037 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) β {0}) |
59 | | elsni 4604 |
. . . . . . . . . 10
β’ (((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) β {0} β ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) = 0) |
60 | 58, 59 | syl 17 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) = 0) |
61 | 52, 60 | eqtr3d 2775 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β ((π β π΅ β¦ πΆ)β(πβπ)) = 0) |
62 | | fzssuz 13488 |
. . . . . . . . 9
β’
(1...(β―βπ΅)) β
(β€β₯β1) |
63 | 62 | a1i 11 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β
(1...(β―βπ΅))
β (β€β₯β1)) |
64 | 16, 36, 61, 63 | sumss 15614 |
. . . . . . 7
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β (β‘π β π΄)((π β π΅ β¦ πΆ)β(πβπ)) = Ξ£π β (1...(β―βπ΅))((π β π΅ β¦ πΆ)β(πβπ))) |
65 | 1 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β π΄ β π΅) |
66 | 65 | resmptd 5995 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β ((π β π΅ β¦ πΆ) βΎ π΄) = (π β π΄ β¦ πΆ)) |
67 | 66 | fveq1d 6845 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β (((π β π΅ β¦ πΆ) βΎ π΄)βπ) = ((π β π΄ β¦ πΆ)βπ)) |
68 | | fvres 6862 |
. . . . . . . . . . 11
β’ (π β π΄ β (((π β π΅ β¦ πΆ) βΎ π΄)βπ) = ((π β π΅ β¦ πΆ)βπ)) |
69 | 68 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β (((π β π΅ β¦ πΆ) βΎ π΄)βπ) = ((π β π΅ β¦ πΆ)βπ)) |
70 | 67, 69 | eqtr3d 2775 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β ((π β π΄ β¦ πΆ)βπ) = ((π β π΅ β¦ πΆ)βπ)) |
71 | 70 | sumeq2dv 15593 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β π΄ ((π β π΄ β¦ πΆ)βπ) = Ξ£π β π΄ ((π β π΅ β¦ πΆ)βπ)) |
72 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = (πβπ) β ((π β π΅ β¦ πΆ)βπ) = ((π β π΅ β¦ πΆ)β(πβπ))) |
73 | | fzfid 13884 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β
(1...(β―βπ΅))
β Fin) |
74 | 73, 15 | fisuppfi 9317 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (β‘π β π΄) β Fin) |
75 | | f1of1 6784 |
. . . . . . . . . . . 12
β’ (π:(1...(β―βπ΅))β1-1-ontoβπ΅ β π:(1...(β―βπ΅))β1-1βπ΅) |
76 | 13, 75 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π:(1...(β―βπ΅))β1-1βπ΅) |
77 | | f1ores 6799 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπ΅))β1-1βπ΅ β§ (β‘π β π΄) β (1...(β―βπ΅))) β (π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβ(π β (β‘π β π΄))) |
78 | 76, 16, 77 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβ(π β (β‘π β π΄))) |
79 | | f1ofo 6792 |
. . . . . . . . . . . . 13
β’ (π:(1...(β―βπ΅))β1-1-ontoβπ΅ β π:(1...(β―βπ΅))βontoβπ΅) |
80 | 13, 79 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π:(1...(β―βπ΅))βontoβπ΅) |
81 | 1 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π΄ β π΅) |
82 | | foimacnv 6802 |
. . . . . . . . . . . 12
β’ ((π:(1...(β―βπ΅))βontoβπ΅ β§ π΄ β π΅) β (π β (β‘π β π΄)) = π΄) |
83 | 80, 81, 82 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π β (β‘π β π΄)) = π΄) |
84 | 83 | f1oeq3d 6782 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β ((π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβ(π β (β‘π β π΄)) β (π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβπ΄)) |
85 | 78, 84 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβπ΄) |
86 | | fvres 6862 |
. . . . . . . . . 10
β’ (π β (β‘π β π΄) β ((π βΎ (β‘π β π΄))βπ) = (πβπ)) |
87 | 86 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β (β‘π β π΄)) β ((π βΎ (β‘π β π΄))βπ) = (πβπ)) |
88 | 81 | sselda 3945 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β π β π΅) |
89 | 34 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΅) β ((π β π΅ β¦ πΆ)βπ) β β) |
90 | 88, 89 | syldan 592 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β ((π β π΅ β¦ πΆ)βπ) β β) |
91 | 72, 74, 85, 87, 90 | fsumf1o 15613 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β π΄ ((π β π΅ β¦ πΆ)βπ) = Ξ£π β (β‘π β π΄)((π β π΅ β¦ πΆ)β(πβπ))) |
92 | 71, 91 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β π΄ ((π β π΄ β¦ πΆ)βπ) = Ξ£π β (β‘π β π΄)((π β π΅ β¦ πΆ)β(πβπ))) |
93 | | eqidd 2734 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β (1...(β―βπ΅))) β (πβπ) = (πβπ)) |
94 | 72, 73, 13, 93, 89 | fsumf1o 15613 |
. . . . . . 7
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β π΅ ((π β π΅ β¦ πΆ)βπ) = Ξ£π β (1...(β―βπ΅))((π β π΅ β¦ πΆ)β(πβπ))) |
95 | 64, 92, 94 | 3eqtr4d 2783 |
. . . . . 6
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β π΄ ((π β π΄ β¦ πΆ)βπ) = Ξ£π β π΅ ((π β π΅ β¦ πΆ)βπ)) |
96 | | sumfc 15599 |
. . . . . 6
β’
Ξ£π β
π΄ ((π β π΄ β¦ πΆ)βπ) = Ξ£π β π΄ πΆ |
97 | | sumfc 15599 |
. . . . . 6
β’
Ξ£π β
π΅ ((π β π΅ β¦ πΆ)βπ) = Ξ£π β π΅ πΆ |
98 | 95, 96, 97 | 3eqtr3g 2796 |
. . . . 5
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) |
99 | 98 | expr 458 |
. . . 4
β’ ((π β§ (β―βπ΅) β β) β (π:(1...(β―βπ΅))β1-1-ontoβπ΅ β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ)) |
100 | 99 | exlimdv 1937 |
. . 3
β’ ((π β§ (β―βπ΅) β β) β
(βπ π:(1...(β―βπ΅))β1-1-ontoβπ΅ β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ)) |
101 | 100 | expimpd 455 |
. 2
β’ (π β (((β―βπ΅) β β β§
βπ π:(1...(β―βπ΅))β1-1-ontoβπ΅) β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ)) |
102 | | fsumss.4 |
. . 3
β’ (π β π΅ β Fin) |
103 | | fz1f1o 15600 |
. . 3
β’ (π΅ β Fin β (π΅ = β
β¨
((β―βπ΅) β
β β§ βπ
π:(1...(β―βπ΅))β1-1-ontoβπ΅))) |
104 | 102, 103 | syl 17 |
. 2
β’ (π β (π΅ = β
β¨ ((β―βπ΅) β β β§
βπ π:(1...(β―βπ΅))β1-1-ontoβπ΅))) |
105 | 11, 101, 104 | mpjaod 859 |
1
β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) |