This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
Assertion subrgnrg ( ( 𝐺 ∈ NrmRing ∧ 𝐴 ∈ ( SubRing ‘ 𝐺 ) ) → 𝐻 ∈ NrmRing )

Proof

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