Step | Hyp | Ref
| Expression |
1 | | mbfmulc2re.3 |
. . . . 5
β’ (π β πΉ:π΄βΆβ) |
2 | 1 | fdmd 6684 |
. . . 4
β’ (π β dom πΉ = π΄) |
3 | | mbfmulc2re.1 |
. . . . 5
β’ (π β πΉ β MblFn) |
4 | 3 | dmexd 7847 |
. . . 4
β’ (π β dom πΉ β V) |
5 | 2, 4 | eqeltrrd 2839 |
. . 3
β’ (π β π΄ β V) |
6 | | mbfmulc2re.2 |
. . . 4
β’ (π β π΅ β β) |
7 | 6 | adantr 482 |
. . 3
β’ ((π β§ π₯ β π΄) β π΅ β β) |
8 | 1 | ffvelcdmda 7040 |
. . 3
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β β) |
9 | | fconstmpt 5699 |
. . . 4
β’ (π΄ Γ {π΅}) = (π₯ β π΄ β¦ π΅) |
10 | 9 | a1i 11 |
. . 3
β’ (π β (π΄ Γ {π΅}) = (π₯ β π΄ β¦ π΅)) |
11 | 1 | feqmptd 6915 |
. . 3
β’ (π β πΉ = (π₯ β π΄ β¦ (πΉβπ₯))) |
12 | 5, 7, 8, 10, 11 | offval2 7642 |
. 2
β’ (π β ((π΄ Γ {π΅}) βf Β· πΉ) = (π₯ β π΄ β¦ (π΅ Β· (πΉβπ₯)))) |
13 | 7, 8 | remul2d 15119 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (ββ(π΅ Β· (πΉβπ₯))) = (π΅ Β· (ββ(πΉβπ₯)))) |
14 | 13 | mpteq2dva 5210 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) = (π₯ β π΄ β¦ (π΅ Β· (ββ(πΉβπ₯))))) |
15 | 8 | recld 15086 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (ββ(πΉβπ₯)) β β) |
16 | | eqidd 2738 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (ββ(πΉβπ₯))) = (π₯ β π΄ β¦ (ββ(πΉβπ₯)))) |
17 | 5, 7, 15, 10, 16 | offval2 7642 |
. . . . 5
β’ (π β ((π΄ Γ {π΅}) βf Β· (π₯ β π΄ β¦ (ββ(πΉβπ₯)))) = (π₯ β π΄ β¦ (π΅ Β· (ββ(πΉβπ₯))))) |
18 | 14, 17 | eqtr4d 2780 |
. . . 4
β’ (π β (π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) = ((π΄ Γ {π΅}) βf Β· (π₯ β π΄ β¦ (ββ(πΉβπ₯))))) |
19 | 11, 3 | eqeltrrd 2839 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ (πΉβπ₯)) β MblFn) |
20 | 8 | ismbfcn2 25018 |
. . . . . . 7
β’ (π β ((π₯ β π΄ β¦ (πΉβπ₯)) β MblFn β ((π₯ β π΄ β¦ (ββ(πΉβπ₯))) β MblFn β§ (π₯ β π΄ β¦ (ββ(πΉβπ₯))) β MblFn))) |
21 | 19, 20 | mpbid 231 |
. . . . . 6
β’ (π β ((π₯ β π΄ β¦ (ββ(πΉβπ₯))) β MblFn β§ (π₯ β π΄ β¦ (ββ(πΉβπ₯))) β MblFn)) |
22 | 21 | simpld 496 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββ(πΉβπ₯))) β MblFn) |
23 | 15 | fmpttd 7068 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββ(πΉβπ₯))):π΄βΆβ) |
24 | 22, 6, 23 | mbfmulc2lem 25027 |
. . . 4
β’ (π β ((π΄ Γ {π΅}) βf Β· (π₯ β π΄ β¦ (ββ(πΉβπ₯)))) β MblFn) |
25 | 18, 24 | eqeltrd 2838 |
. . 3
β’ (π β (π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) β MblFn) |
26 | 7, 8 | immul2d 15120 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (ββ(π΅ Β· (πΉβπ₯))) = (π΅ Β· (ββ(πΉβπ₯)))) |
27 | 26 | mpteq2dva 5210 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) = (π₯ β π΄ β¦ (π΅ Β· (ββ(πΉβπ₯))))) |
28 | 8 | imcld 15087 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (ββ(πΉβπ₯)) β β) |
29 | | eqidd 2738 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (ββ(πΉβπ₯))) = (π₯ β π΄ β¦ (ββ(πΉβπ₯)))) |
30 | 5, 7, 28, 10, 29 | offval2 7642 |
. . . . 5
β’ (π β ((π΄ Γ {π΅}) βf Β· (π₯ β π΄ β¦ (ββ(πΉβπ₯)))) = (π₯ β π΄ β¦ (π΅ Β· (ββ(πΉβπ₯))))) |
31 | 27, 30 | eqtr4d 2780 |
. . . 4
β’ (π β (π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) = ((π΄ Γ {π΅}) βf Β· (π₯ β π΄ β¦ (ββ(πΉβπ₯))))) |
32 | 21 | simprd 497 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββ(πΉβπ₯))) β MblFn) |
33 | 28 | fmpttd 7068 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββ(πΉβπ₯))):π΄βΆβ) |
34 | 32, 6, 33 | mbfmulc2lem 25027 |
. . . 4
β’ (π β ((π΄ Γ {π΅}) βf Β· (π₯ β π΄ β¦ (ββ(πΉβπ₯)))) β MblFn) |
35 | 31, 34 | eqeltrd 2838 |
. . 3
β’ (π β (π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) β MblFn) |
36 | 6 | recnd 11190 |
. . . . . 6
β’ (π β π΅ β β) |
37 | 36 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π΄) β π΅ β β) |
38 | 37, 8 | mulcld 11182 |
. . . 4
β’ ((π β§ π₯ β π΄) β (π΅ Β· (πΉβπ₯)) β β) |
39 | 38 | ismbfcn2 25018 |
. . 3
β’ (π β ((π₯ β π΄ β¦ (π΅ Β· (πΉβπ₯))) β MblFn β ((π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) β MblFn β§ (π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) β MblFn))) |
40 | 25, 35, 39 | mpbir2and 712 |
. 2
β’ (π β (π₯ β π΄ β¦ (π΅ Β· (πΉβπ₯))) β MblFn) |
41 | 12, 40 | eqeltrd 2838 |
1
β’ (π β ((π΄ Γ {π΅}) βf Β· πΉ) β MblFn) |