Step | Hyp | Ref
| Expression |
1 | | abv0.a |
. . . . . . 7
β’ π΄ = (AbsValβπ
) |
2 | 1 | abvrcl 20323 |
. . . . . 6
β’ (πΉ β π΄ β π
β Ring) |
3 | 2 | adantr 482 |
. . . . 5
β’ ((πΉ β π΄ β§ π β π΅) β π
β Ring) |
4 | | ringgrp 19977 |
. . . . . . 7
β’ (π
β Ring β π
β Grp) |
5 | 2, 4 | syl 17 |
. . . . . 6
β’ (πΉ β π΄ β π
β Grp) |
6 | | abvneg.b |
. . . . . . 7
β’ π΅ = (Baseβπ
) |
7 | | abvneg.p |
. . . . . . 7
β’ π = (invgβπ
) |
8 | 6, 7 | grpinvcl 18806 |
. . . . . 6
β’ ((π
β Grp β§ π β π΅) β (πβπ) β π΅) |
9 | 5, 8 | sylan 581 |
. . . . 5
β’ ((πΉ β π΄ β§ π β π΅) β (πβπ) β π΅) |
10 | | simpr 486 |
. . . . 5
β’ ((πΉ β π΄ β§ π β π΅) β π β π΅) |
11 | | eqid 2733 |
. . . . . 6
β’
(1rβπ
) = (1rβπ
) |
12 | | eqid 2733 |
. . . . . 6
β’
(0gβπ
) = (0gβπ
) |
13 | 6, 11, 12 | ring1eq0 20022 |
. . . . 5
β’ ((π
β Ring β§ (πβπ) β π΅ β§ π β π΅) β ((1rβπ
) = (0gβπ
) β (πβπ) = π)) |
14 | 3, 9, 10, 13 | syl3anc 1372 |
. . . 4
β’ ((πΉ β π΄ β§ π β π΅) β ((1rβπ
) = (0gβπ
) β (πβπ) = π)) |
15 | 14 | imp 408 |
. . 3
β’ (((πΉ β π΄ β§ π β π΅) β§ (1rβπ
) = (0gβπ
)) β (πβπ) = π) |
16 | 15 | fveq2d 6850 |
. 2
β’ (((πΉ β π΄ β§ π β π΅) β§ (1rβπ
) = (0gβπ
)) β (πΉβ(πβπ)) = (πΉβπ)) |
17 | 6, 11 | ringidcl 19997 |
. . . . . . . . . . . . . . . 16
β’ (π
β Ring β
(1rβπ
)
β π΅) |
18 | 2, 17 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (πΉ β π΄ β (1rβπ
) β π΅) |
19 | 6, 7 | grpinvcl 18806 |
. . . . . . . . . . . . . . 15
β’ ((π
β Grp β§
(1rβπ
)
β π΅) β (πβ(1rβπ
)) β π΅) |
20 | 5, 18, 19 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (πΉ β π΄ β (πβ(1rβπ
)) β π΅) |
21 | 1, 6 | abvcl 20326 |
. . . . . . . . . . . . . 14
β’ ((πΉ β π΄ β§ (πβ(1rβπ
)) β π΅) β (πΉβ(πβ(1rβπ
))) β
β) |
22 | 20, 21 | mpdan 686 |
. . . . . . . . . . . . 13
β’ (πΉ β π΄ β (πΉβ(πβ(1rβπ
))) β
β) |
23 | 22 | recnd 11191 |
. . . . . . . . . . . 12
β’ (πΉ β π΄ β (πΉβ(πβ(1rβπ
))) β
β) |
24 | 23 | sqvald 14057 |
. . . . . . . . . . 11
β’ (πΉ β π΄ β ((πΉβ(πβ(1rβπ
)))β2) = ((πΉβ(πβ(1rβπ
))) Β· (πΉβ(πβ(1rβπ
))))) |
25 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(.rβπ
) = (.rβπ
) |
26 | 1, 6, 25 | abvmul 20331 |
. . . . . . . . . . . 12
β’ ((πΉ β π΄ β§ (πβ(1rβπ
)) β π΅ β§ (πβ(1rβπ
)) β π΅) β (πΉβ((πβ(1rβπ
))(.rβπ
)(πβ(1rβπ
)))) = ((πΉβ(πβ(1rβπ
))) Β· (πΉβ(πβ(1rβπ
))))) |
27 | 20, 20, 26 | mpd3an23 1464 |
. . . . . . . . . . 11
β’ (πΉ β π΄ β (πΉβ((πβ(1rβπ
))(.rβπ
)(πβ(1rβπ
)))) = ((πΉβ(πβ(1rβπ
))) Β· (πΉβ(πβ(1rβπ
))))) |
28 | 6, 25, 7, 2, 20, 18 | ringmneg2 20029 |
. . . . . . . . . . . . 13
β’ (πΉ β π΄ β ((πβ(1rβπ
))(.rβπ
)(πβ(1rβπ
))) = (πβ((πβ(1rβπ
))(.rβπ
)(1rβπ
)))) |
29 | 6, 25, 11, 7, 2, 18 | ringnegl 20026 |
. . . . . . . . . . . . . 14
β’ (πΉ β π΄ β ((πβ(1rβπ
))(.rβπ
)(1rβπ
)) = (πβ(1rβπ
))) |
30 | 29 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (πΉ β π΄ β (πβ((πβ(1rβπ
))(.rβπ
)(1rβπ
))) = (πβ(πβ(1rβπ
)))) |
31 | 6, 7 | grpinvinv 18822 |
. . . . . . . . . . . . . 14
β’ ((π
β Grp β§
(1rβπ
)
β π΅) β (πβ(πβ(1rβπ
))) = (1rβπ
)) |
32 | 5, 18, 31 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (πΉ β π΄ β (πβ(πβ(1rβπ
))) = (1rβπ
)) |
33 | 28, 30, 32 | 3eqtrd 2777 |
. . . . . . . . . . . 12
β’ (πΉ β π΄ β ((πβ(1rβπ
))(.rβπ
)(πβ(1rβπ
))) = (1rβπ
)) |
34 | 33 | fveq2d 6850 |
. . . . . . . . . . 11
β’ (πΉ β π΄ β (πΉβ((πβ(1rβπ
))(.rβπ
)(πβ(1rβπ
)))) = (πΉβ(1rβπ
))) |
35 | 24, 27, 34 | 3eqtr2d 2779 |
. . . . . . . . . 10
β’ (πΉ β π΄ β ((πΉβ(πβ(1rβπ
)))β2) = (πΉβ(1rβπ
))) |
36 | 35 | adantr 482 |
. . . . . . . . 9
β’ ((πΉ β π΄ β§ (1rβπ
) β
(0gβπ
))
β ((πΉβ(πβ(1rβπ
)))β2) = (πΉβ(1rβπ
))) |
37 | 1, 11, 12 | abv1z 20334 |
. . . . . . . . 9
β’ ((πΉ β π΄ β§ (1rβπ
) β
(0gβπ
))
β (πΉβ(1rβπ
)) = 1) |
38 | 36, 37 | eqtrd 2773 |
. . . . . . . 8
β’ ((πΉ β π΄ β§ (1rβπ
) β
(0gβπ
))
β ((πΉβ(πβ(1rβπ
)))β2) =
1) |
39 | | sq1 14108 |
. . . . . . . 8
β’
(1β2) = 1 |
40 | 38, 39 | eqtr4di 2791 |
. . . . . . 7
β’ ((πΉ β π΄ β§ (1rβπ
) β
(0gβπ
))
β ((πΉβ(πβ(1rβπ
)))β2) =
(1β2)) |
41 | 1, 6 | abvge0 20327 |
. . . . . . . . . 10
β’ ((πΉ β π΄ β§ (πβ(1rβπ
)) β π΅) β 0 β€ (πΉβ(πβ(1rβπ
)))) |
42 | 20, 41 | mpdan 686 |
. . . . . . . . 9
β’ (πΉ β π΄ β 0 β€ (πΉβ(πβ(1rβπ
)))) |
43 | | 1re 11163 |
. . . . . . . . . 10
β’ 1 β
β |
44 | | 0le1 11686 |
. . . . . . . . . 10
β’ 0 β€
1 |
45 | | sq11 14045 |
. . . . . . . . . 10
β’ ((((πΉβ(πβ(1rβπ
))) β β β§ 0 β€
(πΉβ(πβ(1rβπ
)))) β§ (1 β β
β§ 0 β€ 1)) β (((πΉβ(πβ(1rβπ
)))β2) = (1β2) β
(πΉβ(πβ(1rβπ
))) = 1)) |
46 | 43, 44, 45 | mpanr12 704 |
. . . . . . . . 9
β’ (((πΉβ(πβ(1rβπ
))) β β β§ 0 β€
(πΉβ(πβ(1rβπ
)))) β (((πΉβ(πβ(1rβπ
)))β2) = (1β2) β
(πΉβ(πβ(1rβπ
))) = 1)) |
47 | 22, 42, 46 | syl2anc 585 |
. . . . . . . 8
β’ (πΉ β π΄ β (((πΉβ(πβ(1rβπ
)))β2) = (1β2) β
(πΉβ(πβ(1rβπ
))) = 1)) |
48 | 47 | biimpa 478 |
. . . . . . 7
β’ ((πΉ β π΄ β§ ((πΉβ(πβ(1rβπ
)))β2) = (1β2)) β
(πΉβ(πβ(1rβπ
))) = 1) |
49 | 40, 48 | syldan 592 |
. . . . . 6
β’ ((πΉ β π΄ β§ (1rβπ
) β
(0gβπ
))
β (πΉβ(πβ(1rβπ
))) = 1) |
50 | 49 | adantlr 714 |
. . . . 5
β’ (((πΉ β π΄ β§ π β π΅) β§ (1rβπ
) β
(0gβπ
))
β (πΉβ(πβ(1rβπ
))) = 1) |
51 | 50 | oveq1d 7376 |
. . . 4
β’ (((πΉ β π΄ β§ π β π΅) β§ (1rβπ
) β
(0gβπ
))
β ((πΉβ(πβ(1rβπ
))) Β· (πΉβπ)) = (1 Β· (πΉβπ))) |
52 | | simpl 484 |
. . . . . . 7
β’ ((πΉ β π΄ β§ π β π΅) β πΉ β π΄) |
53 | 20 | adantr 482 |
. . . . . . 7
β’ ((πΉ β π΄ β§ π β π΅) β (πβ(1rβπ
)) β π΅) |
54 | 1, 6, 25 | abvmul 20331 |
. . . . . . 7
β’ ((πΉ β π΄ β§ (πβ(1rβπ
)) β π΅ β§ π β π΅) β (πΉβ((πβ(1rβπ
))(.rβπ
)π)) = ((πΉβ(πβ(1rβπ
))) Β· (πΉβπ))) |
55 | 52, 53, 10, 54 | syl3anc 1372 |
. . . . . 6
β’ ((πΉ β π΄ β§ π β π΅) β (πΉβ((πβ(1rβπ
))(.rβπ
)π)) = ((πΉβ(πβ(1rβπ
))) Β· (πΉβπ))) |
56 | 6, 25, 11, 7, 3, 10 | ringnegl 20026 |
. . . . . . 7
β’ ((πΉ β π΄ β§ π β π΅) β ((πβ(1rβπ
))(.rβπ
)π) = (πβπ)) |
57 | 56 | fveq2d 6850 |
. . . . . 6
β’ ((πΉ β π΄ β§ π β π΅) β (πΉβ((πβ(1rβπ
))(.rβπ
)π)) = (πΉβ(πβπ))) |
58 | 55, 57 | eqtr3d 2775 |
. . . . 5
β’ ((πΉ β π΄ β§ π β π΅) β ((πΉβ(πβ(1rβπ
))) Β· (πΉβπ)) = (πΉβ(πβπ))) |
59 | 58 | adantr 482 |
. . . 4
β’ (((πΉ β π΄ β§ π β π΅) β§ (1rβπ
) β
(0gβπ
))
β ((πΉβ(πβ(1rβπ
))) Β· (πΉβπ)) = (πΉβ(πβπ))) |
60 | 51, 59 | eqtr3d 2775 |
. . 3
β’ (((πΉ β π΄ β§ π β π΅) β§ (1rβπ
) β
(0gβπ
))
β (1 Β· (πΉβπ)) = (πΉβ(πβπ))) |
61 | 1, 6 | abvcl 20326 |
. . . . . 6
β’ ((πΉ β π΄ β§ π β π΅) β (πΉβπ) β β) |
62 | 61 | recnd 11191 |
. . . . 5
β’ ((πΉ β π΄ β§ π β π΅) β (πΉβπ) β β) |
63 | 62 | mulid2d 11181 |
. . . 4
β’ ((πΉ β π΄ β§ π β π΅) β (1 Β· (πΉβπ)) = (πΉβπ)) |
64 | 63 | adantr 482 |
. . 3
β’ (((πΉ β π΄ β§ π β π΅) β§ (1rβπ
) β
(0gβπ
))
β (1 Β· (πΉβπ)) = (πΉβπ)) |
65 | 60, 64 | eqtr3d 2775 |
. 2
β’ (((πΉ β π΄ β§ π β π΅) β§ (1rβπ
) β
(0gβπ
))
β (πΉβ(πβπ)) = (πΉβπ)) |
66 | 16, 65 | pm2.61dane 3029 |
1
β’ ((πΉ β π΄ β§ π β π΅) β (πΉβ(πβπ)) = (πΉβπ)) |