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

Metamath Proof Explorer

Theorem 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 ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
tngngp.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
tngngp.m ⊢ − = ( -g ‘ 𝐺 )
tngngp.z ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion tngngp ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝑇 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) )

Proof

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