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 |`s A )
Assertion subrgnrg 
|- ( ( G e. NrmRing /\ A e. ( SubRing ` G ) ) -> H e. NrmRing )

Proof

Step Hyp Ref Expression
1 subrgnrg.h 
 |-  H = ( G |`s A )
2 nrgngp 
 |-  ( G e. NrmRing -> G e. NrmGrp )
3 subrgsubg 
 |-  ( A e. ( SubRing ` G ) -> A e. ( SubGrp ` G ) )
4 1 subgngp 
 |-  ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) -> H e. NrmGrp )
5 2 3 4 syl2an 
 |-  ( ( G e. NrmRing /\ A e. ( SubRing ` G ) ) -> H e. NrmGrp )
6 3 adantl 
 |-  ( ( G e. NrmRing /\ A e. ( SubRing ` G ) ) -> A e. ( SubGrp ` G ) )
7 eqid 
 |-  ( norm ` G ) = ( norm ` G )
8 eqid 
 |-  ( norm ` H ) = ( norm ` H )
9 1 7 8 subgnm 
 |-  ( A e. ( SubGrp ` G ) -> ( norm ` H ) = ( ( norm ` G ) |` A ) )
10 6 9 syl 
 |-  ( ( G e. NrmRing /\ A e. ( SubRing ` G ) ) -> ( norm ` H ) = ( ( norm ` G ) |` A ) )
11 eqid 
 |-  ( AbsVal ` G ) = ( AbsVal ` G )
12 7 11 nrgabv 
 |-  ( G e. NrmRing -> ( norm ` G ) e. ( AbsVal ` G ) )
13 eqid 
 |-  ( AbsVal ` H ) = ( AbsVal ` H )
14 11 1 13 abvres 
 |-  ( ( ( norm ` G ) e. ( AbsVal ` G ) /\ A e. ( SubRing ` G ) ) -> ( ( norm ` G ) |` A ) e. ( AbsVal ` H ) )
15 12 14 sylan 
 |-  ( ( G e. NrmRing /\ A e. ( SubRing ` G ) ) -> ( ( norm ` G ) |` A ) e. ( AbsVal ` H ) )
16 10 15 eqeltrd 
 |-  ( ( G e. NrmRing /\ A e. ( SubRing ` G ) ) -> ( norm ` H ) e. ( AbsVal ` H ) )
17 8 13 isnrg 
 |-  ( H e. NrmRing <-> ( H e. NrmGrp /\ ( norm ` H ) e. ( AbsVal ` H ) ) )
18 5 16 17 sylanbrc 
 |-  ( ( G e. NrmRing /\ A e. ( SubRing ` G ) ) -> H e. NrmRing )