Step | Hyp | Ref
| Expression |
1 | | simpl3 1194 |
. . . . 5
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β π
β NzRing) |
2 | | nzrring 20747 |
. . . . 5
β’ (π
β NzRing β π
β Ring) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β π
β Ring) |
4 | | simpr 486 |
. . . 4
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β π β
β€) |
5 | | zrhnm.1 |
. . . . . 6
β’ πΏ = (β€RHomβπ
) |
6 | | eqid 2733 |
. . . . . 6
β’
(.gβπ
) = (.gβπ
) |
7 | | eqid 2733 |
. . . . . 6
β’
(1rβπ
) = (1rβπ
) |
8 | 5, 6, 7 | zrhmulg 20926 |
. . . . 5
β’ ((π
β Ring β§ π β β€) β (πΏβπ) = (π(.gβπ
)(1rβπ
))) |
9 | 8 | fveq2d 6847 |
. . . 4
β’ ((π
β Ring β§ π β β€) β (πβ(πΏβπ)) = (πβ(π(.gβπ
)(1rβπ
)))) |
10 | 3, 4, 9 | syl2anc 585 |
. . 3
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β (πβ(πΏβπ)) = (πβ(π(.gβπ
)(1rβπ
)))) |
11 | | simpl1 1192 |
. . . 4
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β π β NrmMod) |
12 | | nmmulg.x |
. . . . . 6
β’ π΅ = (Baseβπ
) |
13 | 12, 7 | ringidcl 19994 |
. . . . 5
β’ (π
β Ring β
(1rβπ
)
β π΅) |
14 | 3, 13 | syl 17 |
. . . 4
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β
(1rβπ
)
β π΅) |
15 | | nmmulg.n |
. . . . 5
β’ π = (normβπ
) |
16 | | nmmulg.z |
. . . . 5
β’ π = (β€Modβπ
) |
17 | 12, 15, 16, 6 | nmmulg 32606 |
. . . 4
β’ ((π β NrmMod β§ π β β€ β§
(1rβπ
)
β π΅) β (πβ(π(.gβπ
)(1rβπ
))) = ((absβπ) Β· (πβ(1rβπ
)))) |
18 | 11, 4, 14, 17 | syl3anc 1372 |
. . 3
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β (πβ(π(.gβπ
)(1rβπ
))) = ((absβπ) Β· (πβ(1rβπ
)))) |
19 | 16, 15 | zlmnm 32604 |
. . . . . . 7
β’ (π
β NzRing β π = (normβπ)) |
20 | 1, 19 | syl 17 |
. . . . . 6
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β π = (normβπ)) |
21 | 20 | fveq1d 6845 |
. . . . 5
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β (πβ(1rβπ
)) = ((normβπ)β(1rβπ
))) |
22 | | simpl2 1193 |
. . . . . 6
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β π β
NrmRing) |
23 | | nrgring 24043 |
. . . . . . . 8
β’ (π β NrmRing β π β Ring) |
24 | 22, 23 | syl 17 |
. . . . . . 7
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β π β Ring) |
25 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπ
) = (0gβπ
) |
26 | 7, 25 | nzrnz 20746 |
. . . . . . . 8
β’ (π
β NzRing β
(1rβπ
)
β (0gβπ
)) |
27 | 1, 26 | syl 17 |
. . . . . . 7
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β
(1rβπ
)
β (0gβπ
)) |
28 | 16, 7 | zlm1 32599 |
. . . . . . . 8
β’
(1rβπ
) = (1rβπ) |
29 | 16, 25 | zlm0 32598 |
. . . . . . . 8
β’
(0gβπ
) = (0gβπ) |
30 | 28, 29 | isnzr 20745 |
. . . . . . 7
β’ (π β NzRing β (π β Ring β§
(1rβπ
)
β (0gβπ
))) |
31 | 24, 27, 30 | sylanbrc 584 |
. . . . . 6
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β π β NzRing) |
32 | | eqid 2733 |
. . . . . . 7
β’
(normβπ) =
(normβπ) |
33 | 32, 28 | nm1 24047 |
. . . . . 6
β’ ((π β NrmRing β§ π β NzRing) β
((normβπ)β(1rβπ
)) = 1) |
34 | 22, 31, 33 | syl2anc 585 |
. . . . 5
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β
((normβπ)β(1rβπ
)) = 1) |
35 | 21, 34 | eqtrd 2773 |
. . . 4
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β (πβ(1rβπ
)) = 1) |
36 | 35 | oveq2d 7374 |
. . 3
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β
((absβπ) Β·
(πβ(1rβπ
))) = ((absβπ) Β· 1)) |
37 | 10, 18, 36 | 3eqtrd 2777 |
. 2
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β (πβ(πΏβπ)) = ((absβπ) Β· 1)) |
38 | 4 | zcnd 12613 |
. . 3
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β π β
β) |
39 | | abscl 15169 |
. . . 4
β’ (π β β β
(absβπ) β
β) |
40 | 39 | recnd 11188 |
. . 3
β’ (π β β β
(absβπ) β
β) |
41 | | mulid1 11158 |
. . 3
β’
((absβπ)
β β β ((absβπ) Β· 1) = (absβπ)) |
42 | 38, 40, 41 | 3syl 18 |
. 2
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β
((absβπ) Β· 1)
= (absβπ)) |
43 | 37, 42 | eqtrd 2773 |
1
β’ (((π β NrmMod β§ π β NrmRing β§ π
β NzRing) β§ π β β€) β (πβ(πΏβπ)) = (absβπ)) |