Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β π΄ β π) |
2 | | simp2 1138 |
. . . 4
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β πΉ:π΄βΆβ) |
3 | 2 | ffnd 6719 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β πΉ Fn π΄) |
4 | | simp3 1139 |
. . . 4
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β πΊ:π΄βΆ(β β
{0})) |
5 | 4 | ffnd 6719 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β πΊ Fn π΄) |
6 | | inidm 4219 |
. . 3
β’ (π΄ β© π΄) = π΄ |
7 | 3, 5, 1, 1, 6 | offn 7683 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β (πΉ βf Β·
πΊ) Fn π΄) |
8 | | eqidd 2734 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β§ π₯ β π΄) β (πΉβπ₯) = (πΉβπ₯)) |
9 | | eqidd 2734 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β§ π₯ β π΄) β (πΊβπ₯) = (πΊβπ₯)) |
10 | 3, 5, 1, 1, 6, 8, 9 | ofval 7681 |
. 2
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β§ π₯ β π΄) β ((πΉ βf Β· πΊ)βπ₯) = ((πΉβπ₯) Β· (πΊβπ₯))) |
11 | | ffvelcdm 7084 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ π₯ β π΄) β (πΉβπ₯) β β) |
12 | 2, 11 | sylan 581 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β§ π₯ β π΄) β (πΉβπ₯) β β) |
13 | | ffvelcdm 7084 |
. . . . 5
β’ ((πΊ:π΄βΆ(β β {0}) β§ π₯ β π΄) β (πΊβπ₯) β (β β
{0})) |
14 | | eldifsn 4791 |
. . . . 5
β’ ((πΊβπ₯) β (β β {0}) β ((πΊβπ₯) β β β§ (πΊβπ₯) β 0)) |
15 | 13, 14 | sylib 217 |
. . . 4
β’ ((πΊ:π΄βΆ(β β {0}) β§ π₯ β π΄) β ((πΊβπ₯) β β β§ (πΊβπ₯) β 0)) |
16 | 4, 15 | sylan 581 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β§ π₯ β π΄) β ((πΊβπ₯) β β β§ (πΊβπ₯) β 0)) |
17 | | divcan4 11899 |
. . . 4
β’ (((πΉβπ₯) β β β§ (πΊβπ₯) β β β§ (πΊβπ₯) β 0) β (((πΉβπ₯) Β· (πΊβπ₯)) / (πΊβπ₯)) = (πΉβπ₯)) |
18 | 17 | 3expb 1121 |
. . 3
β’ (((πΉβπ₯) β β β§ ((πΊβπ₯) β β β§ (πΊβπ₯) β 0)) β (((πΉβπ₯) Β· (πΊβπ₯)) / (πΊβπ₯)) = (πΉβπ₯)) |
19 | 12, 16, 18 | syl2anc 585 |
. 2
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β§ π₯ β π΄) β (((πΉβπ₯) Β· (πΊβπ₯)) / (πΊβπ₯)) = (πΉβπ₯)) |
20 | 1, 7, 5, 3, 10, 9,
19 | offveq 7694 |
1
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β
((πΉ βf
Β· πΊ)
βf / πΊ) =
πΉ) |