Metamath Proof Explorer

Theorem 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 ⊢ - ˙ = - W
ngpi.0 ⊢ 0 ˙ = 0 W
Assertion ngpi ⊢ W ∈ NrmGrp → W ∈ Grp ∧ N : V ⟶ ℝ ∧ ∀ x ∈ V N ⁡ x = 0 ↔ x = 0 ˙ ∧ ∀ y ∈ V N ⁡ x - ˙ y ≤ N ⁡ x + N ⁡ y

Proof

Step Hyp Ref Expression
1 ngpi.v ⊢ V = Base W
2 ngpi.n ⊢ N = norm ⁡ W
3 ngpi.m ⊢ - ˙ = - W
4 ngpi.0 ⊢ 0 ˙ = 0 W
5 ngpgrp ⊢ W ∈ NrmGrp → W ∈ Grp
6 1 2 nmf ⊢ W ∈ NrmGrp → N : V ⟶ ℝ
7 1 2 4 nmeq0 ⊢ W ∈ NrmGrp ∧ x ∈ V → N ⁡ x = 0 ↔ x = 0 ˙
8 1 2 3 nmmtri ⊢ W ∈ NrmGrp ∧ x ∈ V ∧ y ∈ V → N ⁡ x - ˙ y ≤ N ⁡ x + N ⁡ y
9 8 3expa ⊢ W ∈ NrmGrp ∧ x ∈ V ∧ y ∈ V → N ⁡ x - ˙ y ≤ N ⁡ x + N ⁡ y
10 9 ralrimiva ⊢ W ∈ NrmGrp ∧ x ∈ V → ∀ y ∈ V N ⁡ x - ˙ y ≤ N ⁡ x + N ⁡ y
11 7 10 jca ⊢ W ∈ NrmGrp ∧ x ∈ V → N ⁡ x = 0 ↔ x = 0 ˙ ∧ ∀ y ∈ V N ⁡ x - ˙ y ≤ N ⁡ x + N ⁡ y
12 11 ralrimiva ⊢ W ∈ NrmGrp → ∀ x ∈ V N ⁡ x = 0 ↔ x = 0 ˙ ∧ ∀ y ∈ V N ⁡ x - ˙ y ≤ N ⁡ x + N ⁡ y
13 5 6 12 3jca ⊢ W ∈ NrmGrp → W ∈ Grp ∧ N : V ⟶ ℝ ∧ ∀ x ∈ V N ⁡ x = 0 ↔ x = 0 ˙ ∧ ∀ y ∈ V N ⁡ x - ˙ y ≤ N ⁡ x + N ⁡ y