This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
ngpi.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
ngpi.m ⊢ − = ( -g ‘ 𝑊 )
ngpi.0 ⊢ 0 = ( 0g ‘ 𝑊 )
Assertion ngpi ( 𝑊 ∈ NrmGrp → ( 𝑊 ∈ Grp ∧ 𝑁 : 𝑉 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ngpi.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 ngpi.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
3 ngpi.m ⊢ − = ( -g ‘ 𝑊 )
4 ngpi.0 ⊢ 0 = ( 0g ‘ 𝑊 )
5 ngpgrp ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ Grp )
6 1 2 nmf ⊢ ( 𝑊 ∈ NrmGrp → 𝑁 : 𝑉 ⟶ ℝ )
7 1 2 4 nmeq0 ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) )
8 1 2 3 nmmtri ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
9 8 3expa ⊢ ( ( ( 𝑊 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
10 9 ralrimiva ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ) → ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
11 7 10 jca ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ) → ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) )
12 11 ralrimiva ⊢ ( 𝑊 ∈ NrmGrp → ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) )
13 5 6 12 3jca ⊢ ( 𝑊 ∈ NrmGrp → ( 𝑊 ∈ Grp ∧ 𝑁 : 𝑉 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )