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