Description: The ZZ -module built from a normed ring is also a normed ring. (Contributed by Thierry Arnoux, 8-Nov-2017)
Ref | Expression | ||
---|---|---|---|
Hypothesis | zlmlem2.1 | |
|
Assertion | zhmnrg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zlmlem2.1 | |
|
2 | eqid | |
|
3 | 2 | a1i | |
4 | 1 2 | zlmbas | |
5 | 4 | a1i | |
6 | eqid | |
|
7 | 1 6 | zlmplusg | |
8 | 7 | a1i | |
9 | 8 | oveqdr | |
10 | 3 5 9 | grppropd | |
11 | eqid | |
|
12 | 1 11 | zlmds | |
13 | 12 | reseq1d | |
14 | eqid | |
|
15 | 1 14 | zlmtset | |
16 | 5 15 | topnpropd | |
17 | 3 5 13 16 | mspropd | |
18 | eqid | |
|
19 | 1 18 | zlmnm | |
20 | 5 8 | grpsubpropd | |
21 | 19 20 | coeq12d | |
22 | 21 12 | sseq12d | |
23 | 10 17 22 | 3anbi123d | |
24 | eqid | |
|
25 | 18 24 11 | isngp | |
26 | eqid | |
|
27 | eqid | |
|
28 | eqid | |
|
29 | 26 27 28 | isngp | |
30 | 23 25 29 | 3bitr4g | |
31 | eqid | |
|
32 | 1 31 | zlmmulr | |
33 | 32 | a1i | |
34 | 5 8 33 | abvpropd2 | |
35 | 19 34 | eleq12d | |
36 | 30 35 | anbi12d | |
37 | eqid | |
|
38 | 18 37 | isnrg | |
39 | eqid | |
|
40 | 26 39 | isnrg | |
41 | 36 38 40 | 3bitr4g | |
42 | 41 | ibi | |