Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . 4
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β πΉ β π΄) |
2 | | simpr1 1195 |
. . . 4
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β π β π΅) |
3 | | simpll 766 |
. . . . 5
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β π
β
DivRing) |
4 | | simpr2 1196 |
. . . . 5
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β π β π΅) |
5 | | simpr3 1197 |
. . . . 5
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β π β 0 ) |
6 | | abvneg.b |
. . . . . 6
β’ π΅ = (Baseβπ
) |
7 | | abvrec.z |
. . . . . 6
β’ 0 =
(0gβπ
) |
8 | | eqid 2733 |
. . . . . 6
β’
(invrβπ
) = (invrβπ
) |
9 | 6, 7, 8 | drnginvrcl 20379 |
. . . . 5
β’ ((π
β DivRing β§ π β π΅ β§ π β 0 ) β
((invrβπ
)βπ) β π΅) |
10 | 3, 4, 5, 9 | syl3anc 1372 |
. . . 4
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β
((invrβπ
)βπ) β π΅) |
11 | | abv0.a |
. . . . 5
β’ π΄ = (AbsValβπ
) |
12 | | eqid 2733 |
. . . . 5
β’
(.rβπ
) = (.rβπ
) |
13 | 11, 6, 12 | abvmul 20437 |
. . . 4
β’ ((πΉ β π΄ β§ π β π΅ β§ ((invrβπ
)βπ) β π΅) β (πΉβ(π(.rβπ
)((invrβπ
)βπ))) = ((πΉβπ) Β· (πΉβ((invrβπ
)βπ)))) |
14 | 1, 2, 10, 13 | syl3anc 1372 |
. . 3
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β (πΉβ(π(.rβπ
)((invrβπ
)βπ))) = ((πΉβπ) Β· (πΉβ((invrβπ
)βπ)))) |
15 | 11, 6, 7, 8 | abvrec 20444 |
. . . . 5
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β 0 )) β (πΉβ((invrβπ
)βπ)) = (1 / (πΉβπ))) |
16 | 15 | 3adantr1 1170 |
. . . 4
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β (πΉβ((invrβπ
)βπ)) = (1 / (πΉβπ))) |
17 | 16 | oveq2d 7425 |
. . 3
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β ((πΉβπ) Β· (πΉβ((invrβπ
)βπ))) = ((πΉβπ) Β· (1 / (πΉβπ)))) |
18 | 14, 17 | eqtrd 2773 |
. 2
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β (πΉβ(π(.rβπ
)((invrβπ
)βπ))) = ((πΉβπ) Β· (1 / (πΉβπ)))) |
19 | | eqid 2733 |
. . . . . . 7
β’
(Unitβπ
) =
(Unitβπ
) |
20 | 6, 19, 7 | drngunit 20362 |
. . . . . 6
β’ (π
β DivRing β (π β (Unitβπ
) β (π β π΅ β§ π β 0 ))) |
21 | 3, 20 | syl 17 |
. . . . 5
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β (π β (Unitβπ
) β (π β π΅ β§ π β 0 ))) |
22 | 4, 5, 21 | mpbir2and 712 |
. . . 4
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β π β (Unitβπ
)) |
23 | | abvdiv.p |
. . . . 5
β’ / =
(/rβπ
) |
24 | 6, 12, 19, 8, 23 | dvrval 20217 |
. . . 4
β’ ((π β π΅ β§ π β (Unitβπ
)) β (π / π) = (π(.rβπ
)((invrβπ
)βπ))) |
25 | 2, 22, 24 | syl2anc 585 |
. . 3
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β (π / π) = (π(.rβπ
)((invrβπ
)βπ))) |
26 | 25 | fveq2d 6896 |
. 2
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β (πΉβ(π / π)) = (πΉβ(π(.rβπ
)((invrβπ
)βπ)))) |
27 | 11, 6 | abvcl 20432 |
. . . . 5
β’ ((πΉ β π΄ β§ π β π΅) β (πΉβπ) β β) |
28 | 1, 2, 27 | syl2anc 585 |
. . . 4
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β (πΉβπ) β β) |
29 | 28 | recnd 11242 |
. . 3
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β (πΉβπ) β β) |
30 | 11, 6 | abvcl 20432 |
. . . . 5
β’ ((πΉ β π΄ β§ π β π΅) β (πΉβπ) β β) |
31 | 1, 4, 30 | syl2anc 585 |
. . . 4
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β (πΉβπ) β β) |
32 | 31 | recnd 11242 |
. . 3
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β (πΉβπ) β β) |
33 | 11, 6, 7 | abvne0 20435 |
. . . 4
β’ ((πΉ β π΄ β§ π β π΅ β§ π β 0 ) β (πΉβπ) β 0) |
34 | 1, 4, 5, 33 | syl3anc 1372 |
. . 3
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β (πΉβπ) β 0) |
35 | 29, 32, 34 | divrecd 11993 |
. 2
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β ((πΉβπ) / (πΉβπ)) = ((πΉβπ) Β· (1 / (πΉβπ)))) |
36 | 18, 26, 35 | 3eqtr4d 2783 |
1
β’ (((π
β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β (πΉβ(π / π)) = ((πΉβπ) / (πΉβπ))) |