isngp4

Description: Express the property of being a normed group purely in terms of right-translation invariance of the metric instead of using the definition of norm (which itself uses the metric). (Contributed by Mario Carneiro, 29-Oct-2015)

	Ref	Expression
Hypotheses	ngprcan.x	$⊢ X = {Base}_{G}$
	ngprcan.p	$⊢ \underset{˙}{+} = +_{G}$
	ngprcan.d	$⊢ D = dist (G)$
Assertion	isngp4	$⊢ G \in NrmGrp \leftrightarrow (G \in Grp \land G \in MetSp \land \forall x \in X \forall y \in X \forall z \in X (x \underset{˙}{+} z) D (y \underset{˙}{+} z) = x D y)$

Proof

Step	Hyp	Ref	Expression
1		ngprcan.x	$⊢ X = {Base}_{G}$
2		ngprcan.p	$⊢ \underset{˙}{+} = +_{G}$
3		ngprcan.d	$⊢ D = dist (G)$
4		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
5		ngpms	$⊢ G \in NrmGrp \to G \in MetSp$
6	1 2 3	ngprcan	$⊢ (G \in NrmGrp \land (x \in X \land y \in X \land z \in X)) \to (x \underset{˙}{+} z) D (y \underset{˙}{+} z) = x D y$
7	6	ralrimivvva	$⊢ G \in NrmGrp \to \forall x \in X \forall y \in X \forall z \in X (x \underset{˙}{+} z) D (y \underset{˙}{+} z) = x D y$
8	4 5 7	3jca	$⊢ G \in NrmGrp \to (G \in Grp \land G \in MetSp \land \forall x \in X \forall y \in X \forall z \in X (x \underset{˙}{+} z) D (y \underset{˙}{+} z) = x D y)$
9		simp1	$⊢ (G \in Grp \land G \in MetSp \land \forall x \in X \forall y \in X \forall z \in X (x \underset{˙}{+} z) D (y \underset{˙}{+} z) = x D y) \to G \in Grp$
10		simp2	$⊢ (G \in Grp \land G \in MetSp \land \forall x \in X \forall y \in X \forall z \in X (x \underset{˙}{+} z) D (y \underset{˙}{+} z) = x D y) \to G \in MetSp$
11		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
12	1 11	grpinvcl	$⊢ (G \in Grp \land y \in X) \to {inv}_{g} (G) (y) \in X$
13	12	ad2ant2rl	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to {inv}_{g} (G) (y) \in X$
14		eqcom	$⊢ (x \underset{˙}{+} z) D (y \underset{˙}{+} z) = x D y \leftrightarrow x D y = (x \underset{˙}{+} z) D (y \underset{˙}{+} z)$
15		oveq2	$⊢ z = {inv}_{g} (G) (y) \to x \underset{˙}{+} z = x \underset{˙}{+} {inv}_{g} (G) (y)$
16		oveq2	$⊢ z = {inv}_{g} (G) (y) \to y \underset{˙}{+} z = y \underset{˙}{+} {inv}_{g} (G) (y)$
17	15 16	oveq12d	$⊢ z = {inv}_{g} (G) (y) \to (x \underset{˙}{+} z) D (y \underset{˙}{+} z) = (x \underset{˙}{+} {inv}_{g} (G) (y)) D (y \underset{˙}{+} {inv}_{g} (G) (y))$
18	17	eqeq2d	$⊢ z = {inv}_{g} (G) (y) \to (x D y = (x \underset{˙}{+} z) D (y \underset{˙}{+} z) \leftrightarrow x D y = (x \underset{˙}{+} {inv}_{g} (G) (y)) D (y \underset{˙}{+} {inv}_{g} (G) (y)))$
19	14 18	syl5bb	$⊢ z = {inv}_{g} (G) (y) \to ((x \underset{˙}{+} z) D (y \underset{˙}{+} z) = x D y \leftrightarrow x D y = (x \underset{˙}{+} {inv}_{g} (G) (y)) D (y \underset{˙}{+} {inv}_{g} (G) (y)))$
20	19	rspcv	$⊢ {inv}_{g} (G) (y) \in X \to (\forall z \in X (x \underset{˙}{+} z) D (y \underset{˙}{+} z) = x D y \to x D y = (x \underset{˙}{+} {inv}_{g} (G) (y)) D (y \underset{˙}{+} {inv}_{g} (G) (y)))$
21	13 20	syl	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to (\forall z \in X (x \underset{˙}{+} z) D (y \underset{˙}{+} z) = x D y \to x D y = (x \underset{˙}{+} {inv}_{g} (G) (y)) D (y \underset{˙}{+} {inv}_{g} (G) (y)))$
22		eqid	$⊢ -_{G} = -_{G}$
23	1 2 11 22	grpsubval	$⊢ (x \in X \land y \in X) \to x -_{G} y = x \underset{˙}{+} {inv}_{g} (G) (y)$
24	23	adantl	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to x -_{G} y = x \underset{˙}{+} {inv}_{g} (G) (y)$
25	24	eqcomd	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to x \underset{˙}{+} {inv}_{g} (G) (y) = x -_{G} y$
26		eqid	$⊢ 0_{G} = 0_{G}$
27	1 2 26 11	grprinv	$⊢ (G \in Grp \land y \in X) \to y \underset{˙}{+} {inv}_{g} (G) (y) = 0_{G}$
28	27	ad2ant2rl	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to y \underset{˙}{+} {inv}_{g} (G) (y) = 0_{G}$
29	25 28	oveq12d	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to (x \underset{˙}{+} {inv}_{g} (G) (y)) D (y \underset{˙}{+} {inv}_{g} (G) (y)) = (x -_{G} y) D 0_{G}$
30	1 22	grpsubcl	$⊢ (G \in Grp \land x \in X \land y \in X) \to x -_{G} y \in X$
31	30	3expb	$⊢ (G \in Grp \land (x \in X \land y \in X)) \to x -_{G} y \in X$
32	31	adantlr	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to x -_{G} y \in X$
33		eqid	$⊢ norm (G) = norm (G)$
34	33 1 26 3	nmval	$⊢ x -_{G} y \in X \to norm (G) (x -_{G} y) = (x -_{G} y) D 0_{G}$
35	32 34	syl	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to norm (G) (x -_{G} y) = (x -_{G} y) D 0_{G}$
36	29 35	eqtr4d	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to (x \underset{˙}{+} {inv}_{g} (G) (y)) D (y \underset{˙}{+} {inv}_{g} (G) (y)) = norm (G) (x -_{G} y)$
37	36	eqeq2d	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to (x D y = (x \underset{˙}{+} {inv}_{g} (G) (y)) D (y \underset{˙}{+} {inv}_{g} (G) (y)) \leftrightarrow x D y = norm (G) (x -_{G} y))$
38	21 37	sylibd	$⊢ ((G \in Grp \land G \in MetSp) \land (x \in X \land y \in X)) \to (\forall z \in X (x \underset{˙}{+} z) D (y \underset{˙}{+} z) = x D y \to x D y = norm (G) (x -_{G} y))$
39	38	ralimdvva	$⊢ (G \in Grp \land G \in MetSp) \to (\forall x \in X \forall y \in X \forall z \in X (x \underset{˙}{+} z) D (y \underset{˙}{+} z) = x D y \to \forall x \in X \forall y \in X x D y = norm (G) (x -_{G} y))$
40	39	3impia	$⊢ (G \in Grp \land G \in MetSp \land \forall x \in X \forall y \in X \forall z \in X (x \underset{˙}{+} z) D (y \underset{˙}{+} z) = x D y) \to \forall x \in X \forall y \in X x D y = norm (G) (x -_{G} y)$
41	33 22 3 1	isngp3	$⊢ G \in NrmGrp \leftrightarrow (G \in Grp \land G \in MetSp \land \forall x \in X \forall y \in X x D y = norm (G) (x -_{G} y))$
42	9 10 40 41	syl3anbrc	$⊢ (G \in Grp \land G \in MetSp \land \forall x \in X \forall y \in X \forall z \in X (x \underset{˙}{+} z) D (y \underset{˙}{+} z) = x D y) \to G \in NrmGrp$
43	8 42	impbii	$⊢ G \in NrmGrp \leftrightarrow (G \in Grp \land G \in MetSp \land \forall x \in X \forall y \in X \forall z \in X (x \underset{˙}{+} z) D (y \underset{˙}{+} z) = x D y)$

Metamath Proof Explorer

Theorem isngp4

Proof