Metamath Proof Explorer

Theorem zhmnrg

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 ⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
Assertion zhmnrg ( 𝐺 ∈ NrmRing → 𝑊 ∈ NrmRing )

Proof

Step Hyp Ref Expression
1 zlmlem2.1 ⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
2 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3 2 a1i ⊢ ( 𝐺 ∈ NrmRing → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
4 1 2 zlmbas ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝑊 )
5 4 a1i ⊢ ( 𝐺 ∈ NrmRing → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑊 ) )
6 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
7 1 6 zlmplusg ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝑊 )
8 7 a1i ⊢ ( 𝐺 ∈ NrmRing → ( +g ‘ 𝐺 ) = ( +g ‘ 𝑊 ) )
9 8 oveqdr ⊢ ( ( 𝐺 ∈ NrmRing ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) )
10 3 5 9 grppropd ⊢ ( 𝐺 ∈ NrmRing → ( 𝐺 ∈ Grp ↔ 𝑊 ∈ Grp ) )
11 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
12 1 11 zlmds ⊢ ( 𝐺 ∈ NrmRing → ( dist ‘ 𝐺 ) = ( dist ‘ 𝑊 ) )
13 12 reseq1d ⊢ ( 𝐺 ∈ NrmRing → ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) = ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) )
14 eqid ⊢ ( TopSet ‘ 𝐺 ) = ( TopSet ‘ 𝐺 )
15 1 14 zlmtset ⊢ ( 𝐺 ∈ NrmRing → ( TopSet ‘ 𝐺 ) = ( TopSet ‘ 𝑊 ) )
16 5 15 topnpropd ⊢ ( 𝐺 ∈ NrmRing → ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝑊 ) )
17 3 5 13 16 mspropd ⊢ ( 𝐺 ∈ NrmRing → ( 𝐺 ∈ MetSp ↔ 𝑊 ∈ MetSp ) )
18 eqid ⊢ ( norm ‘ 𝐺 ) = ( norm ‘ 𝐺 )
19 1 18 zlmnm ⊢ ( 𝐺 ∈ NrmRing → ( norm ‘ 𝐺 ) = ( norm ‘ 𝑊 ) )
20 5 8 grpsubpropd ⊢ ( 𝐺 ∈ NrmRing → ( -g ‘ 𝐺 ) = ( -g ‘ 𝑊 ) )
21 19 20 coeq12d ⊢ ( 𝐺 ∈ NrmRing → ( ( norm ‘ 𝐺 ) ∘ ( -g ‘ 𝐺 ) ) = ( ( norm ‘ 𝑊 ) ∘ ( -g ‘ 𝑊 ) ) )
22 21 12 sseq12d ⊢ ( 𝐺 ∈ NrmRing → ( ( ( norm ‘ 𝐺 ) ∘ ( -g ‘ 𝐺 ) ) ⊆ ( dist ‘ 𝐺 ) ↔ ( ( norm ‘ 𝑊 ) ∘ ( -g ‘ 𝑊 ) ) ⊆ ( dist ‘ 𝑊 ) ) )
23 10 17 22 3anbi123d ⊢ ( 𝐺 ∈ NrmRing → ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( ( norm ‘ 𝐺 ) ∘ ( -g ‘ 𝐺 ) ) ⊆ ( dist ‘ 𝐺 ) ) ↔ ( 𝑊 ∈ Grp ∧ 𝑊 ∈ MetSp ∧ ( ( norm ‘ 𝑊 ) ∘ ( -g ‘ 𝑊 ) ) ⊆ ( dist ‘ 𝑊 ) ) ) )
24 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
25 18 24 11 isngp ⊢ ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( ( norm ‘ 𝐺 ) ∘ ( -g ‘ 𝐺 ) ) ⊆ ( dist ‘ 𝐺 ) ) )
26 eqid ⊢ ( norm ‘ 𝑊 ) = ( norm ‘ 𝑊 )
27 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
28 eqid ⊢ ( dist ‘ 𝑊 ) = ( dist ‘ 𝑊 )
29 26 27 28 isngp ⊢ ( 𝑊 ∈ NrmGrp ↔ ( 𝑊 ∈ Grp ∧ 𝑊 ∈ MetSp ∧ ( ( norm ‘ 𝑊 ) ∘ ( -g ‘ 𝑊 ) ) ⊆ ( dist ‘ 𝑊 ) ) )
30 23 25 29 3bitr4g ⊢ ( 𝐺 ∈ NrmRing → ( 𝐺 ∈ NrmGrp ↔ 𝑊 ∈ NrmGrp ) )
31 eqid ⊢ ( .r ‘ 𝐺 ) = ( .r ‘ 𝐺 )
32 1 31 zlmmulr ⊢ ( .r ‘ 𝐺 ) = ( .r ‘ 𝑊 )
33 32 a1i ⊢ ( 𝐺 ∈ NrmRing → ( .r ‘ 𝐺 ) = ( .r ‘ 𝑊 ) )
34 5 8 33 abvpropd2 ⊢ ( 𝐺 ∈ NrmRing → ( AbsVal ‘ 𝐺 ) = ( AbsVal ‘ 𝑊 ) )
35 19 34 eleq12d ⊢ ( 𝐺 ∈ NrmRing → ( ( norm ‘ 𝐺 ) ∈ ( AbsVal ‘ 𝐺 ) ↔ ( norm ‘ 𝑊 ) ∈ ( AbsVal ‘ 𝑊 ) ) )
36 30 35 anbi12d ⊢ ( 𝐺 ∈ NrmRing → ( ( 𝐺 ∈ NrmGrp ∧ ( norm ‘ 𝐺 ) ∈ ( AbsVal ‘ 𝐺 ) ) ↔ ( 𝑊 ∈ NrmGrp ∧ ( norm ‘ 𝑊 ) ∈ ( AbsVal ‘ 𝑊 ) ) ) )
37 eqid ⊢ ( AbsVal ‘ 𝐺 ) = ( AbsVal ‘ 𝐺 )
38 18 37 isnrg ⊢ ( 𝐺 ∈ NrmRing ↔ ( 𝐺 ∈ NrmGrp ∧ ( norm ‘ 𝐺 ) ∈ ( AbsVal ‘ 𝐺 ) ) )
39 eqid ⊢ ( AbsVal ‘ 𝑊 ) = ( AbsVal ‘ 𝑊 )
40 26 39 isnrg ⊢ ( 𝑊 ∈ NrmRing ↔ ( 𝑊 ∈ NrmGrp ∧ ( norm ‘ 𝑊 ) ∈ ( AbsVal ‘ 𝑊 ) ) )
41 36 38 40 3bitr4g ⊢ ( 𝐺 ∈ NrmRing → ( 𝐺 ∈ NrmRing ↔ 𝑊 ∈ NrmRing ) )
42 41 ibi ⊢ ( 𝐺 ∈ NrmRing → 𝑊 ∈ NrmRing )