Step | Hyp | Ref
| Expression |
1 | | mbfmulc2re.3 |
. . . . 5
β’ (π β πΉ:π΄βΆβ) |
2 | 1 | fdmd 6722 |
. . . 4
β’ (π β dom πΉ = π΄) |
3 | | mbfmulc2re.1 |
. . . . 5
β’ (π β πΉ β MblFn) |
4 | 3 | dmexd 7893 |
. . . 4
β’ (π β dom πΉ β V) |
5 | 2, 4 | eqeltrrd 2828 |
. . 3
β’ (π β π΄ β V) |
6 | | mbfmulc2re.2 |
. . . 4
β’ (π β π΅ β β) |
7 | 6 | adantr 480 |
. . 3
β’ ((π β§ π₯ β π΄) β π΅ β β) |
8 | 1 | ffvelcdmda 7080 |
. . 3
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β β) |
9 | | fconstmpt 5731 |
. . . 4
β’ (π΄ Γ {π΅}) = (π₯ β π΄ β¦ π΅) |
10 | 9 | a1i 11 |
. . 3
β’ (π β (π΄ Γ {π΅}) = (π₯ β π΄ β¦ π΅)) |
11 | 1 | feqmptd 6954 |
. . 3
β’ (π β πΉ = (π₯ β π΄ β¦ (πΉβπ₯))) |
12 | 5, 7, 8, 10, 11 | offval2 7687 |
. 2
β’ (π β ((π΄ Γ {π΅}) βf Β· πΉ) = (π₯ β π΄ β¦ (π΅ Β· (πΉβπ₯)))) |
13 | 7, 8 | remul2d 15180 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (ββ(π΅ Β· (πΉβπ₯))) = (π΅ Β· (ββ(πΉβπ₯)))) |
14 | 13 | mpteq2dva 5241 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) = (π₯ β π΄ β¦ (π΅ Β· (ββ(πΉβπ₯))))) |
15 | 8 | recld 15147 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (ββ(πΉβπ₯)) β β) |
16 | | eqidd 2727 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (ββ(πΉβπ₯))) = (π₯ β π΄ β¦ (ββ(πΉβπ₯)))) |
17 | 5, 7, 15, 10, 16 | offval2 7687 |
. . . . 5
β’ (π β ((π΄ Γ {π΅}) βf Β· (π₯ β π΄ β¦ (ββ(πΉβπ₯)))) = (π₯ β π΄ β¦ (π΅ Β· (ββ(πΉβπ₯))))) |
18 | 14, 17 | eqtr4d 2769 |
. . . 4
β’ (π β (π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) = ((π΄ Γ {π΅}) βf Β· (π₯ β π΄ β¦ (ββ(πΉβπ₯))))) |
19 | 11, 3 | eqeltrrd 2828 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ (πΉβπ₯)) β MblFn) |
20 | 8 | ismbfcn2 25522 |
. . . . . . 7
β’ (π β ((π₯ β π΄ β¦ (πΉβπ₯)) β MblFn β ((π₯ β π΄ β¦ (ββ(πΉβπ₯))) β MblFn β§ (π₯ β π΄ β¦ (ββ(πΉβπ₯))) β MblFn))) |
21 | 19, 20 | mpbid 231 |
. . . . . 6
β’ (π β ((π₯ β π΄ β¦ (ββ(πΉβπ₯))) β MblFn β§ (π₯ β π΄ β¦ (ββ(πΉβπ₯))) β MblFn)) |
22 | 21 | simpld 494 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββ(πΉβπ₯))) β MblFn) |
23 | 15 | fmpttd 7110 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββ(πΉβπ₯))):π΄βΆβ) |
24 | 22, 6, 23 | mbfmulc2lem 25531 |
. . . 4
β’ (π β ((π΄ Γ {π΅}) βf Β· (π₯ β π΄ β¦ (ββ(πΉβπ₯)))) β MblFn) |
25 | 18, 24 | eqeltrd 2827 |
. . 3
β’ (π β (π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) β MblFn) |
26 | 7, 8 | immul2d 15181 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (ββ(π΅ Β· (πΉβπ₯))) = (π΅ Β· (ββ(πΉβπ₯)))) |
27 | 26 | mpteq2dva 5241 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) = (π₯ β π΄ β¦ (π΅ Β· (ββ(πΉβπ₯))))) |
28 | 8 | imcld 15148 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (ββ(πΉβπ₯)) β β) |
29 | | eqidd 2727 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (ββ(πΉβπ₯))) = (π₯ β π΄ β¦ (ββ(πΉβπ₯)))) |
30 | 5, 7, 28, 10, 29 | offval2 7687 |
. . . . 5
β’ (π β ((π΄ Γ {π΅}) βf Β· (π₯ β π΄ β¦ (ββ(πΉβπ₯)))) = (π₯ β π΄ β¦ (π΅ Β· (ββ(πΉβπ₯))))) |
31 | 27, 30 | eqtr4d 2769 |
. . . 4
β’ (π β (π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) = ((π΄ Γ {π΅}) βf Β· (π₯ β π΄ β¦ (ββ(πΉβπ₯))))) |
32 | 21 | simprd 495 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββ(πΉβπ₯))) β MblFn) |
33 | 28 | fmpttd 7110 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββ(πΉβπ₯))):π΄βΆβ) |
34 | 32, 6, 33 | mbfmulc2lem 25531 |
. . . 4
β’ (π β ((π΄ Γ {π΅}) βf Β· (π₯ β π΄ β¦ (ββ(πΉβπ₯)))) β MblFn) |
35 | 31, 34 | eqeltrd 2827 |
. . 3
β’ (π β (π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) β MblFn) |
36 | 6 | recnd 11246 |
. . . . . 6
β’ (π β π΅ β β) |
37 | 36 | adantr 480 |
. . . . 5
β’ ((π β§ π₯ β π΄) β π΅ β β) |
38 | 37, 8 | mulcld 11238 |
. . . 4
β’ ((π β§ π₯ β π΄) β (π΅ Β· (πΉβπ₯)) β β) |
39 | 38 | ismbfcn2 25522 |
. . 3
β’ (π β ((π₯ β π΄ β¦ (π΅ Β· (πΉβπ₯))) β MblFn β ((π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) β MblFn β§ (π₯ β π΄ β¦ (ββ(π΅ Β· (πΉβπ₯)))) β MblFn))) |
40 | 25, 35, 39 | mpbir2and 710 |
. 2
β’ (π β (π₯ β π΄ β¦ (π΅ Β· (πΉβπ₯))) β MblFn) |
41 | 12, 40 | eqeltrd 2827 |
1
β’ (π β ((π΄ Γ {π΅}) βf Β· πΉ) β MblFn) |