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 \in NrmGrp \land A \in SubGrp (G)) \to H \in NrmGrp$

Proof

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

Metamath Proof Explorer

Theorem subgngp

Proof