Step | Hyp | Ref
| Expression |
1 | | eqid 2731 |
. . . . . . . 8
β’
(BaseβπΊ) =
(BaseβπΊ) |
2 | 1 | a1i 11 |
. . . . . . 7
β’ (πΊ β NrmRing β
(BaseβπΊ) =
(BaseβπΊ)) |
3 | | zlmlem2.1 |
. . . . . . . . 9
β’ π = (β€ModβπΊ) |
4 | 3, 1 | zlmbas 21378 |
. . . . . . . 8
β’
(BaseβπΊ) =
(Baseβπ) |
5 | 4 | a1i 11 |
. . . . . . 7
β’ (πΊ β NrmRing β
(BaseβπΊ) =
(Baseβπ)) |
6 | | eqid 2731 |
. . . . . . . . . 10
β’
(+gβπΊ) = (+gβπΊ) |
7 | 3, 6 | zlmplusg 21380 |
. . . . . . . . 9
β’
(+gβπΊ) = (+gβπ) |
8 | 7 | a1i 11 |
. . . . . . . 8
β’ (πΊ β NrmRing β
(+gβπΊ) =
(+gβπ)) |
9 | 8 | oveqdr 7440 |
. . . . . . 7
β’ ((πΊ β NrmRing β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β (π₯(+gβπΊ)π¦) = (π₯(+gβπ)π¦)) |
10 | 2, 5, 9 | grppropd 18879 |
. . . . . 6
β’ (πΊ β NrmRing β (πΊ β Grp β π β Grp)) |
11 | | eqid 2731 |
. . . . . . . . 9
β’
(distβπΊ) =
(distβπΊ) |
12 | 3, 11 | zlmds 33406 |
. . . . . . . 8
β’ (πΊ β NrmRing β
(distβπΊ) =
(distβπ)) |
13 | 12 | reseq1d 5980 |
. . . . . . 7
β’ (πΊ β NrmRing β
((distβπΊ) βΎ
((BaseβπΊ) Γ
(BaseβπΊ))) =
((distβπ) βΎ
((BaseβπΊ) Γ
(BaseβπΊ)))) |
14 | | eqid 2731 |
. . . . . . . . 9
β’
(TopSetβπΊ) =
(TopSetβπΊ) |
15 | 3, 14 | zlmtset 33408 |
. . . . . . . 8
β’ (πΊ β NrmRing β
(TopSetβπΊ) =
(TopSetβπ)) |
16 | 5, 15 | topnpropd 17389 |
. . . . . . 7
β’ (πΊ β NrmRing β
(TopOpenβπΊ) =
(TopOpenβπ)) |
17 | 2, 5, 13, 16 | mspropd 24300 |
. . . . . 6
β’ (πΊ β NrmRing β (πΊ β MetSp β π β MetSp)) |
18 | | eqid 2731 |
. . . . . . . . 9
β’
(normβπΊ) =
(normβπΊ) |
19 | 3, 18 | zlmnm 33410 |
. . . . . . . 8
β’ (πΊ β NrmRing β
(normβπΊ) =
(normβπ)) |
20 | 5, 8 | grpsubpropd 18971 |
. . . . . . . 8
β’ (πΊ β NrmRing β
(-gβπΊ) =
(-gβπ)) |
21 | 19, 20 | coeq12d 5864 |
. . . . . . 7
β’ (πΊ β NrmRing β
((normβπΊ) β
(-gβπΊ)) =
((normβπ) β
(-gβπ))) |
22 | 21, 12 | sseq12d 4015 |
. . . . . 6
β’ (πΊ β NrmRing β
(((normβπΊ) β
(-gβπΊ))
β (distβπΊ)
β ((normβπ)
β (-gβπ)) β (distβπ))) |
23 | 10, 17, 22 | 3anbi123d 1435 |
. . . . 5
β’ (πΊ β NrmRing β ((πΊ β Grp β§ πΊ β MetSp β§
((normβπΊ) β
(-gβπΊ))
β (distβπΊ))
β (π β Grp β§
π β MetSp β§
((normβπ) β
(-gβπ))
β (distβπ)))) |
24 | | eqid 2731 |
. . . . . 6
β’
(-gβπΊ) = (-gβπΊ) |
25 | 18, 24, 11 | isngp 24425 |
. . . . 5
β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§
((normβπΊ) β
(-gβπΊ))
β (distβπΊ))) |
26 | | eqid 2731 |
. . . . . 6
β’
(normβπ) =
(normβπ) |
27 | | eqid 2731 |
. . . . . 6
β’
(-gβπ) = (-gβπ) |
28 | | eqid 2731 |
. . . . . 6
β’
(distβπ) =
(distβπ) |
29 | 26, 27, 28 | isngp 24425 |
. . . . 5
β’ (π β NrmGrp β (π β Grp β§ π β MetSp β§
((normβπ) β
(-gβπ))
β (distβπ))) |
30 | 23, 25, 29 | 3bitr4g 314 |
. . . 4
β’ (πΊ β NrmRing β (πΊ β NrmGrp β π β
NrmGrp)) |
31 | | eqid 2731 |
. . . . . . . 8
β’
(.rβπΊ) = (.rβπΊ) |
32 | 3, 31 | zlmmulr 21382 |
. . . . . . 7
β’
(.rβπΊ) = (.rβπ) |
33 | 32 | a1i 11 |
. . . . . 6
β’ (πΊ β NrmRing β
(.rβπΊ) =
(.rβπ)) |
34 | 5, 8, 33 | abvpropd2 32562 |
. . . . 5
β’ (πΊ β NrmRing β
(AbsValβπΊ) =
(AbsValβπ)) |
35 | 19, 34 | eleq12d 2826 |
. . . 4
β’ (πΊ β NrmRing β
((normβπΊ) β
(AbsValβπΊ) β
(normβπ) β
(AbsValβπ))) |
36 | 30, 35 | anbi12d 630 |
. . 3
β’ (πΊ β NrmRing β ((πΊ β NrmGrp β§
(normβπΊ) β
(AbsValβπΊ)) β
(π β NrmGrp β§
(normβπ) β
(AbsValβπ)))) |
37 | | eqid 2731 |
. . . 4
β’
(AbsValβπΊ) =
(AbsValβπΊ) |
38 | 18, 37 | isnrg 24497 |
. . 3
β’ (πΊ β NrmRing β (πΊ β NrmGrp β§
(normβπΊ) β
(AbsValβπΊ))) |
39 | | eqid 2731 |
. . . 4
β’
(AbsValβπ) =
(AbsValβπ) |
40 | 26, 39 | isnrg 24497 |
. . 3
β’ (π β NrmRing β (π β NrmGrp β§
(normβπ) β
(AbsValβπ))) |
41 | 36, 38, 40 | 3bitr4g 314 |
. 2
β’ (πΊ β NrmRing β (πΊ β NrmRing β π β
NrmRing)) |
42 | 41 | ibi 267 |
1
β’ (πΊ β NrmRing β π β
NrmRing) |