Step | Hyp | Ref
| Expression |
1 | | isumcl.1 |
. . 3
β’ π =
(β€β₯βπ) |
2 | | isumcl.2 |
. . 3
β’ (π β π β β€) |
3 | | eqidd 2727 |
. . 3
β’ ((π β§ π β π) β ((π β π β¦ (π΅ Β· π΄))βπ) = ((π β π β¦ (π΅ Β· π΄))βπ)) |
4 | | summulc.6 |
. . . . . . 7
β’ (π β π΅ β β) |
5 | 4 | adantr 480 |
. . . . . 6
β’ ((π β§ π β π) β π΅ β β) |
6 | | isumcl.4 |
. . . . . 6
β’ ((π β§ π β π) β π΄ β β) |
7 | 5, 6 | mulcld 11238 |
. . . . 5
β’ ((π β§ π β π) β (π΅ Β· π΄) β β) |
8 | 7 | fmpttd 7110 |
. . . 4
β’ (π β (π β π β¦ (π΅ Β· π΄)):πβΆβ) |
9 | 8 | ffvelcdmda 7080 |
. . 3
β’ ((π β§ π β π) β ((π β π β¦ (π΅ Β· π΄))βπ) β β) |
10 | | isumcl.3 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) = π΄) |
11 | | isumcl.5 |
. . . . 5
β’ (π β seqπ( + , πΉ) β dom β ) |
12 | 1, 2, 10, 6, 11 | isumclim2 15710 |
. . . 4
β’ (π β seqπ( + , πΉ) β Ξ£π β π π΄) |
13 | 10, 6 | eqeltrd 2827 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β β) |
14 | 13 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β π (πΉβπ) β β) |
15 | | fveq2 6885 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
16 | 15 | eleq1d 2812 |
. . . . . 6
β’ (π = π β ((πΉβπ) β β β (πΉβπ) β β)) |
17 | 16 | rspccva 3605 |
. . . . 5
β’
((βπ β
π (πΉβπ) β β β§ π β π) β (πΉβπ) β β) |
18 | 14, 17 | sylan 579 |
. . . 4
β’ ((π β§ π β π) β (πΉβπ) β β) |
19 | | simpr 484 |
. . . . . . . 8
β’ ((π β§ π β π) β π β π) |
20 | | ovex 7438 |
. . . . . . . 8
β’ (π΅ Β· π΄) β V |
21 | | eqid 2726 |
. . . . . . . . 9
β’ (π β π β¦ (π΅ Β· π΄)) = (π β π β¦ (π΅ Β· π΄)) |
22 | 21 | fvmpt2 7003 |
. . . . . . . 8
β’ ((π β π β§ (π΅ Β· π΄) β V) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· π΄)) |
23 | 19, 20, 22 | sylancl 585 |
. . . . . . 7
β’ ((π β§ π β π) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· π΄)) |
24 | 10 | oveq2d 7421 |
. . . . . . 7
β’ ((π β§ π β π) β (π΅ Β· (πΉβπ)) = (π΅ Β· π΄)) |
25 | 23, 24 | eqtr4d 2769 |
. . . . . 6
β’ ((π β§ π β π) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ))) |
26 | 25 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β π ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ))) |
27 | | nffvmpt1 6896 |
. . . . . . 7
β’
β²π((π β π β¦ (π΅ Β· π΄))βπ) |
28 | 27 | nfeq1 2912 |
. . . . . 6
β’
β²π((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ)) |
29 | | fveq2 6885 |
. . . . . . 7
β’ (π = π β ((π β π β¦ (π΅ Β· π΄))βπ) = ((π β π β¦ (π΅ Β· π΄))βπ)) |
30 | 15 | oveq2d 7421 |
. . . . . . 7
β’ (π = π β (π΅ Β· (πΉβπ)) = (π΅ Β· (πΉβπ))) |
31 | 29, 30 | eqeq12d 2742 |
. . . . . 6
β’ (π = π β (((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ)) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ)))) |
32 | 28, 31 | rspc 3594 |
. . . . 5
β’ (π β π β (βπ β π ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ)) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ)))) |
33 | 26, 32 | mpan9 506 |
. . . 4
β’ ((π β§ π β π) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ))) |
34 | 1, 2, 4, 12, 18, 33 | isermulc2 15610 |
. . 3
β’ (π β seqπ( + , (π β π β¦ (π΅ Β· π΄))) β (π΅ Β· Ξ£π β π π΄)) |
35 | 1, 2, 3, 9, 34 | isumclim 15709 |
. 2
β’ (π β Ξ£π β π ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· Ξ£π β π π΄)) |
36 | | sumfc 15661 |
. 2
β’
Ξ£π β
π ((π β π β¦ (π΅ Β· π΄))βπ) = Ξ£π β π (π΅ Β· π΄) |
37 | 35, 36 | eqtr3di 2781 |
1
β’ (π β (π΅ Β· Ξ£π β π π΄) = Ξ£π β π (π΅ Β· π΄)) |