Step | Hyp | Ref
| Expression |
1 | | fsumss.1 |
. . . . . 6
β’ (π β π΄ β π΅) |
2 | | sseq0 3464 |
. . . . . 6
β’ ((π΄ β π΅ β§ π΅ = β
) β π΄ = β
) |
3 | 1, 2 | sylan 283 |
. . . . 5
β’ ((π β§ π΅ = β
) β π΄ = β
) |
4 | 3 | sumeq1d 11373 |
. . . 4
β’ ((π β§ π΅ = β
) β Ξ£π β π΄ πΆ = Ξ£π β β
πΆ) |
5 | | simpr 110 |
. . . . 5
β’ ((π β§ π΅ = β
) β π΅ = β
) |
6 | 5 | sumeq1d 11373 |
. . . 4
β’ ((π β§ π΅ = β
) β Ξ£π β π΅ πΆ = Ξ£π β β
πΆ) |
7 | 4, 6 | eqtr4d 2213 |
. . 3
β’ ((π β§ π΅ = β
) β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) |
8 | 7 | ex 115 |
. 2
β’ (π β (π΅ = β
β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ)) |
9 | | cnvimass 4991 |
. . . . . . . . 9
β’ (β‘π β π΄) β dom π |
10 | | simprr 531 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π:(1...(β―βπ΅))β1-1-ontoβπ΅) |
11 | | f1of 5461 |
. . . . . . . . . 10
β’ (π:(1...(β―βπ΅))β1-1-ontoβπ΅ β π:(1...(β―βπ΅))βΆπ΅) |
12 | 10, 11 | syl 14 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π:(1...(β―βπ΅))βΆπ΅) |
13 | 9, 12 | fssdm 5380 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (β‘π β π΄) β (1...(β―βπ΅))) |
14 | 12 | ffnd 5366 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π Fn (1...(β―βπ΅))) |
15 | | elpreima 5635 |
. . . . . . . . . . . 12
β’ (π Fn (1...(β―βπ΅)) β (π β (β‘π β π΄) β (π β (1...(β―βπ΅)) β§ (πβπ) β π΄))) |
16 | 14, 15 | syl 14 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π β (β‘π β π΄) β (π β (1...(β―βπ΅)) β§ (πβπ) β π΄))) |
17 | 12 | ffvelcdmda 5651 |
. . . . . . . . . . . . 13
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β (1...(β―βπ΅))) β (πβπ) β π΅) |
18 | 17 | ex 115 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π β (1...(β―βπ΅)) β (πβπ) β π΅)) |
19 | 18 | adantrd 279 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β ((π β (1...(β―βπ΅)) β§ (πβπ) β π΄) β (πβπ) β π΅)) |
20 | 16, 19 | sylbid 150 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π β (β‘π β π΄) β (πβπ) β π΅)) |
21 | 20 | imp 124 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β (β‘π β π΄)) β (πβπ) β π΅) |
22 | | fsumss.2 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β πΆ β β) |
23 | 22 | ex 115 |
. . . . . . . . . . . . . 14
β’ (π β (π β π΄ β πΆ β β)) |
24 | 23 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β (π β π΄ β πΆ β β)) |
25 | | eldif 3138 |
. . . . . . . . . . . . . . 15
β’ (π β (π΅ β π΄) β (π β π΅ β§ Β¬ π β π΄)) |
26 | | fsumss.3 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΅ β π΄)) β πΆ = 0) |
27 | | 0cn 7948 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β |
28 | 26, 27 | eqeltrdi 2268 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π΅ β π΄)) β πΆ β β) |
29 | 25, 28 | sylan2br 288 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ Β¬ π β π΄)) β πΆ β β) |
30 | 29 | expr 375 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β (Β¬ π β π΄ β πΆ β β)) |
31 | | eleq1w 2238 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π β π΄ β π β π΄)) |
32 | 31 | dcbid 838 |
. . . . . . . . . . . . . . 15
β’ (π = π β (DECID π β π΄ β DECID π β π΄)) |
33 | | fisumss.adc |
. . . . . . . . . . . . . . . 16
β’ (π β βπ β π΅ DECID π β π΄) |
34 | 33 | adantr 276 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΅) β βπ β π΅ DECID π β π΄) |
35 | | simpr 110 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΅) β π β π΅) |
36 | 32, 34, 35 | rspcdva 2846 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΅) β DECID π β π΄) |
37 | | exmiddc 836 |
. . . . . . . . . . . . . 14
β’
(DECID π β π΄ β (π β π΄ β¨ Β¬ π β π΄)) |
38 | 36, 37 | syl 14 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β (π β π΄ β¨ Β¬ π β π΄)) |
39 | 24, 30, 38 | mpjaod 718 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β πΆ β β) |
40 | 39 | fmpttd 5671 |
. . . . . . . . . . 11
β’ (π β (π β π΅ β¦ πΆ):π΅βΆβ) |
41 | 40 | adantr 276 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π β π΅ β¦ πΆ):π΅βΆβ) |
42 | 41 | ffvelcdmda 5651 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ (πβπ) β π΅) β ((π β π΅ β¦ πΆ)β(πβπ)) β β) |
43 | 21, 42 | syldan 282 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β (β‘π β π΄)) β ((π β π΅ β¦ πΆ)β(πβπ)) β β) |
44 | | eldifi 3257 |
. . . . . . . . . . . 12
β’ (π β
((1...(β―βπ΅))
β (β‘π β π΄)) β π β (1...(β―βπ΅))) |
45 | 44, 17 | sylan2 286 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β (πβπ) β π΅) |
46 | | eldifn 3258 |
. . . . . . . . . . . . 13
β’ (π β
((1...(β―βπ΅))
β (β‘π β π΄)) β Β¬ π β (β‘π β π΄)) |
47 | 46 | adantl 277 |
. . . . . . . . . . . 12
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β Β¬ π β (β‘π β π΄)) |
48 | 16 | adantr 276 |
. . . . . . . . . . . . 13
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β (π β (β‘π β π΄) β (π β (1...(β―βπ΅)) β§ (πβπ) β π΄))) |
49 | 44 | adantl 277 |
. . . . . . . . . . . . . 14
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β π β (1...(β―βπ΅))) |
50 | 49 | biantrurd 305 |
. . . . . . . . . . . . 13
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β ((πβπ) β π΄ β (π β (1...(β―βπ΅)) β§ (πβπ) β π΄))) |
51 | 48, 50 | bitr4d 191 |
. . . . . . . . . . . 12
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β (π β (β‘π β π΄) β (πβπ) β π΄)) |
52 | 47, 51 | mtbid 672 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β Β¬ (πβπ) β π΄) |
53 | 45, 52 | eldifd 3139 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β (πβπ) β (π΅ β π΄)) |
54 | | difss 3261 |
. . . . . . . . . . . . 13
β’ (π΅ β π΄) β π΅ |
55 | | resmpt 4955 |
. . . . . . . . . . . . 13
β’ ((π΅ β π΄) β π΅ β ((π β π΅ β¦ πΆ) βΎ (π΅ β π΄)) = (π β (π΅ β π΄) β¦ πΆ)) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((π β π΅ β¦ πΆ) βΎ (π΅ β π΄)) = (π β (π΅ β π΄) β¦ πΆ) |
57 | 56 | fveq1i 5516 |
. . . . . . . . . . 11
β’ (((π β π΅ β¦ πΆ) βΎ (π΅ β π΄))β(πβπ)) = ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) |
58 | | fvres 5539 |
. . . . . . . . . . 11
β’ ((πβπ) β (π΅ β π΄) β (((π β π΅ β¦ πΆ) βΎ (π΅ β π΄))β(πβπ)) = ((π β π΅ β¦ πΆ)β(πβπ))) |
59 | 57, 58 | eqtr3id 2224 |
. . . . . . . . . 10
β’ ((πβπ) β (π΅ β π΄) β ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) = ((π β π΅ β¦ πΆ)β(πβπ))) |
60 | 53, 59 | syl 14 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) = ((π β π΅ β¦ πΆ)β(πβπ))) |
61 | | c0ex 7950 |
. . . . . . . . . . . . . . 15
β’ 0 β
V |
62 | 61 | elsn2 3626 |
. . . . . . . . . . . . . 14
β’ (πΆ β {0} β πΆ = 0) |
63 | 26, 62 | sylibr 134 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΅ β π΄)) β πΆ β {0}) |
64 | 63 | fmpttd 5671 |
. . . . . . . . . . . 12
β’ (π β (π β (π΅ β π΄) β¦ πΆ):(π΅ β π΄)βΆ{0}) |
65 | 64 | ad2antrr 488 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β (π β (π΅ β π΄) β¦ πΆ):(π΅ β π΄)βΆ{0}) |
66 | 65, 53 | ffvelcdmd 5652 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) β {0}) |
67 | | elsni 3610 |
. . . . . . . . . 10
β’ (((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) β {0} β ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) = 0) |
68 | 66, 67 | syl 14 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) = 0) |
69 | 60, 68 | eqtr3d 2212 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β ((π β π΅ β¦ πΆ)β(πβπ)) = 0) |
70 | | eleq1 2240 |
. . . . . . . . . . . . 13
β’ (π = (πβπ’) β (π β π΄ β (πβπ’) β π΄)) |
71 | 70 | dcbid 838 |
. . . . . . . . . . . 12
β’ (π = (πβπ’) β (DECID π β π΄ β DECID (πβπ’) β π΄)) |
72 | 33 | ad3antrrr 492 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β§ π’ β
(1...(β―βπ΅)))
β βπ β
π΅ DECID
π β π΄) |
73 | 12 | ad2antrr 488 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β§ π’ β
(1...(β―βπ΅)))
β π:(1...(β―βπ΅))βΆπ΅) |
74 | | simpr 110 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β§ π’ β
(1...(β―βπ΅)))
β π’ β
(1...(β―βπ΅))) |
75 | 73, 74 | ffvelcdmd 5652 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β§ π’ β
(1...(β―βπ΅)))
β (πβπ’) β π΅) |
76 | 71, 72, 75 | rspcdva 2846 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β§ π’ β
(1...(β―βπ΅)))
β DECID (πβπ’) β π΄) |
77 | 10 | ad2antrr 488 |
. . . . . . . . . . . . . 14
β’ ((((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β§ π’ β
(1...(β―βπ΅)))
β π:(1...(β―βπ΅))β1-1-ontoβπ΅) |
78 | | f1ofun 5463 |
. . . . . . . . . . . . . 14
β’ (π:(1...(β―βπ΅))β1-1-ontoβπ΅ β Fun π) |
79 | 77, 78 | syl 14 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β§ π’ β
(1...(β―βπ΅)))
β Fun π) |
80 | | f1odm 5465 |
. . . . . . . . . . . . . . 15
β’ (π:(1...(β―βπ΅))β1-1-ontoβπ΅ β dom π = (1...(β―βπ΅))) |
81 | 77, 80 | syl 14 |
. . . . . . . . . . . . . 14
β’ ((((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β§ π’ β
(1...(β―βπ΅)))
β dom π =
(1...(β―βπ΅))) |
82 | 74, 81 | eleqtrrd 2257 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β§ π’ β
(1...(β―βπ΅)))
β π’ β dom π) |
83 | | fvimacnv 5631 |
. . . . . . . . . . . . 13
β’ ((Fun
π β§ π’ β dom π) β ((πβπ’) β π΄ β π’ β (β‘π β π΄))) |
84 | 79, 82, 83 | syl2anc 411 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β§ π’ β
(1...(β―βπ΅)))
β ((πβπ’) β π΄ β π’ β (β‘π β π΄))) |
85 | 84 | dcbid 838 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β§ π’ β
(1...(β―βπ΅)))
β (DECID (πβπ’) β π΄ β DECID π’ β (β‘π β π΄))) |
86 | 76, 85 | mpbid 147 |
. . . . . . . . . 10
β’ ((((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β§ π’ β
(1...(β―βπ΅)))
β DECID π’ β (β‘π β π΄)) |
87 | | elpreima 5635 |
. . . . . . . . . . . . . . . . 17
β’ (π Fn (1...(β―βπ΅)) β (π’ β (β‘π β π΄) β (π’ β (1...(β―βπ΅)) β§ (πβπ’) β π΄))) |
88 | | simpl 109 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β
(1...(β―βπ΅))
β§ (πβπ’) β π΄) β π’ β (1...(β―βπ΅))) |
89 | 87, 88 | syl6bi 163 |
. . . . . . . . . . . . . . . 16
β’ (π Fn (1...(β―βπ΅)) β (π’ β (β‘π β π΄) β π’ β (1...(β―βπ΅)))) |
90 | 89 | con3d 631 |
. . . . . . . . . . . . . . 15
β’ (π Fn (1...(β―βπ΅)) β (Β¬ π’ β
(1...(β―βπ΅))
β Β¬ π’ β
(β‘π β π΄))) |
91 | 14, 90 | syl 14 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (Β¬ π’ β
(1...(β―βπ΅))
β Β¬ π’ β
(β‘π β π΄))) |
92 | 91 | adantr 276 |
. . . . . . . . . . . . 13
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β (Β¬ π’ β
(1...(β―βπ΅))
β Β¬ π’ β
(β‘π β π΄))) |
93 | 92 | imp 124 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β§ Β¬ π’ β
(1...(β―βπ΅)))
β Β¬ π’ β
(β‘π β π΄)) |
94 | 93 | olcd 734 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β§ Β¬ π’ β
(1...(β―βπ΅)))
β (π’ β (β‘π β π΄) β¨ Β¬ π’ β (β‘π β π΄))) |
95 | | df-dc 835 |
. . . . . . . . . . 11
β’
(DECID π’ β (β‘π β π΄) β (π’ β (β‘π β π΄) β¨ Β¬ π’ β (β‘π β π΄))) |
96 | 94, 95 | sylibr 134 |
. . . . . . . . . 10
β’ ((((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β§ Β¬ π’ β
(1...(β―βπ΅)))
β DECID π’ β (β‘π β π΄)) |
97 | | eluzelz 9536 |
. . . . . . . . . . . . 13
β’ (π’ β
(β€β₯β1) β π’ β β€) |
98 | 97 | adantl 277 |
. . . . . . . . . . . 12
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β π’ β
β€) |
99 | | 1zzd 9279 |
. . . . . . . . . . . 12
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β 1 β β€) |
100 | | simplrl 535 |
. . . . . . . . . . . . 13
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β (β―βπ΅)
β β) |
101 | 100 | nnzd 9373 |
. . . . . . . . . . . 12
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β (β―βπ΅)
β β€) |
102 | | fzdcel 10039 |
. . . . . . . . . . . 12
β’ ((π’ β β€ β§ 1 β
β€ β§ (β―βπ΅) β β€) β
DECID π’
β (1...(β―βπ΅))) |
103 | 98, 99, 101, 102 | syl3anc 1238 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β DECID π’ β (1...(β―βπ΅))) |
104 | | exmiddc 836 |
. . . . . . . . . . 11
β’
(DECID π’ β (1...(β―βπ΅)) β (π’ β (1...(β―βπ΅)) β¨ Β¬ π’ β (1...(β―βπ΅)))) |
105 | 103, 104 | syl 14 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β (π’ β
(1...(β―βπ΅))
β¨ Β¬ π’ β
(1...(β―βπ΅)))) |
106 | 86, 96, 105 | mpjaodan 798 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π’ β (β€β₯β1))
β DECID π’ β (β‘π β π΄)) |
107 | 106 | ralrimiva 2550 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β βπ’ β
(β€β₯β1)DECID π’ β (β‘π β π΄)) |
108 | | 1zzd 9279 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β 1 β
β€) |
109 | | fzssuz 10064 |
. . . . . . . . 9
β’
(1...(β―βπ΅)) β
(β€β₯β1) |
110 | 109 | a1i 9 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β
(1...(β―βπ΅))
β (β€β₯β1)) |
111 | 103 | ralrimiva 2550 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β βπ’ β
(β€β₯β1)DECID π’ β (1...(β―βπ΅))) |
112 | 13, 43, 69, 107, 108, 110, 111 | isumss 11398 |
. . . . . . 7
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β (β‘π β π΄)((π β π΅ β¦ πΆ)β(πβπ)) = Ξ£π β (1...(β―βπ΅))((π β π΅ β¦ πΆ)β(πβπ))) |
113 | 1 | ad2antrr 488 |
. . . . . . . . . . . 12
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β π΄ β π΅) |
114 | 113 | resmptd 4958 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β ((π β π΅ β¦ πΆ) βΎ π΄) = (π β π΄ β¦ πΆ)) |
115 | 114 | fveq1d 5517 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β (((π β π΅ β¦ πΆ) βΎ π΄)βπ) = ((π β π΄ β¦ πΆ)βπ)) |
116 | | fvres 5539 |
. . . . . . . . . . 11
β’ (π β π΄ β (((π β π΅ β¦ πΆ) βΎ π΄)βπ) = ((π β π΅ β¦ πΆ)βπ)) |
117 | 116 | adantl 277 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β (((π β π΅ β¦ πΆ) βΎ π΄)βπ) = ((π β π΅ β¦ πΆ)βπ)) |
118 | 115, 117 | eqtr3d 2212 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β ((π β π΄ β¦ πΆ)βπ) = ((π β π΅ β¦ πΆ)βπ)) |
119 | 118 | sumeq2dv 11375 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β π΄ ((π β π΄ β¦ πΆ)βπ) = Ξ£π β π΄ ((π β π΅ β¦ πΆ)βπ)) |
120 | | fveq2 5515 |
. . . . . . . . 9
β’ (π = (πβπ) β ((π β π΅ β¦ πΆ)βπ) = ((π β π΅ β¦ πΆ)β(πβπ))) |
121 | 1 | adantr 276 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π΄ β π΅) |
122 | | fsumss.4 |
. . . . . . . . . . . 12
β’ (π β π΅ β Fin) |
123 | | ssfidc 6933 |
. . . . . . . . . . . 12
β’ ((π΅ β Fin β§ π΄ β π΅ β§ βπ β π΅ DECID π β π΄) β π΄ β Fin) |
124 | 122, 1, 33, 123 | syl3anc 1238 |
. . . . . . . . . . 11
β’ (π β π΄ β Fin) |
125 | 124 | adantr 276 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π΄ β Fin) |
126 | 121, 10, 125 | preimaf1ofi 6949 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (β‘π β π΄) β Fin) |
127 | | f1of1 5460 |
. . . . . . . . . . . 12
β’ (π:(1...(β―βπ΅))β1-1-ontoβπ΅ β π:(1...(β―βπ΅))β1-1βπ΅) |
128 | 10, 127 | syl 14 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π:(1...(β―βπ΅))β1-1βπ΅) |
129 | | f1ores 5476 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπ΅))β1-1βπ΅ β§ (β‘π β π΄) β (1...(β―βπ΅))) β (π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβ(π β (β‘π β π΄))) |
130 | 128, 13, 129 | syl2anc 411 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβ(π β (β‘π β π΄))) |
131 | | f1ofo 5468 |
. . . . . . . . . . . . 13
β’ (π:(1...(β―βπ΅))β1-1-ontoβπ΅ β π:(1...(β―βπ΅))βontoβπ΅) |
132 | 10, 131 | syl 14 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π:(1...(β―βπ΅))βontoβπ΅) |
133 | | foimacnv 5479 |
. . . . . . . . . . . 12
β’ ((π:(1...(β―βπ΅))βontoβπ΅ β§ π΄ β π΅) β (π β (β‘π β π΄)) = π΄) |
134 | 132, 121,
133 | syl2anc 411 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π β (β‘π β π΄)) = π΄) |
135 | | f1oeq3 5451 |
. . . . . . . . . . 11
β’ ((π β (β‘π β π΄)) = π΄ β ((π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβ(π β (β‘π β π΄)) β (π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβπ΄)) |
136 | 134, 135 | syl 14 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β ((π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβ(π β (β‘π β π΄)) β (π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβπ΄)) |
137 | 130, 136 | mpbid 147 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβπ΄) |
138 | | fvres 5539 |
. . . . . . . . . 10
β’ (π β (β‘π β π΄) β ((π βΎ (β‘π β π΄))βπ) = (πβπ)) |
139 | 138 | adantl 277 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β (β‘π β π΄)) β ((π βΎ (β‘π β π΄))βπ) = (πβπ)) |
140 | 121 | sselda 3155 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β π β π΅) |
141 | 41 | ffvelcdmda 5651 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΅) β ((π β π΅ β¦ πΆ)βπ) β β) |
142 | 140, 141 | syldan 282 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β ((π β π΅ β¦ πΆ)βπ) β β) |
143 | 120, 126,
137, 139, 142 | fsumf1o 11397 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β π΄ ((π β π΅ β¦ πΆ)βπ) = Ξ£π β (β‘π β π΄)((π β π΅ β¦ πΆ)β(πβπ))) |
144 | 119, 143 | eqtrd 2210 |
. . . . . . 7
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β π΄ ((π β π΄ β¦ πΆ)βπ) = Ξ£π β (β‘π β π΄)((π β π΅ β¦ πΆ)β(πβπ))) |
145 | | simprl 529 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (β―βπ΅) β
β) |
146 | 145 | nnzd 9373 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (β―βπ΅) β
β€) |
147 | 108, 146 | fzfigd 10430 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β
(1...(β―βπ΅))
β Fin) |
148 | | eqidd 2178 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β (1...(β―βπ΅))) β (πβπ) = (πβπ)) |
149 | 120, 147,
10, 148, 141 | fsumf1o 11397 |
. . . . . . 7
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β π΅ ((π β π΅ β¦ πΆ)βπ) = Ξ£π β (1...(β―βπ΅))((π β π΅ β¦ πΆ)β(πβπ))) |
150 | 112, 144,
149 | 3eqtr4d 2220 |
. . . . . 6
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β π΄ ((π β π΄ β¦ πΆ)βπ) = Ξ£π β π΅ ((π β π΅ β¦ πΆ)βπ)) |
151 | 22 | ralrimiva 2550 |
. . . . . . . 8
β’ (π β βπ β π΄ πΆ β β) |
152 | | sumfct 11381 |
. . . . . . . 8
β’
(βπ β
π΄ πΆ β β β Ξ£π β π΄ ((π β π΄ β¦ πΆ)βπ) = Ξ£π β π΄ πΆ) |
153 | 151, 152 | syl 14 |
. . . . . . 7
β’ (π β Ξ£π β π΄ ((π β π΄ β¦ πΆ)βπ) = Ξ£π β π΄ πΆ) |
154 | 153 | adantr 276 |
. . . . . 6
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β π΄ ((π β π΄ β¦ πΆ)βπ) = Ξ£π β π΄ πΆ) |
155 | 22 | adantlr 477 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ π β π΄) β πΆ β β) |
156 | | simpll 527 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΅) β§ Β¬ π β π΄) β π) |
157 | | simplr 528 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΅) β§ Β¬ π β π΄) β π β π΅) |
158 | | simpr 110 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΅) β§ Β¬ π β π΄) β Β¬ π β π΄) |
159 | 157, 158 | eldifd 3139 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΅) β§ Β¬ π β π΄) β π β (π΅ β π΄)) |
160 | 156, 159,
26 | syl2anc 411 |
. . . . . . . . . . 11
β’ (((π β§ π β π΅) β§ Β¬ π β π΄) β πΆ = 0) |
161 | | 0cnd 7949 |
. . . . . . . . . . 11
β’ (((π β§ π β π΅) β§ Β¬ π β π΄) β 0 β β) |
162 | 160, 161 | eqeltrd 2254 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ Β¬ π β π΄) β πΆ β β) |
163 | 155, 162,
38 | mpjaodan 798 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β πΆ β β) |
164 | 163 | ralrimiva 2550 |
. . . . . . . 8
β’ (π β βπ β π΅ πΆ β β) |
165 | | sumfct 11381 |
. . . . . . . 8
β’
(βπ β
π΅ πΆ β β β Ξ£π β π΅ ((π β π΅ β¦ πΆ)βπ) = Ξ£π β π΅ πΆ) |
166 | 164, 165 | syl 14 |
. . . . . . 7
β’ (π β Ξ£π β π΅ ((π β π΅ β¦ πΆ)βπ) = Ξ£π β π΅ πΆ) |
167 | 166 | adantr 276 |
. . . . . 6
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β π΅ ((π β π΅ β¦ πΆ)βπ) = Ξ£π β π΅ πΆ) |
168 | 150, 154,
167 | 3eqtr3d 2218 |
. . . . 5
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) |
169 | 168 | expr 375 |
. . . 4
β’ ((π β§ (β―βπ΅) β β) β (π:(1...(β―βπ΅))β1-1-ontoβπ΅ β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ)) |
170 | 169 | exlimdv 1819 |
. . 3
β’ ((π β§ (β―βπ΅) β β) β
(βπ π:(1...(β―βπ΅))β1-1-ontoβπ΅ β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ)) |
171 | 170 | expimpd 363 |
. 2
β’ (π β (((β―βπ΅) β β β§
βπ π:(1...(β―βπ΅))β1-1-ontoβπ΅) β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ)) |
172 | | fz1f1o 11382 |
. . 3
β’ (π΅ β Fin β (π΅ = β
β¨
((β―βπ΅) β
β β§ βπ
π:(1...(β―βπ΅))β1-1-ontoβπ΅))) |
173 | 122, 172 | syl 14 |
. 2
β’ (π β (π΅ = β
β¨ ((β―βπ΅) β β β§
βπ π:(1...(β―βπ΅))β1-1-ontoβπ΅))) |
174 | 8, 171, 173 | mpjaod 718 |
1
β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) |