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 ) ∧ ∀ 𝑦𝑉 ( 𝑁 ‘ ( 𝑥 𝑦 ) ) ≤ ( ( 𝑁𝑥 ) + ( 𝑁𝑦 ) ) ) ) )