Metamath Proof Explorer

Theorem subrgnrg

Description: A normed ring restricted to a subring is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypothesis subrgnrg.h ⊢ H = G ↾ 𝑠 A
Assertion subrgnrg ⊢ G ∈ NrmRing ∧ A ∈ SubRing ⁡ G → H ∈ NrmRing

Proof

Step Hyp Ref Expression
1 subrgnrg.h ⊢ H = G ↾ 𝑠 A
2 nrgngp ⊢ G ∈ NrmRing → G ∈ NrmGrp
3 subrgsubg ⊢ A ∈ SubRing ⁡ G → A ∈ SubGrp ⁡ G
4 1 subgngp ⊢ G ∈ NrmGrp ∧ A ∈ SubGrp ⁡ G → H ∈ NrmGrp
5 2 3 4 syl2an ⊢ G ∈ NrmRing ∧ A ∈ SubRing ⁡ G → H ∈ NrmGrp
6 3 adantl ⊢ G ∈ NrmRing ∧ A ∈ SubRing ⁡ G → A ∈ SubGrp ⁡ G
7 eqid ⊢ norm ⁡ G = norm ⁡ G
8 eqid ⊢ norm ⁡ H = norm ⁡ H
9 1 7 8 subgnm ⊢ A ∈ SubGrp ⁡ G → norm ⁡ H = norm ⁡ G ↾ A
10 6 9 syl ⊢ G ∈ NrmRing ∧ A ∈ SubRing ⁡ G → norm ⁡ H = norm ⁡ G ↾ A
11 eqid ⊢ AbsVal ⁡ G = AbsVal ⁡ G
12 7 11 nrgabv ⊢ G ∈ NrmRing → norm ⁡ G ∈ AbsVal ⁡ G
13 eqid ⊢ AbsVal ⁡ H = AbsVal ⁡ H
14 11 1 13 abvres ⊢ norm ⁡ G ∈ AbsVal ⁡ G ∧ A ∈ SubRing ⁡ G → norm ⁡ G ↾ A ∈ AbsVal ⁡ H
15 12 14 sylan ⊢ G ∈ NrmRing ∧ A ∈ SubRing ⁡ G → norm ⁡ G ↾ A ∈ AbsVal ⁡ H
16 10 15 eqeltrd ⊢ G ∈ NrmRing ∧ A ∈ SubRing ⁡ G → norm ⁡ H ∈ AbsVal ⁡ H
17 8 13 isnrg ⊢ H ∈ NrmRing ↔ H ∈ NrmGrp ∧ norm ⁡ H ∈ AbsVal ⁡ H
18 5 16 17 sylanbrc ⊢ G ∈ NrmRing ∧ A ∈ SubRing ⁡ G → H ∈ NrmRing