tngngp

Description: Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	tngngp.t	$⊢ T = G toNrmGrp N$
	tngngp.x	$⊢ X = {Base}_{G}$
	tngngp.m	$⊢ \underset{˙}{-} = -_{G}$
	tngngp.z	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	tngngp	$⊢ N : X ⟶ ℝ \to (T \in NrmGrp \leftrightarrow (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y))))$

Proof

Step	Hyp	Ref	Expression
1		tngngp.t	$⊢ T = G toNrmGrp N$
2		tngngp.x	$⊢ X = {Base}_{G}$
3		tngngp.m	$⊢ \underset{˙}{-} = -_{G}$
4		tngngp.z	$⊢ \underset{˙}{0} = 0_{G}$
5		eqid	$⊢ dist (T) = dist (T)$
6	1 2 5	tngngp2	$⊢ N : X ⟶ ℝ \to (T \in NrmGrp \leftrightarrow (G \in Grp \land dist (T) \in Met (X)))$
7	6	simprbda	$⊢ (N : X ⟶ ℝ \land T \in NrmGrp) \to G \in Grp$
8		simplr	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to T \in NrmGrp$
9		simpr	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to x \in X$
10	2	fvexi	$⊢ X \in V$
11		reex	$⊢ ℝ \in V$
12		fex2	$⊢ (N : X ⟶ ℝ \land X \in V \land ℝ \in V) \to N \in V$
13	10 11 12	mp3an23	$⊢ N : X ⟶ ℝ \to N \in V$
14	13	ad2antrr	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to N \in V$
15	1 2	tngbas	$⊢ N \in V \to X = {Base}_{T}$
16	14 15	syl	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to X = {Base}_{T}$
17	9 16	eleqtrd	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to x \in {Base}_{T}$
18		eqid	$⊢ {Base}_{T} = {Base}_{T}$
19		eqid	$⊢ norm (T) = norm (T)$
20		eqid	$⊢ 0_{T} = 0_{T}$
21	18 19 20	nmeq0	$⊢ (T \in NrmGrp \land x \in {Base}_{T}) \to (norm (T) (x) = 0 \leftrightarrow x = 0_{T})$
22	8 17 21	syl2anc	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to (norm (T) (x) = 0 \leftrightarrow x = 0_{T})$
23	7	adantr	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to G \in Grp$
24		simpll	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to N : X ⟶ ℝ$
25	1 2 11	tngnm	$⊢ (G \in Grp \land N : X ⟶ ℝ) \to N = norm (T)$
26	23 24 25	syl2anc	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to N = norm (T)$
27	26	fveq1d	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to N (x) = norm (T) (x)$
28	27	eqeq1d	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to (N (x) = 0 \leftrightarrow norm (T) (x) = 0)$
29	1 4	tng0	$⊢ N \in V \to \underset{˙}{0} = 0_{T}$
30	14 29	syl	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to \underset{˙}{0} = 0_{T}$
31	30	eqeq2d	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to (x = \underset{˙}{0} \leftrightarrow x = 0_{T})$
32	22 28 31	3bitr4d	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to (N (x) = 0 \leftrightarrow x = \underset{˙}{0})$
33		simpllr	$⊢ (((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \land y \in X) \to T \in NrmGrp$
34	17	adantr	$⊢ (((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \land y \in X) \to x \in {Base}_{T}$
35	16	eleq2d	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to (y \in X \leftrightarrow y \in {Base}_{T})$
36	35	biimpa	$⊢ (((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \land y \in X) \to y \in {Base}_{T}$
37		eqid	$⊢ -_{T} = -_{T}$
38	18 19 37	nmmtri	$⊢ (T \in NrmGrp \land x \in {Base}_{T} \land y \in {Base}_{T}) \to norm (T) (x -_{T} y) \leq norm (T) (x) + norm (T) (y)$
39	33 34 36 38	syl3anc	$⊢ (((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \land y \in X) \to norm (T) (x -_{T} y) \leq norm (T) (x) + norm (T) (y)$
40	2 16	syl5eqr	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to {Base}_{G} = {Base}_{T}$
41		eqid	$⊢ +_{G} = +_{G}$
42	1 41	tngplusg	$⊢ N \in V \to +_{G} = +_{T}$
43	14 42	syl	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to +_{G} = +_{T}$
44	40 43	grpsubpropd	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to -_{G} = -_{T}$
45	3 44	syl5eq	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to \underset{˙}{-} = -_{T}$
46	45	oveqd	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to x \underset{˙}{-} y = x -_{T} y$
47	26 46	fveq12d	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to N (x \underset{˙}{-} y) = norm (T) (x -_{T} y)$
48	47	adantr	$⊢ (((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \land y \in X) \to N (x \underset{˙}{-} y) = norm (T) (x -_{T} y)$
49	26	fveq1d	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to N (y) = norm (T) (y)$
50	27 49	oveq12d	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to N (x) + N (y) = norm (T) (x) + norm (T) (y)$
51	50	adantr	$⊢ (((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \land y \in X) \to N (x) + N (y) = norm (T) (x) + norm (T) (y)$
52	39 48 51	3brtr4d	$⊢ (((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \land y \in X) \to N (x \underset{˙}{-} y) \leq N (x) + N (y)$
53	52	ralrimiva	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)$
54	32 53	jca	$⊢ ((N : X ⟶ ℝ \land T \in NrmGrp) \land x \in X) \to ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y))$
55	54	ralrimiva	$⊢ (N : X ⟶ ℝ \land T \in NrmGrp) \to \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y))$
56	7 55	jca	$⊢ (N : X ⟶ ℝ \land T \in NrmGrp) \to (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)))$
57		simprl	$⊢ (N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)))) \to G \in Grp$
58		simpl	$⊢ (N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)))) \to N : X ⟶ ℝ$
59		simpl	$⊢ ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)) \to (N (x) = 0 \leftrightarrow x = \underset{˙}{0})$
60	59	ralimi	$⊢ \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)) \to \forall x \in X (N (x) = 0 \leftrightarrow x = \underset{˙}{0})$
61	60	ad2antll	$⊢ (N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)))) \to \forall x \in X (N (x) = 0 \leftrightarrow x = \underset{˙}{0})$
62		fveq2	$⊢ x = a \to N (x) = N (a)$
63	62	eqeq1d	$⊢ x = a \to (N (x) = 0 \leftrightarrow N (a) = 0)$
64		eqeq1	$⊢ x = a \to (x = \underset{˙}{0} \leftrightarrow a = \underset{˙}{0})$
65	63 64	bibi12d	$⊢ x = a \to ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \leftrightarrow (N (a) = 0 \leftrightarrow a = \underset{˙}{0}))$
66	65	rspccva	$⊢ (\forall x \in X (N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land a \in X) \to (N (a) = 0 \leftrightarrow a = \underset{˙}{0})$
67	61 66	sylan	$⊢ ((N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)))) \land a \in X) \to (N (a) = 0 \leftrightarrow a = \underset{˙}{0})$
68		simpr	$⊢ ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)) \to \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)$
69	68	ralimi	$⊢ \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)) \to \forall x \in X \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)$
70	69	ad2antll	$⊢ (N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)))) \to \forall x \in X \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)$
71		fvoveq1	$⊢ x = a \to N (x \underset{˙}{-} y) = N (a \underset{˙}{-} y)$
72	62	oveq1d	$⊢ x = a \to N (x) + N (y) = N (a) + N (y)$
73	71 72	breq12d	$⊢ x = a \to (N (x \underset{˙}{-} y) \leq N (x) + N (y) \leftrightarrow N (a \underset{˙}{-} y) \leq N (a) + N (y))$
74		oveq2	$⊢ y = b \to a \underset{˙}{-} y = a \underset{˙}{-} b$
75	74	fveq2d	$⊢ y = b \to N (a \underset{˙}{-} y) = N (a \underset{˙}{-} b)$
76		fveq2	$⊢ y = b \to N (y) = N (b)$
77	76	oveq2d	$⊢ y = b \to N (a) + N (y) = N (a) + N (b)$
78	75 77	breq12d	$⊢ y = b \to (N (a \underset{˙}{-} y) \leq N (a) + N (y) \leftrightarrow N (a \underset{˙}{-} b) \leq N (a) + N (b))$
79	73 78	rspc2va	$⊢ ((a \in X \land b \in X) \land \forall x \in X \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)) \to N (a \underset{˙}{-} b) \leq N (a) + N (b)$
80	79	ancoms	$⊢ (\forall x \in X \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y) \land (a \in X \land b \in X)) \to N (a \underset{˙}{-} b) \leq N (a) + N (b)$
81	70 80	sylan	$⊢ ((N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)))) \land (a \in X \land b \in X)) \to N (a \underset{˙}{-} b) \leq N (a) + N (b)$
82	1 2 3 4 57 58 67 81	tngngpd	$⊢ (N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y)))) \to T \in NrmGrp$
83	56 82	impbida	$⊢ N : X ⟶ ℝ \to (T \in NrmGrp \leftrightarrow (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in X N (x \underset{˙}{-} y) \leq N (x) + N (y))))$

Metamath Proof Explorer

Theorem tngngp

Proof