Metamath Proof Explorer

Theorem subgngp

Description: A normed group restricted to a subgroup is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypothesis subgngp.h 
|- H = ( G |`s A )
Assertion subgngp 
|- ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) -> H e. NrmGrp )

Proof

Step Hyp Ref Expression
1 subgngp.h 
 |-  H = ( G |`s A )
2 1 subggrp 
 |-  ( A e. ( SubGrp ` G ) -> H e. Grp )
3 2 adantl 
 |-  ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) -> H e. Grp )
4 ngpms 
 |-  ( G e. NrmGrp -> G e. MetSp )
5 ressms 
 |-  ( ( G e. MetSp /\ A e. ( SubGrp ` G ) ) -> ( G |`s A ) e. MetSp )
6 4 5 sylan 
 |-  ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) -> ( G |`s A ) e. MetSp )
7 1 6 eqeltrid 
 |-  ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) -> H e. MetSp )
8 simplr 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> A e. ( SubGrp ` G ) )
9 simprl 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> x e. ( Base ` H ) )
10 1 subgbas 
 |-  ( A e. ( SubGrp ` G ) -> A = ( Base ` H ) )
11 10 ad2antlr 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> A = ( Base ` H ) )
12 9 11 eleqtrrd 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> x e. A )
13 simprr 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> y e. ( Base ` H ) )
14 13 11 eleqtrrd 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> y e. A )
15 eqid 
 |-  ( -g ` G ) = ( -g ` G )
16 eqid 
 |-  ( -g ` H ) = ( -g ` H )
17 15 1 16 subgsub 
 |-  ( ( A e. ( SubGrp ` G ) /\ x e. A /\ y e. A ) -> ( x ( -g ` G ) y ) = ( x ( -g ` H ) y ) )
18 8 12 14 17 syl3anc 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> ( x ( -g ` G ) y ) = ( x ( -g ` H ) y ) )
19 18 fveq2d 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> ( ( norm ` G ) ` ( x ( -g ` G ) y ) ) = ( ( norm ` G ) ` ( x ( -g ` H ) y ) ) )
20 eqid 
 |-  ( dist ` G ) = ( dist ` G )
21 1 20 ressds 
 |-  ( A e. ( SubGrp ` G ) -> ( dist ` G ) = ( dist ` H ) )
22 21 ad2antlr 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> ( dist ` G ) = ( dist ` H ) )
23 22 oveqd 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> ( x ( dist ` G ) y ) = ( x ( dist ` H ) y ) )
24 simpll 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> G e. NrmGrp )
25 eqid 
 |-  ( Base ` G ) = ( Base ` G )
26 25 subgss 
 |-  ( A e. ( SubGrp ` G ) -> A C_ ( Base ` G ) )
27 26 ad2antlr 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> A C_ ( Base ` G ) )
28 27 12 sseldd 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> x e. ( Base ` G ) )
29 27 14 sseldd 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> y e. ( Base ` G ) )
30 eqid 
 |-  ( norm ` G ) = ( norm ` G )
31 30 25 15 20 ngpds 
 |-  ( ( G e. NrmGrp /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( dist ` G ) y ) = ( ( norm ` G ) ` ( x ( -g ` G ) y ) ) )
32 24 28 29 31 syl3anc 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> ( x ( dist ` G ) y ) = ( ( norm ` G ) ` ( x ( -g ` G ) y ) ) )
33 23 32 eqtr3d 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> ( x ( dist ` H ) y ) = ( ( norm ` G ) ` ( x ( -g ` G ) y ) ) )
34 eqid 
 |-  ( Base ` H ) = ( Base ` H )
35 34 16 grpsubcl 
 |-  ( ( H e. Grp /\ x e. ( Base ` H ) /\ y e. ( Base ` H ) ) -> ( x ( -g ` H ) y ) e. ( Base ` H ) )
36 35 3expb 
 |-  ( ( H e. Grp /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> ( x ( -g ` H ) y ) e. ( Base ` H ) )
37 3 36 sylan 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> ( x ( -g ` H ) y ) e. ( Base ` H ) )
38 37 11 eleqtrrd 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> ( x ( -g ` H ) y ) e. A )
39 eqid 
 |-  ( norm ` H ) = ( norm ` H )
40 1 30 39 subgnm2 
 |-  ( ( A e. ( SubGrp ` G ) /\ ( x ( -g ` H ) y ) e. A ) -> ( ( norm ` H ) ` ( x ( -g ` H ) y ) ) = ( ( norm ` G ) ` ( x ( -g ` H ) y ) ) )
41 8 38 40 syl2anc 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> ( ( norm ` H ) ` ( x ( -g ` H ) y ) ) = ( ( norm ` G ) ` ( x ( -g ` H ) y ) ) )
42 19 33 41 3eqtr4d 
 |-  ( ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) /\ ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) -> ( x ( dist ` H ) y ) = ( ( norm ` H ) ` ( x ( -g ` H ) y ) ) )
43 42 ralrimivva 
 |-  ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) -> A. x e. ( Base ` H ) A. y e. ( Base ` H ) ( x ( dist ` H ) y ) = ( ( norm ` H ) ` ( x ( -g ` H ) y ) ) )
44 eqid 
 |-  ( dist ` H ) = ( dist ` H )
45 39 16 44 34 isngp3 
 |-  ( H e. NrmGrp <-> ( H e. Grp /\ H e. MetSp /\ A. x e. ( Base ` H ) A. y e. ( Base ` H ) ( x ( dist ` H ) y ) = ( ( norm ` H ) ` ( x ( -g ` H ) y ) ) ) )
46 3 7 43 45 syl3anbrc 
 |-  ( ( G e. NrmGrp /\ A e. ( SubGrp ` G ) ) -> H e. NrmGrp )