Metamath Proof Explorer

Theorem tngngp3

Description: Alternate definition of a normed group (i.e., a group equipped with a norm) without using the properties of a metric space. This corresponds to the definition in N. H. Bingham, A. J. Ostaszewski: "Normed versus topological groups: dichotomy and duality", 2010, Dissertationes Mathematicae 472, pp. 1-138 and E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006. (Contributed by AV, 16-Oct-2021)

Ref Expression
Hypotheses tngngp3.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
tngngp3.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
tngngp3.z ⊢ 0 = ( 0g ‘ 𝐺 )
tngngp3.p ⊢ + = ( +g ‘ 𝐺 )
tngngp3.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion tngngp3 ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝑇 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 tngngp3.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 tngngp3.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 tngngp3.z ⊢ 0 = ( 0g ‘ 𝐺 )
4 tngngp3.p ⊢ + = ( +g ‘ 𝐺 )
5 tngngp3.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
6 2 fvexi ⊢ 𝑋 ∈ V
7 fex ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑋 ∈ V ) → 𝑁 ∈ V )
8 6 7 mpan2 ⊢ ( 𝑁 : 𝑋 ⟶ ℝ → 𝑁 ∈ V )
9 1 tnggrpr ⊢ ( ( 𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp ) → 𝐺 ∈ Grp )
10 simp2 ⊢ ( ( ( 𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp ) ∧ 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ ℝ ) → 𝐺 ∈ Grp )
11 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
12 eqid ⊢ ( norm ‘ 𝑇 ) = ( norm ‘ 𝑇 )
13 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
14 11 12 13 nmeq0 ⊢ ( ( 𝑇 ∈ NrmGrp ∧ 𝑥 ∈ ( Base ‘ 𝑇 ) ) → ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑇 ) ) )
15 eqid ⊢ ( invg ‘ 𝑇 ) = ( invg ‘ 𝑇 )
16 11 12 15 nminv ⊢ ( ( 𝑇 ∈ NrmGrp ∧ 𝑥 ∈ ( Base ‘ 𝑇 ) ) → ( ( norm ‘ 𝑇 ) ‘ ( ( invg ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) )
17 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
18 11 12 17 nmtri ⊢ ( ( 𝑇 ∈ NrmGrp ∧ 𝑥 ∈ ( Base ‘ 𝑇 ) ∧ 𝑦 ∈ ( Base ‘ 𝑇 ) ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) ≤ ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) + ( ( norm ‘ 𝑇 ) ‘ 𝑦 ) ) )
19 18 3expa ⊢ ( ( ( 𝑇 ∈ NrmGrp ∧ 𝑥 ∈ ( Base ‘ 𝑇 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑇 ) ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) ≤ ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) + ( ( norm ‘ 𝑇 ) ‘ 𝑦 ) ) )
20 19 ralrimiva ⊢ ( ( 𝑇 ∈ NrmGrp ∧ 𝑥 ∈ ( Base ‘ 𝑇 ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝑇 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) ≤ ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) + ( ( norm ‘ 𝑇 ) ‘ 𝑦 ) ) )
21 14 16 20 3jca ⊢ ( ( 𝑇 ∈ NrmGrp ∧ 𝑥 ∈ ( Base ‘ 𝑇 ) ) → ( ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑇 ) ) ∧ ( ( norm ‘ 𝑇 ) ‘ ( ( invg ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑇 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) ≤ ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) + ( ( norm ‘ 𝑇 ) ‘ 𝑦 ) ) ) )
22 21 ralrimiva ⊢ ( 𝑇 ∈ NrmGrp → ∀ 𝑥 ∈ ( Base ‘ 𝑇 ) ( ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑇 ) ) ∧ ( ( norm ‘ 𝑇 ) ‘ ( ( invg ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑇 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) ≤ ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) + ( ( norm ‘ 𝑇 ) ‘ 𝑦 ) ) ) )
23 22 adantl ⊢ ( ( 𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp ) → ∀ 𝑥 ∈ ( Base ‘ 𝑇 ) ( ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑇 ) ) ∧ ( ( norm ‘ 𝑇 ) ‘ ( ( invg ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑇 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) ≤ ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) + ( ( norm ‘ 𝑇 ) ‘ 𝑦 ) ) ) )
24 23 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp ) ∧ 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ ℝ ) → ∀ 𝑥 ∈ ( Base ‘ 𝑇 ) ( ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑇 ) ) ∧ ( ( norm ‘ 𝑇 ) ‘ ( ( invg ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑇 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) ≤ ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) + ( ( norm ‘ 𝑇 ) ‘ 𝑦 ) ) ) )
25 1 2 tngbas ⊢ ( 𝑁 ∈ V → 𝑋 = ( Base ‘ 𝑇 ) )
26 1 4 tngplusg ⊢ ( 𝑁 ∈ V → + = ( +g ‘ 𝑇 ) )
27 eqidd ⊢ ( 𝑁 ∈ V → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
28 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
29 1 28 tngbas ⊢ ( 𝑁 ∈ V → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑇 ) )
30 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
31 1 30 tngplusg ⊢ ( 𝑁 ∈ V → ( +g ‘ 𝐺 ) = ( +g ‘ 𝑇 ) )
32 31 oveqd ⊢ ( 𝑁 ∈ V → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) )
33 32 adantr ⊢ ( ( 𝑁 ∈ V ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) )
34 27 29 33 grpinvpropd ⊢ ( 𝑁 ∈ V → ( invg ‘ 𝐺 ) = ( invg ‘ 𝑇 ) )
35 5 34 eqtrid ⊢ ( 𝑁 ∈ V → 𝐼 = ( invg ‘ 𝑇 ) )
36 25 26 35 3jca ⊢ ( 𝑁 ∈ V → ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) )
37 36 adantr ⊢ ( ( 𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp ) → ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) )
38 37 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp ) ∧ 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ ℝ ) → ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) )
39 reex ⊢ ℝ ∈ V
40 1 2 39 tngnm ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ ℝ ) → 𝑁 = ( norm ‘ 𝑇 ) )
41 40 3adant1 ⊢ ( ( ( 𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp ) ∧ 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ ℝ ) → 𝑁 = ( norm ‘ 𝑇 ) )
42 1 3 tng0 ⊢ ( 𝑁 ∈ V → 0 = ( 0g ‘ 𝑇 ) )
43 42 adantr ⊢ ( ( 𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp ) → 0 = ( 0g ‘ 𝑇 ) )
44 43 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp ) ∧ 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ ℝ ) → 0 = ( 0g ‘ 𝑇 ) )
45 38 41 44 3jca ⊢ ( ( ( 𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp ) ∧ 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ ℝ ) → ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) )
46 simp1 ⊢ ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) → 𝑋 = ( Base ‘ 𝑇 ) )
47 46 3ad2ant1 ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → 𝑋 = ( Base ‘ 𝑇 ) )
48 simp2 ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → 𝑁 = ( norm ‘ 𝑇 ) )
49 48 fveq1d ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → ( 𝑁 ‘ 𝑥 ) = ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) )
50 49 eqeq1d ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) = 0 ) )
51 simp3 ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → 0 = ( 0g ‘ 𝑇 ) )
52 51 eqeq2d ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → ( 𝑥 = 0 ↔ 𝑥 = ( 0g ‘ 𝑇 ) ) )
53 50 52 bibi12d ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ↔ ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑇 ) ) ) )
54 simp3 ⊢ ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) → 𝐼 = ( invg ‘ 𝑇 ) )
55 54 3ad2ant1 ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → 𝐼 = ( invg ‘ 𝑇 ) )
56 55 fveq1d ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → ( 𝐼 ‘ 𝑥 ) = ( ( invg ‘ 𝑇 ) ‘ 𝑥 ) )
57 48 56 fveq12d ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( ( norm ‘ 𝑇 ) ‘ ( ( invg ‘ 𝑇 ) ‘ 𝑥 ) ) )
58 57 49 eqeq12d ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ↔ ( ( norm ‘ 𝑇 ) ‘ ( ( invg ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) ) )
59 simp2 ⊢ ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) → + = ( +g ‘ 𝑇 ) )
60 59 3ad2ant1 ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → + = ( +g ‘ 𝑇 ) )
61 60 oveqd ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) )
62 48 61 fveq12d ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) = ( ( norm ‘ 𝑇 ) ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) )
63 fveq1 ⊢ ( 𝑁 = ( norm ‘ 𝑇 ) → ( 𝑁 ‘ 𝑥 ) = ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) )
64 fveq1 ⊢ ( 𝑁 = ( norm ‘ 𝑇 ) → ( 𝑁 ‘ 𝑦 ) = ( ( norm ‘ 𝑇 ) ‘ 𝑦 ) )
65 63 64 oveq12d ⊢ ( 𝑁 = ( norm ‘ 𝑇 ) → ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) = ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) + ( ( norm ‘ 𝑇 ) ‘ 𝑦 ) ) )
66 65 3ad2ant2 ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) = ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) + ( ( norm ‘ 𝑇 ) ‘ 𝑦 ) ) )
67 62 66 breq12d ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → ( ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ↔ ( ( norm ‘ 𝑇 ) ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) ≤ ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) + ( ( norm ‘ 𝑇 ) ‘ 𝑦 ) ) ) )
68 47 67 raleqbidv ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → ( ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑇 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) ≤ ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) + ( ( norm ‘ 𝑇 ) ‘ 𝑦 ) ) ) )
69 53 58 68 3anbi123d ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → ( ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ↔ ( ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑇 ) ) ∧ ( ( norm ‘ 𝑇 ) ‘ ( ( invg ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑇 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) ≤ ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) + ( ( norm ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) )
70 47 69 raleqbidv ⊢ ( ( ( 𝑋 = ( Base ‘ 𝑇 ) ∧ + = ( +g ‘ 𝑇 ) ∧ 𝐼 = ( invg ‘ 𝑇 ) ) ∧ 𝑁 = ( norm ‘ 𝑇 ) ∧ 0 = ( 0g ‘ 𝑇 ) ) → ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑇 ) ( ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑇 ) ) ∧ ( ( norm ‘ 𝑇 ) ‘ ( ( invg ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑇 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) ≤ ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) + ( ( norm ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) )
71 45 70 syl ⊢ ( ( ( 𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp ) ∧ 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ ℝ ) → ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑇 ) ( ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑇 ) ) ∧ ( ( norm ‘ 𝑇 ) ‘ ( ( invg ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑇 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) ) ≤ ( ( ( norm ‘ 𝑇 ) ‘ 𝑥 ) + ( ( norm ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) )
72 24 71 mpbird ⊢ ( ( ( 𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp ) ∧ 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ ℝ ) → ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) )
73 10 72 jca ⊢ ( ( ( 𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp ) ∧ 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ ℝ ) → ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )
74 73 3exp ⊢ ( ( 𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp ) → ( 𝐺 ∈ Grp → ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) ) )
75 9 74 mpd ⊢ ( ( 𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp ) → ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) )
76 75 expcom ⊢ ( 𝑇 ∈ NrmGrp → ( 𝑁 ∈ V → ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) ) )
77 76 com13 ⊢ ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝑁 ∈ V → ( 𝑇 ∈ NrmGrp → ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) ) )
78 8 77 mpd ⊢ ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝑇 ∈ NrmGrp → ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) )
79 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
80 simpl ⊢ ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) → 𝐺 ∈ Grp )
81 80 adantl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) → 𝐺 ∈ Grp )
82 simpl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) → 𝑁 : 𝑋 ⟶ ℝ )
83 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑎 ) )
84 83 eqeq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ ( 𝑁 ‘ 𝑎 ) = 0 ) )
85 eqeq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 = 0 ↔ 𝑎 = 0 ) )
86 84 85 bibi12d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ↔ ( ( 𝑁 ‘ 𝑎 ) = 0 ↔ 𝑎 = 0 ) ) )
87 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑎 ) )
88 87 fveq2d ⊢ ( 𝑥 = 𝑎 → ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ ( 𝐼 ‘ 𝑎 ) ) )
89 88 83 eqeq12d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑁 ‘ ( 𝐼 ‘ 𝑎 ) ) = ( 𝑁 ‘ 𝑎 ) ) )
90 fvoveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) = ( 𝑁 ‘ ( 𝑎 + 𝑦 ) ) )
91 83 oveq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) = ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑦 ) ) )
92 90 91 breq12d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝑎 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑦 ) ) ) )
93 92 ralbidv ⊢ ( 𝑥 = 𝑎 → ( ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑎 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑦 ) ) ) )
94 86 89 93 3anbi123d ⊢ ( 𝑥 = 𝑎 → ( ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ↔ ( ( ( 𝑁 ‘ 𝑎 ) = 0 ↔ 𝑎 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑎 ) ) = ( 𝑁 ‘ 𝑎 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑎 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )
95 94 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ 𝑎 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ 𝑎 ) = 0 ↔ 𝑎 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑎 ) ) = ( 𝑁 ‘ 𝑎 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑎 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑦 ) ) ) )
96 simp1 ⊢ ( ( ( ( 𝑁 ‘ 𝑎 ) = 0 ↔ 𝑎 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑎 ) ) = ( 𝑁 ‘ 𝑎 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑎 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ( ( 𝑁 ‘ 𝑎 ) = 0 ↔ 𝑎 = 0 ) )
97 95 96 syl ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ 𝑎 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝑎 ) = 0 ↔ 𝑎 = 0 ) )
98 97 ex ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ( 𝑎 ∈ 𝑋 → ( ( 𝑁 ‘ 𝑎 ) = 0 ↔ 𝑎 = 0 ) ) )
99 98 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) → ( 𝑎 ∈ 𝑋 → ( ( 𝑁 ‘ 𝑎 ) = 0 ↔ 𝑎 = 0 ) ) )
100 99 adantl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) → ( 𝑎 ∈ 𝑋 → ( ( 𝑁 ‘ 𝑎 ) = 0 ↔ 𝑎 = 0 ) ) )
101 100 imp ⊢ ( ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) ∧ 𝑎 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝑎 ) = 0 ↔ 𝑎 = 0 ) )
102 2 4 5 79 grpsubval ⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) = ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) )
103 102 adantl ⊢ ( ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) = ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) )
104 103 fveq2d ⊢ ( ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑁 ‘ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) )
105 3simpc ⊢ ( ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) )
106 105 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) )
107 simpr ⊢ ( ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
108 107 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
109 oveq2 ⊢ ( 𝑦 = ( 𝐼 ‘ 𝑏 ) → ( 𝑎 + 𝑦 ) = ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) )
110 109 fveq2d ⊢ ( 𝑦 = ( 𝐼 ‘ 𝑏 ) → ( 𝑁 ‘ ( 𝑎 + 𝑦 ) ) = ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) )
111 fveq2 ⊢ ( 𝑦 = ( 𝐼 ‘ 𝑏 ) → ( 𝑁 ‘ 𝑦 ) = ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) )
112 111 oveq2d ⊢ ( 𝑦 = ( 𝐼 ‘ 𝑏 ) → ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑦 ) ) = ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) ) )
113 110 112 breq12d ⊢ ( 𝑦 = ( 𝐼 ‘ 𝑏 ) → ( ( 𝑁 ‘ ( 𝑎 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) ) ) )
114 92 113 rspc2v ⊢ ( ( 𝑎 ∈ 𝑋 ∧ ( 𝐼 ‘ 𝑏 ) ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) → ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) ) ) )
115 2 5 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ) → ( 𝐼 ‘ 𝑏 ) ∈ 𝑋 )
116 115 ex ⊢ ( 𝐺 ∈ Grp → ( 𝑏 ∈ 𝑋 → ( 𝐼 ‘ 𝑏 ) ∈ 𝑋 ) )
117 116 anim2d ⊢ ( 𝐺 ∈ Grp → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑎 ∈ 𝑋 ∧ ( 𝐼 ‘ 𝑏 ) ∈ 𝑋 ) ) )
118 117 imp ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑎 ∈ 𝑋 ∧ ( 𝐼 ‘ 𝑏 ) ∈ 𝑋 ) )
119 114 118 syl11 ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) → ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) ) ) )
120 119 expd ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) → ( 𝐺 ∈ Grp → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) ) ) ) )
121 108 120 syl ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ( 𝐺 ∈ Grp → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) ) ) ) )
122 121 imp ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ 𝐺 ∈ Grp ) → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) ) ) )
123 122 imp ⊢ ( ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ 𝐺 ∈ Grp ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) ) )
124 simpl ⊢ ( ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) )
125 124 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) )
126 fveq2 ⊢ ( 𝑥 = 𝑏 → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑏 ) )
127 126 fveq2d ⊢ ( 𝑥 = 𝑏 → ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) )
128 fveq2 ⊢ ( 𝑥 = 𝑏 → ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑏 ) )
129 127 128 eqeq12d ⊢ ( 𝑥 = 𝑏 → ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) = ( 𝑁 ‘ 𝑏 ) ) )
130 129 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ 𝑏 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) = ( 𝑁 ‘ 𝑏 ) )
131 130 eqcomd ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ 𝑏 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑏 ) = ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) )
132 131 ex ⊢ ( ∀ 𝑥 ∈ 𝑋 ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) → ( 𝑏 ∈ 𝑋 → ( 𝑁 ‘ 𝑏 ) = ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) ) )
133 125 132 syl ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ( 𝑏 ∈ 𝑋 → ( 𝑁 ‘ 𝑏 ) = ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) ) )
134 133 adantr ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ 𝐺 ∈ Grp ) → ( 𝑏 ∈ 𝑋 → ( 𝑁 ‘ 𝑏 ) = ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) ) )
135 134 adantld ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ 𝐺 ∈ Grp ) → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑏 ) = ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) ) )
136 135 imp ⊢ ( ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ 𝐺 ∈ Grp ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑁 ‘ 𝑏 ) = ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) )
137 136 oveq2d ⊢ ( ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ 𝐺 ∈ Grp ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑏 ) ) = ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ ( 𝐼 ‘ 𝑏 ) ) ) )
138 123 137 breqtrrd ⊢ ( ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ 𝐺 ∈ Grp ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑏 ) ) )
139 138 ex ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ 𝐺 ∈ Grp ) → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑏 ) ) ) )
140 139 ex ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ( 𝐺 ∈ Grp → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑏 ) ) ) ) )
141 106 140 syl ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ( 𝐺 ∈ Grp → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑏 ) ) ) ) )
142 141 impcom ⊢ ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑏 ) ) ) )
143 142 adantl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑏 ) ) ) )
144 143 imp ⊢ ( ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑁 ‘ ( 𝑎 + ( 𝐼 ‘ 𝑏 ) ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑏 ) ) )
145 104 144 eqbrtrd ⊢ ( ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑁 ‘ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ) ≤ ( ( 𝑁 ‘ 𝑎 ) + ( 𝑁 ‘ 𝑏 ) ) )
146 1 2 79 3 81 82 101 145 tngngpd ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) → 𝑇 ∈ NrmGrp )
147 146 ex ⊢ ( 𝑁 : 𝑋 ⟶ ℝ → ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) → 𝑇 ∈ NrmGrp ) )
148 78 147 impbid ⊢ ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝑇 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑁 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑁 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) )