# 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 ${⊢}\left({G}\in \mathrm{NrmRing}\wedge {A}\in \mathrm{SubRing}\left({G}\right)\right)\to {H}\in \mathrm{NrmRing}$

### Proof

Step Hyp Ref Expression
1 subrgnrg.h ${⊢}{H}={G}{↾}_{𝑠}{A}$
2 nrgngp ${⊢}{G}\in \mathrm{NrmRing}\to {G}\in \mathrm{NrmGrp}$
3 subrgsubg ${⊢}{A}\in \mathrm{SubRing}\left({G}\right)\to {A}\in \mathrm{SubGrp}\left({G}\right)$
4 1 subgngp ${⊢}\left({G}\in \mathrm{NrmGrp}\wedge {A}\in \mathrm{SubGrp}\left({G}\right)\right)\to {H}\in \mathrm{NrmGrp}$
5 2 3 4 syl2an ${⊢}\left({G}\in \mathrm{NrmRing}\wedge {A}\in \mathrm{SubRing}\left({G}\right)\right)\to {H}\in \mathrm{NrmGrp}$
6 3 adantl ${⊢}\left({G}\in \mathrm{NrmRing}\wedge {A}\in \mathrm{SubRing}\left({G}\right)\right)\to {A}\in \mathrm{SubGrp}\left({G}\right)$
7 eqid ${⊢}\mathrm{norm}\left({G}\right)=\mathrm{norm}\left({G}\right)$
8 eqid ${⊢}\mathrm{norm}\left({H}\right)=\mathrm{norm}\left({H}\right)$
9 1 7 8 subgnm ${⊢}{A}\in \mathrm{SubGrp}\left({G}\right)\to \mathrm{norm}\left({H}\right)={\mathrm{norm}\left({G}\right)↾}_{{A}}$
10 6 9 syl ${⊢}\left({G}\in \mathrm{NrmRing}\wedge {A}\in \mathrm{SubRing}\left({G}\right)\right)\to \mathrm{norm}\left({H}\right)={\mathrm{norm}\left({G}\right)↾}_{{A}}$
11 eqid ${⊢}\mathrm{AbsVal}\left({G}\right)=\mathrm{AbsVal}\left({G}\right)$
12 7 11 nrgabv ${⊢}{G}\in \mathrm{NrmRing}\to \mathrm{norm}\left({G}\right)\in \mathrm{AbsVal}\left({G}\right)$
13 eqid ${⊢}\mathrm{AbsVal}\left({H}\right)=\mathrm{AbsVal}\left({H}\right)$
14 11 1 13 abvres ${⊢}\left(\mathrm{norm}\left({G}\right)\in \mathrm{AbsVal}\left({G}\right)\wedge {A}\in \mathrm{SubRing}\left({G}\right)\right)\to {\mathrm{norm}\left({G}\right)↾}_{{A}}\in \mathrm{AbsVal}\left({H}\right)$
15 12 14 sylan ${⊢}\left({G}\in \mathrm{NrmRing}\wedge {A}\in \mathrm{SubRing}\left({G}\right)\right)\to {\mathrm{norm}\left({G}\right)↾}_{{A}}\in \mathrm{AbsVal}\left({H}\right)$
16 10 15 eqeltrd ${⊢}\left({G}\in \mathrm{NrmRing}\wedge {A}\in \mathrm{SubRing}\left({G}\right)\right)\to \mathrm{norm}\left({H}\right)\in \mathrm{AbsVal}\left({H}\right)$
17 8 13 isnrg ${⊢}{H}\in \mathrm{NrmRing}↔\left({H}\in \mathrm{NrmGrp}\wedge \mathrm{norm}\left({H}\right)\in \mathrm{AbsVal}\left({H}\right)\right)$
18 5 16 17 sylanbrc ${⊢}\left({G}\in \mathrm{NrmRing}\wedge {A}\in \mathrm{SubRing}\left({G}\right)\right)\to {H}\in \mathrm{NrmRing}$