Step | Hyp | Ref
| Expression |
1 | | isumcl.1 |
. . 3
β’ π =
(β€β₯βπ) |
2 | | isumcl.2 |
. . 3
β’ (π β π β β€) |
3 | | eqidd 2726 |
. . 3
β’ ((π β§ π β π) β ((π β π β¦ (π΅ Β· π΄))βπ) = ((π β π β¦ (π΅ Β· π΄))βπ)) |
4 | | summulc.6 |
. . . . . . 7
β’ (π β π΅ β β) |
5 | 4 | adantr 479 |
. . . . . 6
β’ ((π β§ π β π) β π΅ β β) |
6 | | isumcl.4 |
. . . . . 6
β’ ((π β§ π β π) β π΄ β β) |
7 | 5, 6 | mulcld 11262 |
. . . . 5
β’ ((π β§ π β π) β (π΅ Β· π΄) β β) |
8 | 7 | fmpttd 7118 |
. . . 4
β’ (π β (π β π β¦ (π΅ Β· π΄)):πβΆβ) |
9 | 8 | ffvelcdmda 7087 |
. . 3
β’ ((π β§ π β π) β ((π β π β¦ (π΅ Β· π΄))βπ) β β) |
10 | | isumcl.3 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) = π΄) |
11 | | isumcl.5 |
. . . . 5
β’ (π β seqπ( + , πΉ) β dom β ) |
12 | 1, 2, 10, 6, 11 | isumclim2 15734 |
. . . 4
β’ (π β seqπ( + , πΉ) β Ξ£π β π π΄) |
13 | 10, 6 | eqeltrd 2825 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β β) |
14 | 13 | ralrimiva 3136 |
. . . . 5
β’ (π β βπ β π (πΉβπ) β β) |
15 | | fveq2 6890 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
16 | 15 | eleq1d 2810 |
. . . . . 6
β’ (π = π β ((πΉβπ) β β β (πΉβπ) β β)) |
17 | 16 | rspccva 3600 |
. . . . 5
β’
((βπ β
π (πΉβπ) β β β§ π β π) β (πΉβπ) β β) |
18 | 14, 17 | sylan 578 |
. . . 4
β’ ((π β§ π β π) β (πΉβπ) β β) |
19 | | simpr 483 |
. . . . . . . 8
β’ ((π β§ π β π) β π β π) |
20 | | ovex 7447 |
. . . . . . . 8
β’ (π΅ Β· π΄) β V |
21 | | eqid 2725 |
. . . . . . . . 9
β’ (π β π β¦ (π΅ Β· π΄)) = (π β π β¦ (π΅ Β· π΄)) |
22 | 21 | fvmpt2 7009 |
. . . . . . . 8
β’ ((π β π β§ (π΅ Β· π΄) β V) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· π΄)) |
23 | 19, 20, 22 | sylancl 584 |
. . . . . . 7
β’ ((π β§ π β π) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· π΄)) |
24 | 10 | oveq2d 7430 |
. . . . . . 7
β’ ((π β§ π β π) β (π΅ Β· (πΉβπ)) = (π΅ Β· π΄)) |
25 | 23, 24 | eqtr4d 2768 |
. . . . . 6
β’ ((π β§ π β π) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ))) |
26 | 25 | ralrimiva 3136 |
. . . . 5
β’ (π β βπ β π ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ))) |
27 | | nffvmpt1 6901 |
. . . . . . 7
β’
β²π((π β π β¦ (π΅ Β· π΄))βπ) |
28 | 27 | nfeq1 2908 |
. . . . . 6
β’
β²π((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ)) |
29 | | fveq2 6890 |
. . . . . . 7
β’ (π = π β ((π β π β¦ (π΅ Β· π΄))βπ) = ((π β π β¦ (π΅ Β· π΄))βπ)) |
30 | 15 | oveq2d 7430 |
. . . . . . 7
β’ (π = π β (π΅ Β· (πΉβπ)) = (π΅ Β· (πΉβπ))) |
31 | 29, 30 | eqeq12d 2741 |
. . . . . 6
β’ (π = π β (((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ)) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ)))) |
32 | 28, 31 | rspc 3589 |
. . . . 5
β’ (π β π β (βπ β π ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ)) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ)))) |
33 | 26, 32 | mpan9 505 |
. . . 4
β’ ((π β§ π β π) β ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· (πΉβπ))) |
34 | 1, 2, 4, 12, 18, 33 | isermulc2 15634 |
. . 3
β’ (π β seqπ( + , (π β π β¦ (π΅ Β· π΄))) β (π΅ Β· Ξ£π β π π΄)) |
35 | 1, 2, 3, 9, 34 | isumclim 15733 |
. 2
β’ (π β Ξ£π β π ((π β π β¦ (π΅ Β· π΄))βπ) = (π΅ Β· Ξ£π β π π΄)) |
36 | | sumfc 15685 |
. 2
β’
Ξ£π β
π ((π β π β¦ (π΅ Β· π΄))βπ) = Ξ£π β π (π΅ Β· π΄) |
37 | 35, 36 | eqtr3di 2780 |
1
β’ (π β (π΅ Β· Ξ£π β π π΄) = Ξ£π β π (π΅ Β· π΄)) |