Step | Hyp | Ref
| Expression |
1 | | fsummulc2.2 |
. . . 4
β’ (π β πΆ β β) |
2 | 1 | mul01d 8349 |
. . 3
β’ (π β (πΆ Β· 0) = 0) |
3 | | sumeq1 11362 |
. . . . . 6
β’ (π΄ = β
β Ξ£π β π΄ π΅ = Ξ£π β β
π΅) |
4 | | sum0 11395 |
. . . . . 6
β’
Ξ£π β
β
π΅ =
0 |
5 | 3, 4 | eqtrdi 2226 |
. . . . 5
β’ (π΄ = β
β Ξ£π β π΄ π΅ = 0) |
6 | 5 | oveq2d 5890 |
. . . 4
β’ (π΄ = β
β (πΆ Β· Ξ£π β π΄ π΅) = (πΆ Β· 0)) |
7 | | sumeq1 11362 |
. . . . 5
β’ (π΄ = β
β Ξ£π β π΄ (πΆ Β· π΅) = Ξ£π β β
(πΆ Β· π΅)) |
8 | | sum0 11395 |
. . . . 5
β’
Ξ£π β
β
(πΆ Β· π΅) = 0 |
9 | 7, 8 | eqtrdi 2226 |
. . . 4
β’ (π΄ = β
β Ξ£π β π΄ (πΆ Β· π΅) = 0) |
10 | 6, 9 | eqeq12d 2192 |
. . 3
β’ (π΄ = β
β ((πΆ Β· Ξ£π β π΄ π΅) = Ξ£π β π΄ (πΆ Β· π΅) β (πΆ Β· 0) = 0)) |
11 | 2, 10 | syl5ibrcom 157 |
. 2
β’ (π β (π΄ = β
β (πΆ Β· Ξ£π β π΄ π΅) = Ξ£π β π΄ (πΆ Β· π΅))) |
12 | | addcl 7935 |
. . . . . . . . 9
β’ ((π’ β β β§ π£ β β) β (π’ + π£) β β) |
13 | 12 | adantl 277 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ (π’ β β β§ π£ β β)) β (π’ + π£) β β) |
14 | 1 | ad2antrr 488 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ (π’ β β β§ π£ β β)) β πΆ β β) |
15 | | simprl 529 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ (π’ β β β§ π£ β β)) β π’ β β) |
16 | | simprr 531 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ (π’ β β β§ π£ β β)) β π£ β β) |
17 | 14, 15, 16 | adddid 7981 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ (π’ β β β§ π£ β β)) β (πΆ Β· (π’ + π£)) = ((πΆ Β· π’) + (πΆ Β· π£))) |
18 | | simprl 529 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
β) |
19 | | nnuz 9562 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
20 | 18, 19 | eleqtrdi 2270 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
(β€β₯β1)) |
21 | | elnnuz 9563 |
. . . . . . . . . . . 12
β’ (π’ β β β π’ β
(β€β₯β1)) |
22 | 21 | biimpri 133 |
. . . . . . . . . . 11
β’ (π’ β
(β€β₯β1) β π’ β β) |
23 | 22 | adantl 277 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β π’ β
β) |
24 | | f1of 5461 |
. . . . . . . . . . . . . . 15
β’ (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β π:(1...(β―βπ΄))βΆπ΄) |
25 | 24 | ad2antll 491 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))βΆπ΄) |
26 | 25 | ad2antrr 488 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
π:(1...(β―βπ΄))βΆπ΄) |
27 | | 1zzd 9279 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β 1
β β€) |
28 | 18 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
(β―βπ΄) β
β) |
29 | 28 | nnzd 9373 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
(β―βπ΄) β
β€) |
30 | | eluzelz 9536 |
. . . . . . . . . . . . . . . 16
β’ (π’ β
(β€β₯β1) β π’ β β€) |
31 | 30 | ad2antlr 489 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
π’ β
β€) |
32 | 27, 29, 31 | 3jca 1177 |
. . . . . . . . . . . . . 14
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
(1 β β€ β§ (β―βπ΄) β β€ β§ π’ β β€)) |
33 | | eluzle 9539 |
. . . . . . . . . . . . . . . 16
β’ (π’ β
(β€β₯β1) β 1 β€ π’) |
34 | 33 | ad2antlr 489 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β 1
β€ π’) |
35 | | simpr 110 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
π’ β€ (β―βπ΄)) |
36 | 34, 35 | jca 306 |
. . . . . . . . . . . . . 14
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
(1 β€ π’ β§ π’ β€ (β―βπ΄))) |
37 | | elfz2 10014 |
. . . . . . . . . . . . . 14
β’ (π’ β
(1...(β―βπ΄))
β ((1 β β€ β§ (β―βπ΄) β β€ β§ π’ β β€) β§ (1 β€ π’ β§ π’ β€ (β―βπ΄)))) |
38 | 32, 36, 37 | sylanbrc 417 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
π’ β
(1...(β―βπ΄))) |
39 | | fvco3 5587 |
. . . . . . . . . . . . 13
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π’ β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ’) = ((π β π΄ β¦ π΅)β(πβπ’))) |
40 | 26, 38, 39 | syl2anc 411 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
(((π β π΄ β¦ π΅) β π)βπ’) = ((π β π΄ β¦ π΅)β(πβπ’))) |
41 | 26, 38 | ffvelcdmd 5652 |
. . . . . . . . . . . . . 14
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
(πβπ’) β π΄) |
42 | | fsummulc2.3 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π΄) β π΅ β β) |
43 | 42 | ralrimiva 2550 |
. . . . . . . . . . . . . . . 16
β’ (π β βπ β π΄ π΅ β β) |
44 | 43 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
βπ β π΄ π΅ β β) |
45 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . . 17
β’
β²πβ¦(πβπ’) / πβ¦π΅ |
46 | 45 | nfel1 2330 |
. . . . . . . . . . . . . . . 16
β’
β²πβ¦(πβπ’) / πβ¦π΅ β β |
47 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβπ’) β π΅ = β¦(πβπ’) / πβ¦π΅) |
48 | 47 | eleq1d 2246 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ’) β (π΅ β β β β¦(πβπ’) / πβ¦π΅ β β)) |
49 | 46, 48 | rspc 2835 |
. . . . . . . . . . . . . . 15
β’ ((πβπ’) β π΄ β (βπ β π΄ π΅ β β β β¦(πβπ’) / πβ¦π΅ β β)) |
50 | 41, 44, 49 | sylc 62 |
. . . . . . . . . . . . . 14
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
β¦(πβπ’) / πβ¦π΅ β β) |
51 | | eqid 2177 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β¦ π΅) = (π β π΄ β¦ π΅) |
52 | 51 | fvmpts 5594 |
. . . . . . . . . . . . . 14
β’ (((πβπ’) β π΄ β§ β¦(πβπ’) / πβ¦π΅ β β) β ((π β π΄ β¦ π΅)β(πβπ’)) = β¦(πβπ’) / πβ¦π΅) |
53 | 41, 50, 52 | syl2anc 411 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
((π β π΄ β¦ π΅)β(πβπ’)) = β¦(πβπ’) / πβ¦π΅) |
54 | 53, 50 | eqeltrd 2254 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
((π β π΄ β¦ π΅)β(πβπ’)) β β) |
55 | 40, 54 | eqeltrd 2254 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
(((π β π΄ β¦ π΅) β π)βπ’) β β) |
56 | | 0cnd 7949 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ Β¬ π’ β€
(β―βπ΄)) β 0
β β) |
57 | 23 | nnzd 9373 |
. . . . . . . . . . . 12
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β π’ β
β€) |
58 | 18 | adantr 276 |
. . . . . . . . . . . . 13
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β (β―βπ΄)
β β) |
59 | 58 | nnzd 9373 |
. . . . . . . . . . . 12
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β (β―βπ΄)
β β€) |
60 | | zdcle 9328 |
. . . . . . . . . . . 12
β’ ((π’ β β€ β§
(β―βπ΄) β
β€) β DECID π’ β€ (β―βπ΄)) |
61 | 57, 59, 60 | syl2anc 411 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β DECID π’ β€ (β―βπ΄)) |
62 | 55, 56, 61 | ifcldadc 3563 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β if(π’ β€
(β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ’), 0) β β) |
63 | | breq1 4006 |
. . . . . . . . . . . 12
β’ (π = π’ β (π β€ (β―βπ΄) β π’ β€ (β―βπ΄))) |
64 | | fveq2 5515 |
. . . . . . . . . . . 12
β’ (π = π’ β (((π β π΄ β¦ π΅) β π)βπ) = (((π β π΄ β¦ π΅) β π)βπ’)) |
65 | 63, 64 | ifbieq1d 3556 |
. . . . . . . . . . 11
β’ (π = π’ β if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 0) = if(π’ β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ’), 0)) |
66 | | eqid 2177 |
. . . . . . . . . . 11
β’ (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 0)) = (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 0)) |
67 | 65, 66 | fvmptg 5592 |
. . . . . . . . . 10
β’ ((π’ β β β§ if(π’ β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ’), 0) β β) β ((π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 0))βπ’) = if(π’ β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ’), 0)) |
68 | 23, 62, 67 | syl2anc 411 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β ((π β β
β¦ if(π β€
(β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 0))βπ’) = if(π’ β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ’), 0)) |
69 | 68, 62 | eqeltrd 2254 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β ((π β β
β¦ if(π β€
(β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 0))βπ’) β β) |
70 | | csbov2g 5915 |
. . . . . . . . . . . 12
β’ ((πβπ’) β π΄ β β¦(πβπ’) / πβ¦(πΆ Β· π΅) = (πΆ Β· β¦(πβπ’) / πβ¦π΅)) |
71 | 41, 70 | syl 14 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
β¦(πβπ’) / πβ¦(πΆ Β· π΅) = (πΆ Β· β¦(πβπ’) / πβ¦π΅)) |
72 | 35 | iftrued 3541 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
if(π’ β€
(β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’), 0) = (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’)) |
73 | | fvco3 5587 |
. . . . . . . . . . . . 13
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π’ β (1...(β―βπ΄))) β (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’) = ((π β π΄ β¦ (πΆ Β· π΅))β(πβπ’))) |
74 | 26, 38, 73 | syl2anc 411 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
(((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’) = ((π β π΄ β¦ (πΆ Β· π΅))β(πβπ’))) |
75 | 1 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
πΆ β
β) |
76 | 75, 50 | mulcld 7977 |
. . . . . . . . . . . . . 14
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
(πΆ Β·
β¦(πβπ’) / πβ¦π΅) β β) |
77 | 71, 76 | eqeltrd 2254 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
β¦(πβπ’) / πβ¦(πΆ Β· π΅) β β) |
78 | | eqid 2177 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β¦ (πΆ Β· π΅)) = (π β π΄ β¦ (πΆ Β· π΅)) |
79 | 78 | fvmpts 5594 |
. . . . . . . . . . . . 13
β’ (((πβπ’) β π΄ β§ β¦(πβπ’) / πβ¦(πΆ Β· π΅) β β) β ((π β π΄ β¦ (πΆ Β· π΅))β(πβπ’)) = β¦(πβπ’) / πβ¦(πΆ Β· π΅)) |
80 | 41, 77, 79 | syl2anc 411 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
((π β π΄ β¦ (πΆ Β· π΅))β(πβπ’)) = β¦(πβπ’) / πβ¦(πΆ Β· π΅)) |
81 | 72, 74, 80 | 3eqtrd 2214 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
if(π’ β€
(β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’), 0) = β¦(πβπ’) / πβ¦(πΆ Β· π΅)) |
82 | 35 | iftrued 3541 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
if(π’ β€
(β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ’), 0) = (((π β π΄ β¦ π΅) β π)βπ’)) |
83 | 82, 40, 53 | 3eqtrd 2214 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
if(π’ β€
(β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ’), 0) = β¦(πβπ’) / πβ¦π΅) |
84 | 83 | oveq2d 5890 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
(πΆ Β· if(π’ β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ’), 0)) = (πΆ Β· β¦(πβπ’) / πβ¦π΅)) |
85 | 71, 81, 84 | 3eqtr4d 2220 |
. . . . . . . . . 10
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
if(π’ β€
(β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’), 0) = (πΆ Β· if(π’ β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ’), 0))) |
86 | 1 | ad3antrrr 492 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ Β¬ π’ β€
(β―βπ΄)) β
πΆ β
β) |
87 | 86 | mul01d 8349 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ Β¬ π’ β€
(β―βπ΄)) β
(πΆ Β· 0) =
0) |
88 | | simpr 110 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ Β¬ π’ β€
(β―βπ΄)) β
Β¬ π’ β€
(β―βπ΄)) |
89 | 88 | iffalsed 3544 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ Β¬ π’ β€
(β―βπ΄)) β
if(π’ β€
(β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ’), 0) = 0) |
90 | 89 | oveq2d 5890 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ Β¬ π’ β€
(β―βπ΄)) β
(πΆ Β· if(π’ β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ’), 0)) = (πΆ Β· 0)) |
91 | 88 | iffalsed 3544 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ Β¬ π’ β€
(β―βπ΄)) β
if(π’ β€
(β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’), 0) = 0) |
92 | 87, 90, 91 | 3eqtr4rd 2221 |
. . . . . . . . . 10
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ Β¬ π’ β€
(β―βπ΄)) β
if(π’ β€
(β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’), 0) = (πΆ Β· if(π’ β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ’), 0))) |
93 | | exmiddc 836 |
. . . . . . . . . . 11
β’
(DECID π’ β€ (β―βπ΄) β (π’ β€ (β―βπ΄) β¨ Β¬ π’ β€ (β―βπ΄))) |
94 | 61, 93 | syl 14 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β (π’ β€
(β―βπ΄) β¨
Β¬ π’ β€
(β―βπ΄))) |
95 | 85, 92, 94 | mpjaodan 798 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β if(π’ β€
(β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’), 0) = (πΆ Β· if(π’ β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ’), 0))) |
96 | 80, 77 | eqeltrd 2254 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
((π β π΄ β¦ (πΆ Β· π΅))β(πβπ’)) β β) |
97 | 74, 96 | eqeltrd 2254 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β§ π’ β€
(β―βπ΄)) β
(((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’) β β) |
98 | 97, 56, 61 | ifcldadc 3563 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β if(π’ β€
(β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’), 0) β β) |
99 | | fveq2 5515 |
. . . . . . . . . . . 12
β’ (π = π’ β (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ) = (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’)) |
100 | 63, 99 | ifbieq1d 3556 |
. . . . . . . . . . 11
β’ (π = π’ β if(π β€ (β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ), 0) = if(π’ β€ (β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’), 0)) |
101 | | eqid 2177 |
. . . . . . . . . . 11
β’ (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ), 0)) = (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ), 0)) |
102 | 100, 101 | fvmptg 5592 |
. . . . . . . . . 10
β’ ((π’ β β β§ if(π’ β€ (β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’), 0) β β) β ((π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ), 0))βπ’) = if(π’ β€ (β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’), 0)) |
103 | 23, 98, 102 | syl2anc 411 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β ((π β β
β¦ if(π β€
(β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ), 0))βπ’) = if(π’ β€ (β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ’), 0)) |
104 | 68 | oveq2d 5890 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β (πΆ Β· ((π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 0))βπ’)) = (πΆ Β· if(π’ β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ’), 0))) |
105 | 95, 103, 104 | 3eqtr4d 2220 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π’ β (β€β₯β1))
β ((π β β
β¦ if(π β€
(β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ), 0))βπ’) = (πΆ Β· ((π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 0))βπ’))) |
106 | | mulcl 7937 |
. . . . . . . . 9
β’ ((π’ β β β§ π£ β β) β (π’ Β· π£) β β) |
107 | 106 | adantl 277 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ (π’ β β β§ π£ β β)) β (π’ Β· π£) β β) |
108 | 1 | adantr 276 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β πΆ β β) |
109 | 13, 17, 20, 69, 105, 107, 108 | seq3distr 10512 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ), 0)))β(β―βπ΄)) = (πΆ Β· (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 0)))β(β―βπ΄)))) |
110 | | fveq2 5515 |
. . . . . . . 8
β’ (π = (πβπ) β ((π β π΄ β¦ (πΆ Β· π΅))βπ) = ((π β π΄ β¦ (πΆ Β· π΅))β(πβπ))) |
111 | | simprr 531 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))β1-1-ontoβπ΄) |
112 | 1 | adantr 276 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β πΆ β β) |
113 | 112, 42 | mulcld 7977 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β (πΆ Β· π΅) β β) |
114 | 113 | fmpttd 5671 |
. . . . . . . . . 10
β’ (π β (π β π΄ β¦ (πΆ Β· π΅)):π΄βΆβ) |
115 | 114 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ (πΆ Β· π΅)):π΄βΆβ) |
116 | 115 | ffvelcdmda 5651 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ (πΆ Β· π΅))βπ) β β) |
117 | | fvco3 5587 |
. . . . . . . . 9
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ) = ((π β π΄ β¦ (πΆ Β· π΅))β(πβπ))) |
118 | 25, 117 | sylan 283 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ) = ((π β π΄ β¦ (πΆ Β· π΅))β(πβπ))) |
119 | 110, 18, 111, 116, 118 | fsum3 11394 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β Ξ£π β π΄ ((π β π΄ β¦ (πΆ Β· π΅))βπ) = (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ (πΆ Β· π΅)) β π)βπ), 0)))β(β―βπ΄))) |
120 | | fveq2 5515 |
. . . . . . . . 9
β’ (π = (πβπ) β ((π β π΄ β¦ π΅)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
121 | 42 | fmpttd 5671 |
. . . . . . . . . . 11
β’ (π β (π β π΄ β¦ π΅):π΄βΆβ) |
122 | 121 | adantr 276 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ π΅):π΄βΆβ) |
123 | 122 | ffvelcdmda 5651 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) β β) |
124 | | fvco3 5587 |
. . . . . . . . . 10
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
125 | 25, 124 | sylan 283 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
126 | 120, 18, 111, 123, 125 | fsum3 11394 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) = (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 0)))β(β―βπ΄))) |
127 | 126 | oveq2d 5890 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (πΆ Β· Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ)) = (πΆ Β· (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 0)))β(β―βπ΄)))) |
128 | 109, 119,
127 | 3eqtr4rd 2221 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (πΆ Β· Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ)) = Ξ£π β π΄ ((π β π΄ β¦ (πΆ Β· π΅))βπ)) |
129 | | sumfct 11381 |
. . . . . . . . 9
β’
(βπ β
π΄ π΅ β β β Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) = Ξ£π β π΄ π΅) |
130 | 43, 129 | syl 14 |
. . . . . . . 8
β’ (π β Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) = Ξ£π β π΄ π΅) |
131 | 130 | oveq2d 5890 |
. . . . . . 7
β’ (π β (πΆ Β· Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ)) = (πΆ Β· Ξ£π β π΄ π΅)) |
132 | 131 | adantr 276 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (πΆ Β· Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ)) = (πΆ Β· Ξ£π β π΄ π΅)) |
133 | 113 | ralrimiva 2550 |
. . . . . . . 8
β’ (π β βπ β π΄ (πΆ Β· π΅) β β) |
134 | | sumfct 11381 |
. . . . . . . 8
β’
(βπ β
π΄ (πΆ Β· π΅) β β β Ξ£π β π΄ ((π β π΄ β¦ (πΆ Β· π΅))βπ) = Ξ£π β π΄ (πΆ Β· π΅)) |
135 | 133, 134 | syl 14 |
. . . . . . 7
β’ (π β Ξ£π β π΄ ((π β π΄ β¦ (πΆ Β· π΅))βπ) = Ξ£π β π΄ (πΆ Β· π΅)) |
136 | 135 | adantr 276 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β Ξ£π β π΄ ((π β π΄ β¦ (πΆ Β· π΅))βπ) = Ξ£π β π΄ (πΆ Β· π΅)) |
137 | 128, 132,
136 | 3eqtr3d 2218 |
. . . . 5
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (πΆ Β· Ξ£π β π΄ π΅) = Ξ£π β π΄ (πΆ Β· π΅)) |
138 | 137 | expr 375 |
. . . 4
β’ ((π β§ (β―βπ΄) β β) β (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β (πΆ Β· Ξ£π β π΄ π΅) = Ξ£π β π΄ (πΆ Β· π΅))) |
139 | 138 | exlimdv 1819 |
. . 3
β’ ((π β§ (β―βπ΄) β β) β
(βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄ β (πΆ Β· Ξ£π β π΄ π΅) = Ξ£π β π΄ (πΆ Β· π΅))) |
140 | 139 | expimpd 363 |
. 2
β’ (π β (((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β (πΆ Β· Ξ£π β π΄ π΅) = Ξ£π β π΄ (πΆ Β· π΅))) |
141 | | fsummulc2.1 |
. . 3
β’ (π β π΄ β Fin) |
142 | | fz1f1o 11382 |
. . 3
β’ (π΄ β Fin β (π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
143 | 141, 142 | syl 14 |
. 2
β’ (π β (π΄ = β
β¨ ((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
144 | 11, 140, 143 | mpjaod 718 |
1
β’ (π β (πΆ Β· Ξ£π β π΄ π΅) = Ξ£π β π΄ (πΆ Β· π΅)) |