Step | Hyp | Ref
| Expression |
1 | | simp1 1133 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β π΄ β π) |
2 | | simp2 1134 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β πΉ:π΄βΆβ) |
3 | 2 | ffnd 6712 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β πΉ Fn π΄) |
4 | | ax-1cn 11170 |
. . . 4
β’ 1 β
β |
5 | | fnconstg 6773 |
. . . 4
β’ (1 β
β β (π΄ Γ
{1}) Fn π΄) |
6 | 4, 5 | mp1i 13 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β (π΄ Γ {1}) Fn π΄) |
7 | | simp3 1135 |
. . . 4
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β πΊ:π΄βΆ(β β
{0})) |
8 | 7 | ffnd 6712 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β πΊ Fn π΄) |
9 | | inidm 4213 |
. . 3
β’ (π΄ β© π΄) = π΄ |
10 | 6, 8, 1, 1, 9 | offn 7680 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β
((π΄ Γ {1})
βf / πΊ) Fn
π΄) |
11 | 3, 8, 1, 1, 9 | offn 7680 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β (πΉ βf / πΊ) Fn π΄) |
12 | | eqidd 2727 |
. 2
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β§ π₯ β π΄) β (πΉβπ₯) = (πΉβπ₯)) |
13 | | 1cnd 11213 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β 1
β β) |
14 | | eqidd 2727 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β§ π₯ β π΄) β (πΊβπ₯) = (πΊβπ₯)) |
15 | 1, 13, 8, 14 | ofc1 7693 |
. 2
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β§ π₯ β π΄) β (((π΄ Γ {1}) βf / πΊ)βπ₯) = (1 / (πΊβπ₯))) |
16 | | ffvelcdm 7077 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π₯ β π΄) β (πΉβπ₯) β β) |
17 | 2, 16 | sylan 579 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β§ π₯ β π΄) β (πΉβπ₯) β β) |
18 | | ffvelcdm 7077 |
. . . . . 6
β’ ((πΊ:π΄βΆ(β β {0}) β§ π₯ β π΄) β (πΊβπ₯) β (β β
{0})) |
19 | | eldifsn 4785 |
. . . . . 6
β’ ((πΊβπ₯) β (β β {0}) β ((πΊβπ₯) β β β§ (πΊβπ₯) β 0)) |
20 | 18, 19 | sylib 217 |
. . . . 5
β’ ((πΊ:π΄βΆ(β β {0}) β§ π₯ β π΄) β ((πΊβπ₯) β β β§ (πΊβπ₯) β 0)) |
21 | 7, 20 | sylan 579 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β§ π₯ β π΄) β ((πΊβπ₯) β β β§ (πΊβπ₯) β 0)) |
22 | | divrec 11892 |
. . . . . 6
β’ (((πΉβπ₯) β β β§ (πΊβπ₯) β β β§ (πΊβπ₯) β 0) β ((πΉβπ₯) / (πΊβπ₯)) = ((πΉβπ₯) Β· (1 / (πΊβπ₯)))) |
23 | 22 | eqcomd 2732 |
. . . . 5
β’ (((πΉβπ₯) β β β§ (πΊβπ₯) β β β§ (πΊβπ₯) β 0) β ((πΉβπ₯) Β· (1 / (πΊβπ₯))) = ((πΉβπ₯) / (πΊβπ₯))) |
24 | 23 | 3expb 1117 |
. . . 4
β’ (((πΉβπ₯) β β β§ ((πΊβπ₯) β β β§ (πΊβπ₯) β 0)) β ((πΉβπ₯) Β· (1 / (πΊβπ₯))) = ((πΉβπ₯) / (πΊβπ₯))) |
25 | 17, 21, 24 | syl2anc 583 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β§ π₯ β π΄) β ((πΉβπ₯) Β· (1 / (πΊβπ₯))) = ((πΉβπ₯) / (πΊβπ₯))) |
26 | 3, 8, 1, 1, 9, 12,
14 | ofval 7678 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β§ π₯ β π΄) β ((πΉ βf / πΊ)βπ₯) = ((πΉβπ₯) / (πΊβπ₯))) |
27 | 25, 26 | eqtr4d 2769 |
. 2
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β§ π₯ β π΄) β ((πΉβπ₯) Β· (1 / (πΊβπ₯))) = ((πΉ βf / πΊ)βπ₯)) |
28 | 1, 3, 10, 11, 12, 15, 27 | offveq 7691 |
1
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β (πΉ βf Β·
((π΄ Γ {1})
βf / πΊ)) =
(πΉ βf /
πΊ)) |