Step | Hyp | Ref
| Expression |
1 | | mbfmul.1 |
. . 3
β’ (π β πΉ β MblFn) |
2 | | mbfmul.3 |
. . 3
β’ (π β πΉ:π΄βΆβ) |
3 | 1, 2 | mbfi1flim 25104 |
. 2
β’ (π β βπ(π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦))) |
4 | | mbfmul.2 |
. . 3
β’ (π β πΊ β MblFn) |
5 | | mbfmul.4 |
. . 3
β’ (π β πΊ:π΄βΆβ) |
6 | 4, 5 | mbfi1flim 25104 |
. 2
β’ (π β βπ(π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦))) |
7 | | exdistrv 1960 |
. . 3
β’
(βπβπ((π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ (π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦))) β (βπ(π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ βπ(π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦)))) |
8 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ ((π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ (π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦)))) β πΉ β MblFn) |
9 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ ((π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ (π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦)))) β πΊ β MblFn) |
10 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ ((π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ (π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦)))) β πΉ:π΄βΆβ) |
11 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ ((π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ (π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦)))) β πΊ:π΄βΆβ) |
12 | | simprll 778 |
. . . . . 6
β’ ((π β§ ((π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ (π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦)))) β π:ββΆdom
β«1) |
13 | | simprlr 779 |
. . . . . . 7
β’ ((π β§ ((π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ (π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦)))) β βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) |
14 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β ((πβπ)βπ¦) = ((πβπ)βπ₯)) |
15 | 14 | mpteq2dv 5208 |
. . . . . . . . . 10
β’ (π¦ = π₯ β (π β β β¦ ((πβπ)βπ¦)) = (π β β β¦ ((πβπ)βπ₯))) |
16 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = π β (πβπ) = (πβπ)) |
17 | 16 | fveq1d 6845 |
. . . . . . . . . . 11
β’ (π = π β ((πβπ)βπ₯) = ((πβπ)βπ₯)) |
18 | 17 | cbvmptv 5219 |
. . . . . . . . . 10
β’ (π β β β¦ ((πβπ)βπ₯)) = (π β β β¦ ((πβπ)βπ₯)) |
19 | 15, 18 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π¦ = π₯ β (π β β β¦ ((πβπ)βπ¦)) = (π β β β¦ ((πβπ)βπ₯))) |
20 | | fveq2 6843 |
. . . . . . . . 9
β’ (π¦ = π₯ β (πΉβπ¦) = (πΉβπ₯)) |
21 | 19, 20 | breq12d 5119 |
. . . . . . . 8
β’ (π¦ = π₯ β ((π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦) β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯))) |
22 | 21 | rspccva 3579 |
. . . . . . 7
β’
((βπ¦ β
π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦) β§ π₯ β π΄) β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)) |
23 | 13, 22 | sylan 581 |
. . . . . 6
β’ (((π β§ ((π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ (π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦)))) β§ π₯ β π΄) β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)) |
24 | | simprrl 780 |
. . . . . 6
β’ ((π β§ ((π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ (π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦)))) β π:ββΆdom
β«1) |
25 | | simprrr 781 |
. . . . . . 7
β’ ((π β§ ((π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ (π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦)))) β βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦)) |
26 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β ((πβπ)βπ¦) = ((πβπ)βπ₯)) |
27 | 26 | mpteq2dv 5208 |
. . . . . . . . . 10
β’ (π¦ = π₯ β (π β β β¦ ((πβπ)βπ¦)) = (π β β β¦ ((πβπ)βπ₯))) |
28 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = π β (πβπ) = (πβπ)) |
29 | 28 | fveq1d 6845 |
. . . . . . . . . . 11
β’ (π = π β ((πβπ)βπ₯) = ((πβπ)βπ₯)) |
30 | 29 | cbvmptv 5219 |
. . . . . . . . . 10
β’ (π β β β¦ ((πβπ)βπ₯)) = (π β β β¦ ((πβπ)βπ₯)) |
31 | 27, 30 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π¦ = π₯ β (π β β β¦ ((πβπ)βπ¦)) = (π β β β¦ ((πβπ)βπ₯))) |
32 | | fveq2 6843 |
. . . . . . . . 9
β’ (π¦ = π₯ β (πΊβπ¦) = (πΊβπ₯)) |
33 | 31, 32 | breq12d 5119 |
. . . . . . . 8
β’ (π¦ = π₯ β ((π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦) β (π β β β¦ ((πβπ)βπ₯)) β (πΊβπ₯))) |
34 | 33 | rspccva 3579 |
. . . . . . 7
β’
((βπ¦ β
π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦) β§ π₯ β π΄) β (π β β β¦ ((πβπ)βπ₯)) β (πΊβπ₯)) |
35 | 25, 34 | sylan 581 |
. . . . . 6
β’ (((π β§ ((π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ (π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦)))) β§ π₯ β π΄) β (π β β β¦ ((πβπ)βπ₯)) β (πΊβπ₯)) |
36 | 8, 9, 10, 11, 12, 23, 24, 35 | mbfmullem2 25105 |
. . . . 5
β’ ((π β§ ((π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ (π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦)))) β (πΉ βf Β· πΊ) β MblFn) |
37 | 36 | ex 414 |
. . . 4
β’ (π β (((π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ (π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦))) β (πΉ βf Β· πΊ) β
MblFn)) |
38 | 37 | exlimdvv 1938 |
. . 3
β’ (π β (βπβπ((π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ (π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦))) β (πΉ βf Β· πΊ) β
MblFn)) |
39 | 7, 38 | biimtrrid 242 |
. 2
β’ (π β ((βπ(π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β§ βπ(π:ββΆdom β«1 β§
βπ¦ β π΄ (π β β β¦ ((πβπ)βπ¦)) β (πΊβπ¦))) β (πΉ βf Β· πΊ) β
MblFn)) |
40 | 3, 6, 39 | mp2and 698 |
1
β’ (π β (πΉ βf Β· πΊ) β MblFn) |