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 )