ngpi

Description: The properties of a normed group, which is a group accompanied by a norm. (Contributed by AV, 7-Oct-2021)

	Ref	Expression
Hypotheses	ngpi.v	$⊢ V = {Base}_{W}$
	ngpi.n	$⊢ N = norm (W)$
	ngpi.m	$⊢ \underset{˙}{-} = -_{W}$
	ngpi.0	$⊢ \underset{˙}{0} = 0_{W}$
Assertion	ngpi	$⊢ W \in NrmGrp \to (W \in Grp \land N : V ⟶ ℝ \land \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y)))$

Step	Hyp	Ref	Expression
1		ngpi.v	$⊢ V = {Base}_{W}$
2		ngpi.n	$⊢ N = norm (W)$
3		ngpi.m	$⊢ \underset{˙}{-} = -_{W}$
4		ngpi.0	$⊢ \underset{˙}{0} = 0_{W}$
5		ngpgrp	$⊢ W \in NrmGrp \to W \in Grp$
6	1 2	nmf	$⊢ W \in NrmGrp \to N : V ⟶ ℝ$
7	1 2 4	nmeq0	$⊢ (W \in NrmGrp \land x \in V) \to (N (x) = 0 \leftrightarrow x = \underset{˙}{0})$
8	1 2 3	nmmtri	$⊢ (W \in NrmGrp \land x \in V \land y \in V) \to N (x \underset{˙}{-} y) \leq N (x) + N (y)$
9	8	3expa	$⊢ ((W \in NrmGrp \land x \in V) \land y \in V) \to N (x \underset{˙}{-} y) \leq N (x) + N (y)$
10	9	ralrimiva	$⊢ (W \in NrmGrp \land x \in V) \to \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y)$
11	7 10	jca	$⊢ (W \in NrmGrp \land x \in V) \to ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y))$
12	11	ralrimiva	$⊢ W \in NrmGrp \to \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y))$
13	5 6 12	3jca	$⊢ W \in NrmGrp \to (W \in Grp \land N : V ⟶ ℝ \land \forall x \in V ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \forall y \in V N (x \underset{˙}{-} y) \leq N (x) + N (y)))$

Metamath Proof Explorer