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 ↾ 𝑠 A
Assertion subgngp ⊢ G ∈ NrmGrp ∧ A ∈ SubGrp ⁡ G → H ∈ NrmGrp

Proof

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