Step | Hyp | Ref
| Expression |
1 | | isumcl.1 |
. . 3
β’ π =
(β€β₯βπ) |
2 | | isumcl.2 |
. . 3
β’ (π β π β β€) |
3 | | eqidd 2734 |
. . 3
β’ ((π β§ π β π) β ((π β π β¦ (π΅ Β· π΄))βπ) = ((π β π β¦ (π΅ Β· π΄))βπ)) |
4 | | summulc.6 |
. . . . . . 7
β’ (π β π΅ β β) |
5 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π) β π΅ β β) |
6 | | isumcl.4 |
. . . . . 6
β’ ((π β§ π β π) β π΄ β β) |
7 | 5, 6 | mulcld 11180 |
. . . . 5
β’ ((π β§ π β π) β (π΅ Β· π΄) β β) |
8 | 7 | fmpttd 7064 |
. . . 4
β’ (π β (π β π β¦ (π΅ Β· π΄)):πβΆβ) |
9 | 8 | ffvelcdmda 7036 |
. . 3
β’ ((π β§ π β π) β ((π β π β¦ (π΅ Β· π΄))βπ) β β) |
10 | | isumcl.3 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) = π΄) |
11 | | isumcl.5 |
. . . . 5
β’ (π β seqπ( + , πΉ) β dom β ) |
12 | 1, 2, 10, 6, 11 | isumclim2 15648 |
. . . 4
β’ (π β seqπ( + , πΉ) β Ξ£π β π π΄) |
13 | 10, 6 | eqeltrd 2834 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β β) |
14 | 13 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β π (πΉβπ) β β) |
15 | | fveq2 6843 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
16 | 15 | eleq1d 2819 |
. . . . . 6
β’ (π = π β ((πΉβπ) β β β (πΉβπ) β β)) |
17 | 16 | rspccva 3579 |
. . . . 5
β’
((βπ β
π (πΉβπ) β β β§ π β π) β (πΉβπ) β β) |
18 | 14, 17 | sylan 581 |
. . . 4
β’ ((π β§ π β π) β (πΉβπ) β β) |
19 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β π) β π β π) |
20 | | ovex 7391 |
. . . . . . . 8
β’ (π΅ Β· π΄) β V |
21 | | eqid 2733 |
. . . . . . . . 9
β’ (π β π β¦ (π΅ Β· π΄)) = (π β π β¦ (π΅ Β· π΄)) |
22 | 21 | fvmpt2 6960 |
. . . . . . . 8
β’ ((π β π β§ (π΅ Β· π΄) β V) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· π΄)) |
23 | 19, 20, 22 | sylancl 587 |
. . . . . . 7
β’ ((π β§ π β π) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· π΄)) |
24 | 10 | oveq2d 7374 |
. . . . . . 7
β’ ((π β§ π β π) β (π΅ Β· (πΉβπ)) = (π΅ Β· π΄)) |
25 | 23, 24 | eqtr4d 2776 |
. . . . . 6
β’ ((π β§ π β π) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ))) |
26 | 25 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β π ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ))) |
27 | | nffvmpt1 6854 |
. . . . . . 7
β’
β²π((π β π β¦ (π΅ Β· π΄))βπ) |
28 | 27 | nfeq1 2919 |
. . . . . 6
β’
β²π((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ)) |
29 | | fveq2 6843 |
. . . . . . 7
β’ (π = π β ((π β π β¦ (π΅ Β· π΄))βπ) = ((π β π β¦ (π΅ Β· π΄))βπ)) |
30 | 15 | oveq2d 7374 |
. . . . . . 7
β’ (π = π β (π΅ Β· (πΉβπ)) = (π΅ Β· (πΉβπ))) |
31 | 29, 30 | eqeq12d 2749 |
. . . . . 6
β’ (π = π β (((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ)) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ)))) |
32 | 28, 31 | rspc 3568 |
. . . . 5
β’ (π β π β (βπ β π ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ)) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ)))) |
33 | 26, 32 | mpan9 508 |
. . . 4
β’ ((π β§ π β π) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ))) |
34 | 1, 2, 4, 12, 18, 33 | isermulc2 15548 |
. . 3
β’ (π β seqπ( + , (π β π β¦ (π΅ Β· π΄))) β (π΅ Β· Ξ£π β π π΄)) |
35 | 1, 2, 3, 9, 34 | isumclim 15647 |
. 2
β’ (π β Ξ£π β π ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· Ξ£π β π π΄)) |
36 | | sumfc 15599 |
. 2
β’
Ξ£π β
π ((π β π β¦ (π΅ Β· π΄))βπ) = Ξ£π β π (π΅ Β· π΄) |
37 | 35, 36 | eqtr3di 2788 |
1
β’ (π β (π΅ Β· Ξ£π β π π΄) = Ξ£π β π (π΅ Β· π΄)) |