isngp3

Description: The property of being a normed group. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	isngp.n	$⊢ N = norm (G)$
	isngp.z	$⊢ \underset{˙}{-} = -_{G}$
	isngp.d	$⊢ D = dist (G)$
	isngp2.x	$⊢ X = {Base}_{G}$
Assertion	isngp3	$⊢ G \in NrmGrp \leftrightarrow (G \in Grp \land G \in MetSp \land \forall x \in X \forall y \in X x D y = N (x \underset{˙}{-} y))$

Proof

Step	Hyp	Ref	Expression
1		isngp.n	$⊢ N = norm (G)$
2		isngp.z	$⊢ \underset{˙}{-} = -_{G}$
3		isngp.d	$⊢ D = dist (G)$
4		isngp2.x	$⊢ X = {Base}_{G}$
5		eqid	$⊢ {D ↾}_{(X \times X)} = {D ↾}_{(X \times X)}$
6	1 2 3 4 5	isngp2	$⊢ G \in NrmGrp \leftrightarrow (G \in Grp \land G \in MetSp \land N \circ \underset{˙}{-} = {D ↾}_{(X \times X)})$
7	4 3	msmet2	$⊢ G \in MetSp \to {D ↾}_{(X \times X)} \in Met (X)$
8	1 4 3 5	nmf2	$⊢ (G \in Grp \land {D ↾}_{(X \times X)} \in Met (X)) \to N : X ⟶ ℝ$
9	7 8	sylan2	$⊢ (G \in Grp \land G \in MetSp) \to N : X ⟶ ℝ$
10	4 2	grpsubf	$⊢ G \in Grp \to \underset{˙}{-} : X \times X ⟶ X$
11	10	adantr	$⊢ (G \in Grp \land G \in MetSp) \to \underset{˙}{-} : X \times X ⟶ X$
12		fco	$⊢ (N : X ⟶ ℝ \land \underset{˙}{-} : X \times X ⟶ X) \to (N \circ \underset{˙}{-}) : X \times X ⟶ ℝ$
13	9 11 12	syl2anc	$⊢ (G \in Grp \land G \in MetSp) \to (N \circ \underset{˙}{-}) : X \times X ⟶ ℝ$
14	13	ffnd	$⊢ (G \in Grp \land G \in MetSp) \to (N \circ \underset{˙}{-}) Fn (X \times X)$
15	7	adantl	$⊢ (G \in Grp \land G \in MetSp) \to {D ↾}_{(X \times X)} \in Met (X)$
16		metf	$⊢ {D ↾}_{(X \times X)} \in Met (X) \to ({D ↾}_{(X \times X)}) : X \times X ⟶ ℝ$
17		ffn	$⊢ ({D ↾}_{(X \times X)}) : X \times X ⟶ ℝ \to ({D ↾}_{(X \times X)}) Fn (X \times X)$
18	15 16 17	3syl	$⊢ (G \in Grp \land G \in MetSp) \to ({D ↾}_{(X \times X)}) Fn (X \times X)$
19		eqfnov2	$⊢ ((N \circ \underset{˙}{-}) Fn (X \times X) \land ({D ↾}_{(X \times X)}) Fn (X \times X)) \to (N \circ \underset{˙}{-} = {D ↾}_{(X \times X)} \leftrightarrow \forall x \in X \forall y \in X x (N \circ \underset{˙}{-}) y = x ({D ↾}_{(X \times X)}) y)$
20	14 18 19	syl2anc	$⊢ (G \in Grp \land G \in MetSp) \to (N \circ \underset{˙}{-} = {D ↾}_{(X \times X)} \leftrightarrow \forall x \in X \forall y \in X x (N \circ \underset{˙}{-}) y = x ({D ↾}_{(X \times X)}) y)$
21		opelxpi	$⊢ (x \in X \land y \in X) \to ⟨x, y⟩ \in (X \times X)$
22		fvco3	$⊢ (\underset{˙}{-} : X \times X ⟶ X \land ⟨x, y⟩ \in (X \times X)) \to (N \circ \underset{˙}{-}) (⟨x, y⟩) = N (\underset{˙}{-} (⟨x, y⟩))$
23	11 21 22	syl2an	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to (N \circ \underset{˙}{-}) (⟨x, y⟩) = N (\underset{˙}{-} (⟨x, y⟩))$
24		df-ov	$⊢ x (N \circ \underset{˙}{-}) y = (N \circ \underset{˙}{-}) (⟨x, y⟩)$
25		df-ov	$⊢ x \underset{˙}{-} y = \underset{˙}{-} (⟨x, y⟩)$
26	25	fveq2i	$⊢ N (x \underset{˙}{-} y) = N (\underset{˙}{-} (⟨x, y⟩))$
27	23 24 26	3eqtr4g	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to x (N \circ \underset{˙}{-}) y = N (x \underset{˙}{-} y)$
28		ovres	$⊢ (x \in X \land y \in X) \to x ({D ↾}_{(X \times X)}) y = x D y$
29	28	adantl	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to x ({D ↾}_{(X \times X)}) y = x D y$
30	27 29	eqeq12d	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to (x (N \circ \underset{˙}{-}) y = x ({D ↾}_{(X \times X)}) y \leftrightarrow N (x \underset{˙}{-} y) = x D y)$
31		eqcom	$⊢ N (x \underset{˙}{-} y) = x D y \leftrightarrow x D y = N (x \underset{˙}{-} y)$
32	30 31	bitrdi	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to (x (N \circ \underset{˙}{-}) y = x ({D ↾}_{(X \times X)}) y \leftrightarrow x D y = N (x \underset{˙}{-} y))$
33	32	2ralbidva	$⊢ (G \in Grp \land G \in MetSp) \to (\forall x \in X \forall y \in X x (N \circ \underset{˙}{-}) y = x ({D ↾}_{(X \times X)}) y \leftrightarrow \forall x \in X \forall y \in X x D y = N (x \underset{˙}{-} y))$
34	20 33	bitrd	$⊢ (G \in Grp \land G \in MetSp) \to (N \circ \underset{˙}{-} = {D ↾}_{(X \times X)} \leftrightarrow \forall x \in X \forall y \in X x D y = N (x \underset{˙}{-} y))$
35	34	pm5.32i	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} = {D ↾}_{(X \times X)}) \leftrightarrow ((G \in Grp \land G \in MetSp) \land \forall x \in X \forall y \in X x D y = N (x \underset{˙}{-} y))$
36		df-3an	$⊢ (G \in Grp \land G \in MetSp \land N \circ \underset{˙}{-} = {D ↾}_{(X \times X)}) \leftrightarrow ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} = {D ↾}_{(X \times X)})$
37		df-3an	$⊢ (G \in Grp \land G \in MetSp \land \forall x \in X \forall y \in X x D y = N (x \underset{˙}{-} y)) \leftrightarrow ((G \in Grp \land G \in MetSp) \land \forall x \in X \forall y \in X x D y = N (x \underset{˙}{-} y))$
38	35 36 37	3bitr4i	$⊢ (G \in Grp \land G \in MetSp \land N \circ \underset{˙}{-} = {D ↾}_{(X \times X)}) \leftrightarrow (G \in Grp \land G \in MetSp \land \forall x \in X \forall y \in X x D y = N (x \underset{˙}{-} y))$
39	6 38	bitri	$⊢ G \in NrmGrp \leftrightarrow (G \in Grp \land G \in MetSp \land \forall x \in X \forall y \in X x D y = N (x \underset{˙}{-} y))$

Metamath Proof Explorer

Theorem isngp3

Proof