Step | Hyp | Ref
| Expression |
1 | | simpll 765 |
. 2
β’ (((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β π΄ β π) |
2 | | simplr 767 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β πΉ:π΄βΆβ) |
3 | 2 | ffnd 6631 |
. 2
β’ (((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β πΉ Fn π΄) |
4 | | simprl 769 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β πΊ:π΄βΆ(β β
{0})) |
5 | 4 | ffnd 6631 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β πΊ Fn π΄) |
6 | | simprr 771 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β π»:π΄βΆ(β β
{0})) |
7 | 6 | ffnd 6631 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β π» Fn π΄) |
8 | | inidm 4158 |
. . 3
β’ (π΄ β© π΄) = π΄ |
9 | 5, 7, 1, 1, 8 | offn 7578 |
. 2
β’ (((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β
(πΊ βf /
π») Fn π΄) |
10 | 3, 7, 1, 1, 8 | offn 7578 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β
(πΉ βf
Β· π») Fn π΄) |
11 | 10, 5, 1, 1, 8 | offn 7578 |
. 2
β’ (((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β
((πΉ βf
Β· π»)
βf / πΊ) Fn
π΄) |
12 | | eqidd 2737 |
. 2
β’ ((((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β§ π₯ β π΄) β (πΉβπ₯) = (πΉβπ₯)) |
13 | | eqidd 2737 |
. 2
β’ ((((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β§ π₯ β π΄) β ((πΊ βf / π»)βπ₯) = ((πΊ βf / π»)βπ₯)) |
14 | | ffvelcdm 6991 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π₯ β π΄) β (πΉβπ₯) β β) |
15 | 2, 14 | sylan 581 |
. . . 4
β’ ((((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β§ π₯ β π΄) β (πΉβπ₯) β β) |
16 | | ffvelcdm 6991 |
. . . . . 6
β’ ((πΊ:π΄βΆ(β β {0}) β§ π₯ β π΄) β (πΊβπ₯) β (β β
{0})) |
17 | | eldifsn 4726 |
. . . . . 6
β’ ((πΊβπ₯) β (β β {0}) β ((πΊβπ₯) β β β§ (πΊβπ₯) β 0)) |
18 | 16, 17 | sylib 217 |
. . . . 5
β’ ((πΊ:π΄βΆ(β β {0}) β§ π₯ β π΄) β ((πΊβπ₯) β β β§ (πΊβπ₯) β 0)) |
19 | 4, 18 | sylan 581 |
. . . 4
β’ ((((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β§ π₯ β π΄) β ((πΊβπ₯) β β β§ (πΊβπ₯) β 0)) |
20 | | ffvelcdm 6991 |
. . . . . 6
β’ ((π»:π΄βΆ(β β {0}) β§ π₯ β π΄) β (π»βπ₯) β (β β
{0})) |
21 | | eldifsn 4726 |
. . . . . 6
β’ ((π»βπ₯) β (β β {0}) β ((π»βπ₯) β β β§ (π»βπ₯) β 0)) |
22 | 20, 21 | sylib 217 |
. . . . 5
β’ ((π»:π΄βΆ(β β {0}) β§ π₯ β π΄) β ((π»βπ₯) β β β§ (π»βπ₯) β 0)) |
23 | 6, 22 | sylan 581 |
. . . 4
β’ ((((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β§ π₯ β π΄) β ((π»βπ₯) β β β§ (π»βπ₯) β 0)) |
24 | | divdiv2 11733 |
. . . 4
β’ (((πΉβπ₯) β β β§ ((πΊβπ₯) β β β§ (πΊβπ₯) β 0) β§ ((π»βπ₯) β β β§ (π»βπ₯) β 0)) β ((πΉβπ₯) / ((πΊβπ₯) / (π»βπ₯))) = (((πΉβπ₯) Β· (π»βπ₯)) / (πΊβπ₯))) |
25 | 15, 19, 23, 24 | syl3anc 1371 |
. . 3
β’ ((((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β§ π₯ β π΄) β ((πΉβπ₯) / ((πΊβπ₯) / (π»βπ₯))) = (((πΉβπ₯) Β· (π»βπ₯)) / (πΊβπ₯))) |
26 | | eqidd 2737 |
. . . . 5
β’ ((((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β§ π₯ β π΄) β (πΊβπ₯) = (πΊβπ₯)) |
27 | | eqidd 2737 |
. . . . 5
β’ ((((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β§ π₯ β π΄) β (π»βπ₯) = (π»βπ₯)) |
28 | 5, 7, 1, 1, 8, 26,
27 | ofval 7576 |
. . . 4
β’ ((((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β§ π₯ β π΄) β ((πΊ βf / π»)βπ₯) = ((πΊβπ₯) / (π»βπ₯))) |
29 | 28 | oveq2d 7323 |
. . 3
β’ ((((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β§ π₯ β π΄) β ((πΉβπ₯) / ((πΊ βf / π»)βπ₯)) = ((πΉβπ₯) / ((πΊβπ₯) / (π»βπ₯)))) |
30 | 3, 7, 1, 1, 8, 12,
27 | ofval 7576 |
. . . 4
β’ ((((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β§ π₯ β π΄) β ((πΉ βf Β· π»)βπ₯) = ((πΉβπ₯) Β· (π»βπ₯))) |
31 | 10, 5, 1, 1, 8, 30,
26 | ofval 7576 |
. . 3
β’ ((((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β§ π₯ β π΄) β (((πΉ βf Β· π») βf / πΊ)βπ₯) = (((πΉβπ₯) Β· (π»βπ₯)) / (πΊβπ₯))) |
32 | 25, 29, 31 | 3eqtr4d 2786 |
. 2
β’ ((((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β§ π₯ β π΄) β ((πΉβπ₯) / ((πΊ βf / π»)βπ₯)) = (((πΉ βf Β· π») βf / πΊ)βπ₯)) |
33 | 1, 3, 9, 11, 12, 13, 32 | offveq 7589 |
1
β’ (((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β
(πΉ βf /
(πΊ βf /
π»)) = ((πΉ βf Β· π») βf / πΊ)) |