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 ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
Assertion subgngp ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐻 ∈ NrmGrp )

Proof

Step Hyp Ref Expression
1 subgngp.h ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
2 1 subggrp ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )
3 2 adantl ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐻 ∈ Grp )
4 ngpms ⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp )
5 ressms ⊢ ( ( 𝐺 ∈ MetSp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 ↾s 𝐴 ) ∈ MetSp )
6 4 5 sylan ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 ↾s 𝐴 ) ∈ MetSp )
7 1 6 eqeltrid ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐻 ∈ MetSp )
8 simplr ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → 𝐴 ∈ ( SubGrp ‘ 𝐺 ) )
9 simprl ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐻 ) )
10 1 subgbas ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝐴 = ( Base ‘ 𝐻 ) )
11 10 ad2antlr ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → 𝐴 = ( Base ‘ 𝐻 ) )
12 9 11 eleqtrrd ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → 𝑥 ∈ 𝐴 )
13 simprr ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐻 ) )
14 13 11 eleqtrrd ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → 𝑦 ∈ 𝐴 )
15 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
16 eqid ⊢ ( -g ‘ 𝐻 ) = ( -g ‘ 𝐻 )
17 15 1 16 subgsub ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( -g ‘ 𝐻 ) 𝑦 ) )
18 8 12 14 17 syl3anc ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( -g ‘ 𝐻 ) 𝑦 ) )
19 18 fveq2d ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → ( ( norm ‘ 𝐺 ) ‘ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝑥 ( -g ‘ 𝐻 ) 𝑦 ) ) )
20 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
21 1 20 ressds ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( dist ‘ 𝐺 ) = ( dist ‘ 𝐻 ) )
22 21 ad2antlr ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → ( dist ‘ 𝐺 ) = ( dist ‘ 𝐻 ) )
23 22 oveqd ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( dist ‘ 𝐻 ) 𝑦 ) )
24 simpll ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → 𝐺 ∈ NrmGrp )
25 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
26 25 subgss ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
27 26 ad2antlr ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
28 27 12 sseldd ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
29 27 14 sseldd ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
30 eqid ⊢ ( norm ‘ 𝐺 ) = ( norm ‘ 𝐺 )
31 30 25 15 20 ngpds ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ) )
32 24 28 29 31 syl3anc ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ) )
33 23 32 eqtr3d ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → ( 𝑥 ( dist ‘ 𝐻 ) 𝑦 ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ) )
34 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
35 34 16 grpsubcl ⊢ ( ( 𝐻 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) → ( 𝑥 ( -g ‘ 𝐻 ) 𝑦 ) ∈ ( Base ‘ 𝐻 ) )
36 35 3expb ⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → ( 𝑥 ( -g ‘ 𝐻 ) 𝑦 ) ∈ ( Base ‘ 𝐻 ) )
37 3 36 sylan ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → ( 𝑥 ( -g ‘ 𝐻 ) 𝑦 ) ∈ ( Base ‘ 𝐻 ) )
38 37 11 eleqtrrd ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → ( 𝑥 ( -g ‘ 𝐻 ) 𝑦 ) ∈ 𝐴 )
39 eqid ⊢ ( norm ‘ 𝐻 ) = ( norm ‘ 𝐻 )
40 1 30 39 subgnm2 ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑥 ( -g ‘ 𝐻 ) 𝑦 ) ∈ 𝐴 ) → ( ( norm ‘ 𝐻 ) ‘ ( 𝑥 ( -g ‘ 𝐻 ) 𝑦 ) ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝑥 ( -g ‘ 𝐻 ) 𝑦 ) ) )
41 8 38 40 syl2anc ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → ( ( norm ‘ 𝐻 ) ‘ ( 𝑥 ( -g ‘ 𝐻 ) 𝑦 ) ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝑥 ( -g ‘ 𝐻 ) 𝑦 ) ) )
42 19 33 41 3eqtr4d ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) → ( 𝑥 ( dist ‘ 𝐻 ) 𝑦 ) = ( ( norm ‘ 𝐻 ) ‘ ( 𝑥 ( -g ‘ 𝐻 ) 𝑦 ) ) )
43 42 ralrimivva ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ( 𝑥 ( dist ‘ 𝐻 ) 𝑦 ) = ( ( norm ‘ 𝐻 ) ‘ ( 𝑥 ( -g ‘ 𝐻 ) 𝑦 ) ) )
44 eqid ⊢ ( dist ‘ 𝐻 ) = ( dist ‘ 𝐻 )
45 39 16 44 34 isngp3 ⊢ ( 𝐻 ∈ NrmGrp ↔ ( 𝐻 ∈ Grp ∧ 𝐻 ∈ MetSp ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ( 𝑥 ( dist ‘ 𝐻 ) 𝑦 ) = ( ( norm ‘ 𝐻 ) ‘ ( 𝑥 ( -g ‘ 𝐻 ) 𝑦 ) ) ) )
46 3 7 43 45 syl3anbrc ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐻 ∈ NrmGrp )